- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

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. | ||