Content deleted Content added
m Robot - Moving category Constraint satisfaction to Category:Constraint programming per CFD at Wikipedia:Categories for discussion/Log/2011 June 15. |
m format |
||
Line 4:
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.
The procedure roughly consists of these three parts:
| |||