Content deleted Content added
mNo edit summary |
mNo edit summary |
||
Line 3:
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.
The procedure roughly consists of these three parts:
* putting the formula in [[prenex]] form
* generating all ground instances
| |||