Davis–Putnam algorithm: Difference between revisions

Revision as of 17:47, 18 January 2009

Revision as of 17:07, 5 February 2009

Line 1:

{{confusingConfusing|ground instance needs to be defined|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.

Line 67:

| conferenceurl =

}}

{{formalmethods-stub}}

[[Category:Boolean algebra]]

[[Category:Constraint satisfaction]]

[[Category:Automated theorem proving]]

{{formalmethods-stub}}

[[de:Davis-Putnam-Verfahren]]