Davis–Putnam algorithm: Difference between revisions

Revision as of 10:32, 26 February 2013

Revision as of 12:53, 20 April 2013

Line 1:

{{Confusing|article|date=February 2009}}

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 (logic)|resolution]]-based decision procedure for [[propositional logic]]. Since the set of valid first-order formulas is [[recursively enumerable]] but not [[Recursive_setRecursive set|recursive]], there exists no general algorithm to solve this problem. Therefore, the Davis-PutnamDavis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis-Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure that is actually only one of the steps of the original algorithm.

The procedure is based on [[Herbrand's theorem]], which implies that an [[satisfiable|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 ''φ'' it is enough to prove that a ground instance of ''¬φ'' is unsatisfiable. If ''φ'' is not valid, then the search for an unsatisfiable ground instance will not terminate.

Line 32:

| issue = 3

| pages = 201–215

| dateyear = 1960

| url = http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034

| doi=10.1145/321033.321034}}

Line 44:

| issue=7

| pages = 394–397

| dateyear=1962

| url=http://portal.acm.org/citation.cfm?doid=368273.368557

| doi=10.1145/368273.368557}}

Line 62:

* {{cite book|author=John Harrison|title=Handbook of practical logic and automated reasoning|year=2009|publisher=Cambridge University Press|isbn=978-0-521-89957-4|pages=79–90}}

{{DEFAULTSORT:Davis-Putnam algorithm}}

[[Category:Boolean algebra]]

[[Category:Constraint programming]]

[[Category:Automated theorem proving]]

{{formalmethods-stub}}