Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:homework12 [2008/05/14 20:08] vkuncak |
sav08:homework12 [2008/05/15 10:06] vkuncak |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| ===== Problem 2 ===== | ===== Problem 2 ===== | ||
| - | In [[Quantifier elimination definition]] we noted that if the validity of first-order formulas in some theory is decidable, then we can extend the language of formulas so that we have quantifier elimination. Previously we also observed that quantifier interpolation implies the existence of interpolants (see the definition of [[interpolation for propositional logic]] as well as the [[Calculus of Computation Textbook]]). We next apply these observations to weak monadic second-order logic over strings described in [[Lecture23]]. | + | In [[Quantifier elimination definition]] we noted that if the validity of first-order formulas in some theory is decidable, then we can extend the language of formulas so that we have quantifier elimination. Previously we also observed that quantifier elimination implies the existence of interpolants (see the definition of [[interpolation for propositional logic]] as well as the [[Calculus of Computation Textbook]]). We next apply these observations to weak monadic second-order logic over strings described in [[Lecture23]]. |
| Extend the language of monadic second-order logic over strings with new predicate symbols and describe an algorithm that, given formulas $P(x,y)$ and $Q(y,z)$ in this extension (where $x$,$y$,$z$ are $n$-tuples of set variables) checks whether | Extend the language of monadic second-order logic over strings with new predicate symbols and describe an algorithm that, given formulas $P(x,y)$ and $Q(y,z)$ in this extension (where $x$,$y$,$z$ are $n$-tuples of set variables) checks whether | ||
| Line 14: | Line 14: | ||
| \] | \] | ||
| holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$. | holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$. | ||
| + | |||
| + | ===== Optional Problem 3 ===== | ||
| + | |||
| + | Describe the set of all binary relations $r^s_F$ definable through singleton sets | ||
| + | \[ | ||
| + | r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \} | ||
| + | \] | ||
| + | where $F$ are formulas of W1S1. How does this set compare to the set of all binary relations definable in Presburger arithmetic? | ||