Content deleted Content added
Fixed some mistakes and added some details. The description of the satisfiability check is still wrong, but I'm to tired to fix it now. (Still a small stub.) |
mNo edit summary |
||
Line 1:
The '''Davis-Putnam algorithm''' was developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the
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.
| |||