| dbpprop:abstract
|
- The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula. It is known that there exist no decision procedure for this task. Therefore the Davis–Putnam procedure does not terminate on some inputs. The procedure is based on Herbrand's theorem, which implies that an unsatisfiable formula has an unsatisfiable ground instance, and on the fact that a formula is valid if and only if its negation is unsatisfiable. Taken together, these facts imply that to prove the validity of <math>\phi</math> it is enough to prove that a ground instance of <math>\lnot\phi</math> is unsatisfiable. If <math>\phi</math> isn't valid, then the search for an unsatisfiable ground instance will not terminate. The procedure roughly consists of these three parts: put the formula in prenex form and eliminate quantifiers generate one by one all ground instances ... and check for each if it is satisfiable The last part is probably the most innovative one, and works as follows: for every variable in the formula for every clause <math>c</math> containing the variable and every clause <math>n</math> containing the negation of the variable resolve c and n and add the resolvent to the formula remove all original clauses containing the variable or its negation The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is equisatisfiable but not equivalent with the original one. The DPLL algorithm is a refinement of the Davis–Putnam procedure that stemmed from its first implementation.
- Das Davis-Putnam-Verfahren entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in Konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem DPLL (Davis-Putnam-Logemann-Loveland) Algorithmus, verwechselt werden.
- 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. Il a été développé par Martin Davis et Hilary Putnam.
- L'algoritmo 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 clausale. È 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 funziona come espresso di seguito: per ogni variabile nella formula per ogni clausola <math>c</math> contenente la variabile e per ogni clausola <math>n</math> contenente la negazione della variabile risolvi <math>c</math> e <math>n</math> e aggiungi il risolvente nella formula rimuovi tutte le clausole originarie che contenevano la variabile diretta o negata Il nome Davis–Putnam o DP è a volte scorrettamente usato in riferimento al correlato ma distinto algoritmo DPLL.
- Procedura Davisa-Putnama to 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ę. Teraz mamy następujące reguły: 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ą Wyjaśnienie: 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).
- 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.
|
| rdfs:comment
|
- The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula. It is known that there exist no decision procedure for this task. Therefore the Davis–Putnam procedure does not terminate on some inputs. The procedure is based on Herbrand's theorem, which implies that an unsatisfiable formula has an unsatisfiable ground instance, and on the fact that a formula is valid if and only if its negation is unsatisfiable.
- Das Davis-Putnam-Verfahren entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in Konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem DPLL (Davis-Putnam-Logemann-Loveland) Algorithmus, verwechselt werden.
- 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. Il a été développé par Martin Davis et Hilary Putnam.
- L'algoritmo 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 clausale. È 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.
- Procedura Davisa-Putnama to 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.
- 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.
|
![[RDF Data]](/statics/sw-cube.png)
