The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Algorisme de Davis-Putnam (ca)
- Davis-Putnam-Verfahren (de)
- Algoritmo de Davis-Putnam (es)
- Davis–Putnam algorithm (en)
- Algoritmo di Davis-Putnam (it)
- Algorithme de Davis-Putnam (fr)
- デービス・パトナムのアルゴリズム (ja)
- Procedura Davisa-Putnama (pl)
- Algoritmo de Davis-Putnam (pt)
- Алгоритм Дэвиса — Патнема (ru)
|
| rdfs:comment
| - Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden. (de)
- The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
- デービス・パトナムのアルゴリズム（英: Davis–Putnam algorithm）は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法として（Martin Davis）とヒラリー・パトナム（Hilary Putnam）により1958年に考案され、一般には1960年に発表された。その後の改良版であるDPLLアルゴリズム（Davis-Putnam-Logemann-Loveland algorithm）のベースとなるアルゴリズムである。 なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムはバックトラックを使用する。 (ja)
- O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada. (pt)
- L'algorisme de Davis-Putnam va ser desenvolupat per Martin Davis i Hilary Putnam per comprovar la satisfacibilitat de les fórmules de la lògica proposicional en forma normal conjuntiva, és a dir, en conjunts de clàusules. Això és una forma de resolució en la qual les variables són triades iterativament i eliminades mitjançant la resolució de cada clàusula en la qual la variable apareix afirmada amb una clàusula en la qual la variable és negada. L'algorisme és així: (ca)
- El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue: (es)
- En calcul propositionnel, l'algorithme de Davis-Putnam est une méthode de détermination de la satisfiabilité d'une formule en forme normale conjonctive, c'est-à-dire une conjonction de clauses (disjonctions de littéraux). Il a été développé par Martin Davis et Hilary Putnam. Cet algorithme a d'abord été conçu pour l'obtention automatique de preuves en calcul des prédicats, mais sa principale innovation concerne la réfutation automatique d'un ensemble de clauses. (fr)
- L'algoritmo di Davis-Putnam fu sviluppato da Martin Davis e Hilary Putnam allo scopo di verificare la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF). È un tipo di procedimento di risoluzione nel quale le variabili sono scelte iterativamente ed eliminate, risolvendo ogni clausola in cui questa compaia diretta con ogni clausola in cui compaia negata. (it)
- Procedura Davisa-Putnama – bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji. Idea jest następująca: negację formuły, którą zamierzamy udowodnić zamieniamy na alternatywę koniunkcji alternatyw literałów, czyli alternatywę CNFów. Taki CNF nazywa się tu zbiorem klauzul, natomiast alternatywa CNFów blokiem. Następnie usuwamy wszystkie powtórzenia literałów i fałsze, oraz wszystkie klauzule zawierające jednocześnie literał i jego negację lub też prawdę. (pl)
|
| foaf:depiction
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| thumbnail
| |
| date
| |
| reason
| - In the algorithm below, adding to and removing from a formula should be defined. I guess the formula has to be in clausal normal form , and adding and removing is achieved by set operations? Moreover, the 'consistent set of literals' test, and the concepts 'polarity', 'pure literal' and 'unit propagation' should be briefly explained. (en)
|
| has abstract
| - L'algorisme de Davis-Putnam va ser desenvolupat per Martin Davis i Hilary Putnam per comprovar la satisfacibilitat de les fórmules de la lògica proposicional en forma normal conjuntiva, és a dir, en conjunts de clàusules. Això és una forma de resolució en la qual les variables són triades iterativament i eliminades mitjançant la resolució de cada clàusula en la qual la variable apareix afirmada amb una clàusula en la qual la variable és negada. L'algorisme és així:
* per a cada variable en la fórmula
* per a cada clàusula que continga la variable i cada clàusula que continga la negació de la variable
* resoldre i i afegir la resolució a la fórmula
* eliminar totes les clàusules originals que continguen la variable o la seva negació El nom algorisme Davis-Putnam o algorisme DP de vegades és emprat incorrectament per referir-se a l', el qual està relacionat però és diferent. (ca)
- Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden. (de)
- The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm. (en)
- El algoritmo de Davis-Putnam fue desarrollado por Martin Davis y Hilary Putnam para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en forma normal conjuntiva, es decir, en conjuntos de cláusulas. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada. El algoritmo es como sigue:
* para cada variable en la fórmula
* para cada cláusula que contenga la variable y cada cláusula que contenga la negación de la variable
* resolver y y añadir la resolución a la fórmula
* eliminar todas las cláusulas originales que contengan la variable o su negación El nombre algoritmo Davis-Putnam o algoritmo DP a veces es empleado incorrectamente para referirse al algoritmo DPLL, el cual está relacionado pero es diferente. (es)
- En calcul propositionnel, l'algorithme de Davis-Putnam est une méthode de détermination de la satisfiabilité d'une formule en forme normale conjonctive, c'est-à-dire une conjonction de clauses (disjonctions de littéraux). Il a été développé par Martin Davis et Hilary Putnam. Cet algorithme a d'abord été conçu pour l'obtention automatique de preuves en calcul des prédicats, mais sa principale innovation concerne la réfutation automatique d'un ensemble de clauses. Comme son dérivé plus connu, l'algorithme DPLL, l'algorithme de Davis-Putnam utilise la propagation unitaire et l'élimination des littéraux purs. Mais l'appel récursif utilisé dans l'algorithme DPLL est remplacé par l'utilisation exhaustive de la règle de résolution sur une variable. L'algorithme de Davis-Putnam permet de prouver qu'un ensemble de clauses est satisfiable (ou non), mais contrairement à l'algorithme DPLL, il ne donne pas directement une affectation satisfaisant cet ensemble de clauses. (fr)
- L'algoritmo di Davis-Putnam fu sviluppato da Martin Davis e Hilary Putnam allo scopo di verificare la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF). È un tipo di procedimento di risoluzione nel quale le variabili sono scelte iterativamente ed eliminate, risolvendo ogni clausola in cui questa compaia diretta con ogni clausola in cui compaia negata. L'algoritmo DP è stato il primo algoritmo per la risoluzione di problemi SAT . Ma questo in generale è molto inefficiente poiché richiede un uso esponenziale della memoria, quindi è adatto a problemi di piccole dimensioni. La sua evoluzione è un algoritmo di ricerca chiamato DPLL. A volte l'algoritmo di Davis–Putnam o DP è scorrettamente usato in riferimento DPLL, ma questi due sono ben distinti. (it)
- デービス・パトナムのアルゴリズム（英: Davis–Putnam algorithm）は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法として（Martin Davis）とヒラリー・パトナム（Hilary Putnam）により1958年に考案され、一般には1960年に発表された。その後の改良版であるDPLLアルゴリズム（Davis-Putnam-Logemann-Loveland algorithm）のベースとなるアルゴリズムである。 なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムはバックトラックを使用する。 (ja)
- Procedura Davisa-Putnama – bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji. Idea jest następująca: negację formuły, którą zamierzamy udowodnić zamieniamy na alternatywę koniunkcji alternatyw literałów, czyli alternatywę CNFów. Taki CNF nazywa się tu zbiorem klauzul, natomiast alternatywa CNFów blokiem. Następnie usuwamy wszystkie powtórzenia literałów i fałsze, oraz wszystkie klauzule zawierające jednocześnie literał i jego negację lub też prawdę. Reguły systemu:
* subsumpcja – jeśli w pewnym zbiorze klauzul klauzula C subsumuje klauzulę D, czyli wszystkie literały C występują też w D, to usuwamy D
* jeśli w pewnym zbiorze klauzul jakiś literał występuje tylko pozytywnie lub tylko negatywnie, usuwamy z niego wszystkie klauzule które go zawierają
* jeśli w pewnym zbiorze klauzul jakaś klauzula to pojedynczy literał, usuwamy wszystkie klauzule zawierające ten literał, oraz zaprzeczenie tego literału z wszystkich klauzul zbioru, które go zawierały
* splitting – jeśli w pewnym zbiorze klauzul pewien literał występuje zarówno pozytywnie jak i negatywnie zastępujemy cały zbiór dwoma zbiorami:
* jednym, w którym usunięte zostały wszystkie klauzule zawierające ten literał, oraz wszystkie wystąpienia jego negacji
* drugim, w którym usunięte zostały wszystkie wystąpienia tego literału, oraz wszystkie klauzule zawierające jego negację
* usuwamy każdy zbiór klauzul zawierają klauzulę pustą – klauzula ta usuwa wszystkie inne przez subsumpcje i ma wartość fałsz, a co za tym idzie zbiór klauzul ma wartość fałsz, która jest nieistotna dla bloku będącego alternatywą Jeśli w bloku nie ma już zbiorów klauzul twierdzenie zostało udowodnione (taki blok, jako alternatywa, jest fałszywy – skoro negacja formuły jest fałszywa, to twierdzenie to jest prawdziwe). Jeśli został jakiś pusty zbiór klauzul, twierdzenie to jest fałszywe (jego zaprzeczenie jest spełnialne). (pl)
- O Algoritmo de Davis-Putnam, criado por Martin Davis e Hilary Putnam, foi um dos pioneiros na área de checagem da satisfatibilidade de uma fórmula quando essa encontra-se na Forma Normal Conjuntiva (FNC). É uma forma de resolução em que cada variável é escolhida pelo fato de se poder resolver todas as cláusulas em que a mesma está contida na sua forma positiva com qualquer cláusula em que ela encontre-se em sua forma negada. (pt)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
