Content deleted Content added
Algebraist (talk | contribs) m moved Davis-Putnam algorithm to Davis–Putnam algorithm over redirect: en dash not hyphen, per WP:MOSDASH |
Algebraist (talk | contribs) m hyphen to en dash, per WP:DASH |
||
Line 1:
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.
Line 17:
The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is [[equisatisfiable]] but not [[equivalent]] with the original one.
The [[DPLL algorithm]] is a refinement of the
{{Comp-sci-stub}}
Line 56:
| editor = J. Doyle and E. Sandewall and P. Torasso
| year =
| title = Directional Resolution: The
| conference =
| booktitle = Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94)
| |||