Davis–Putnam algorithm: Difference between revisions

Revision as of 01:22, 17 May 2009

Revision as of 19:24, 11 June 2009

Line 3:

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.{{Fact|date=May 2009}}

The procedure is based on [[Herbrand's theorem]], which implies that an [[satisfiable|unsatisfiable]] formula has isan 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: