This is an old revision of the document!
Semidecision Procedure for Validity of Formulas in First-Order Logic
Suppose has no model.
Then has no model.
By compactness, some finite subset has no model.
Can check satisfiability of larger and larger initial prefixes of using a SAT solver.
At some point we will reach a contradiction.
Semidecision procedure: if there exists a model, this procedure will loop forever.
- we cannot do much better in general: first-order logic is undecidable
(Some other logics do not even have semi-decision procedures.)