Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
sav08:logic_and_automata_introduction [2008/05/14 10:04] vkuncak created |
sav08:logic_and_automata_introduction [2008/05/14 10:12] 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 = 3 x + 1 \land z = 5 y + 3 | + | \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} \}$ | ||
+ | ++++ | ||
+ | |||
+ | We need a nice //representation// of relations | ||
+ | * in quantifier elimination these are particular quantifier-free formulas | ||
+ | * in automata-based methods that we will look at, we represent relations as regular languages | ||
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. | ||
- | Today we look at a different decision method for Presburger arithmetic, which generalizes to certain more expressive logics (monadic second-order logic over strings and trees). | + | Today we see an alternative decision method, based on Presburger arithmetic, and then generalize it to more expressive logics: monadic second-order logic over strings and trees. |