Content deleted Content added
m Citation maintenance. You can use this bot yourself! Please report any bugs. |
termination is not required to be called an algorithm |
||
Line 1:
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
The procedure is based on [[Herbrand's theorem]], which implies that an un[[satisfiable]] formula has is un[[satisfiable]] [[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.
| |||