Content deleted Content added
No edit summary |
→Overview: suggest image |
||
Line 2:
==Overview==
[[File:Resolution.png|thumb|400px|Two runs of the [[:en:Davis-Putnam procedure|Davis-Putnam procedure]] on example propositional ground instances.
''Top to bottom, Left:'' Starting from the formula <math>(a \lor b \lor c) \land (b \lor \lnot c \lor \lnot f) \land (\lnot b \lor e)</math>, the algorithm resolves on <math>b</math>, and then on <math>c</math>. Since no further resolution is possible, the algorithm stops; since the [[empty clause]] couldn't be derived, the result is "''satisfiable''".
''Right:'' Resolving the given formula on <math>b</math>, then on <math>a</math>, then on <math>c</math> yields the empty clause; hence the algorithm returns "''unsatisfiable''".]]
The procedure is based on [[Herbrand's theorem]], which implies that an [[satisfiable|unsatisfiable]] formula has an unsatisfiable [[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 ''φ'' it is enough to prove that a ground instance of ''¬φ'' is unsatisfiable. If ''φ'' is not valid, then the search for an unsatisfiable ground instance will not terminate.
| |||