Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:logic_and_automata_introduction [2008/05/14 10:05] vkuncak |
sav08:logic_and_automata_introduction [2008/05/14 10:10] vkuncak |
||
|---|---|---|---|
| Line 12: | Line 12: | ||
| Common for quantifier elimination and automata-based techniques: characterize the set of all models (interpretations in which $F$ is true). | Common for quantifier elimination and automata-based techniques: characterize the set of all models (interpretations in which $F$ is true). | ||
| - | Example: | + | More generally, for each formula with free variables, we compute the relation that the formula defines. |
| + | |||
| + | Example: compute the unary relation (set) corresponding to this formula $F(z)$: | ||
| \[ | \[ | ||
| \exists x. \exists y.\ z = 2 x + 1 \land z = 3 y + 2 | \exists x. \exists y.\ z = 2 x + 1 \land z = 3 y + 2 | ||
| \] | \] | ||
| + | ++++| | ||
| + | Add 6k to solution, we obtain a solution. | ||
| + | |||
| + | Find solutions in set $\{0,1,2,3,4,5\}$ | ||
| + | |||
| + | Resulting relation for $F(z)$ is $\{ 6k + 5 \mid k \in \mathbb{Z} \}$ | ||
| + | ++++ | ||
| In [[Lecture15]] we have seen that Presburger arithmetic is decidable using quantifier elimination. | In [[Lecture15]] we have seen that Presburger arithmetic is decidable using quantifier elimination. | ||