Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:logic_and_automata_introduction [2008/05/14 10:05] vkuncak |
sav08:logic_and_automata_introduction [2008/05/14 11:06] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Logic and Automata Introduction ====== | + | ====== Logic and Automata - Introduction ====== |
| Satisfiability of $F$: is there an interpretation in which $F$ is true. | Satisfiability of $F$: is there an interpretation in which $F$ is true. | ||
| 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{N} \}$. \\ | ||
| + | |||
| + | Representation as quantifier-free formula. \\ | ||
| + | |||
| + | Representation as a regular language. | ||
| + | ++++ | ||
| + | |||
| + | ===== Basic Idea ===== | ||
| + | |||
| + | We come up with 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. |