Davis–Putnam algorithm: Difference between revisions

Revision as of 01:03, 6 May 2009

Revision as of 01:22, 17 May 2009

Line 1:

{{Confusing|ground instance needs to be definedarticle|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. 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}}