Revision as of 01:04, 30 August 2008 edit Linas (talk \| contribs) 25,539 edits err, undo what I did ← Previous edit		Revision as of 12:14, 25 October 2008 edit undo C S (talk \| contribs) Pending changes reviewers 8,453 edits No edit summary Next edit →
Line 1: {{confusing\|ground instance needs to be defined}} 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.

Davis–Putnam algorithm: Difference between revisions