Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:finite_models_imply_decidability [2008/04/02 17:06]
vkuncak created
sav08:finite_models_imply_decidability [2008/04/03 13:04] (current)
vkuncak
Line 1: Line 1:
 ====== Finite Models Imply Decidability ====== ====== Finite Models Imply Decidability ======
  
-Prover and counterexample finder running in parallel.+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.
 +
 +**Proof:**
 +
 +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