Davis–Putnam algorithm
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.
- Comment
- enThe 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.
- Date
- enJune 2021
- Depiction
- Has abstract
- enThe 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.
- Is primary topic of
- Davis–Putnam algorithm
- Label
- enDavis–Putnam algorithm
- Link from a Wikipage to an external page
- portal.acm.org/citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=321034
- portal.acm.org/citation.cfm%3Fdoid=368273.368557
- archive.org/details/handbookpractica00harr%7Curl-access=limited%7Cyear=2009%7Cpublisher=Cambridge
- archive.org/details/handbookpractica00harr/page/n100
- Link from a Wikipage to another Wikipage
- Category:Automated theorem proving
- Category:Boolean algebra
- Category:Constraint programming
- Communications of the ACM
- Davis–Putnam–Logemann–Loveland algorithm
- Empty clause
- Equisatisfiable
- File:Resolution.png
- First-order logic
- Ground instance
- Herbrand's theorem
- Herbrandization
- Hilary Putnam
- Journal of the ACM
- Logical equivalence
- Martin Davis (mathematician)
- Prenex
- Propositional logic
- Recursively enumerable
- Recursive set
- Resolution (logic)
- Satisfiable
- SAT solver
- Unit propagation
- Reason
- enIn 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.
- SameAs
- Algorisme de Davis-Putnam
- Algorithme de Davis-Putnam
- Algoritmo de Davis-Putnam
- Algoritmo de Davis-Putnam
- Algoritmo di Davis-Putnam
- Davis-Putnam-Verfahren
- Di3N
- m.07 p4x
- Procedura Davisa-Putnama
- Q1177898
- Алгоритм Дэвиса — Патнема
- デービス・パトナムのアルゴリズム
- Subject
- Category:Automated theorem proving
- Category:Boolean algebra
- Category:Constraint programming
- Thumbnail
- WasDerivedFrom
- Davis–Putnam algorithm?oldid=1071405701&ns=0
- WikiPageLength
- 7042
- Wikipage page ID
- 2732435
- Wikipage revision ID
- 1071405701
- WikiPageUsesTemplate
- Template:Algorithm-begin
- Template:Algorithm-end
- Template:Cite book
- Template:Cite conference
- Template:Cite journal
- Template:Clarify
- Template:Formalmethods-stub
