The Basic Process
A conjecture is a logical consequence of a set of axioms iff
every model of the axioms is a model of the formula.
Algorithm
- Find model of negated conjecture and axioms selected so far
- If no such model, logic consequence is established
- Else choose axiom that is false in the model
Intuition
- Each axiom excludes the model (and others) from being a model
of the axioms and negated conjecture
- The model may be finite or infinite, provided formulae can be evaluated