Semidecision Procedure for Validity of Formulas in First-Order Logic

Davis–Putnam algorithm (see Martin Davis, Martin Davis and Hilary Putnam)

Suppose $S$ has no model.

Then $propExpand(S)$ has no model.

By propositional Compactness Theorem, some finite subset has no model.

Can check satisfiability of larger and larger initial prefixes of $propExpand(S)$ 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.)