Lab for Automated Reasoning and Analysis LARA

Finite Models Imply Decidability

Now for some positive results.

Theorem: Suppose that $S$ is a subset of all first-order logic sentences such that for all $F \in S$,

  • $\lnot F \in S$, and
  • if $F$ has a model, then $F$ has a finite model

Then there exists an algorithm that, given a formula from $F \in S$, determinies whether $F$ is valid.

Note: such algorithm is called a decision procedure for the class of formulas $S$.

Note: we have just shown that such algorithm does not exists for the set of all sentences in first-order logic. There is only an algorithm (e.g. resolution) that will terminate when formula is valid, but need not terminate on invalid formulas.


Prover and counterexample finder running in parallel.

sav08/finite_models_imply_decidability.txt · Last modified: 2008/04/03 13:04 by vkuncak
© EPFL 2018 - Legal notice