LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav08:homework12 [2008/05/15 10:06]
vkuncak
sav08:homework12 [2008/05/15 10:23]
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 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]]. +Describe ​the set of all binary relations ​$r^s_Fdefinable through singleton sets
- +
-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+
 \[ \[
-    ​\forall x,​y,​z. ​(P(x,y) \rightarrow Q(y,z))+   r^s_F = \{(p,q) \mid F(\{p\},\{q\}\}
 \] \]
-holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$.+where $F$ are formulas of WS1S.  How does this set of $r^s_F$ compare to the set of all binary relations definable in Presburger arithmetic  
 +\[ 
 +   r^p_F = \{ (p,q\mid G(p,q\} 
 +\] 
 +where $G$ is a Presburger arithmetic formula Are the set of all $r^s_F$ and set of all $r^p_F$ equal, is one strict subset, or are they incomparable?​
  
 ===== Optional Problem 3 ===== ===== Optional Problem 3 =====
  
-Describe ​the set of all binary relations ​$r^s_Fdefinable through singleton sets+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
 \[ \[
-   r^s_F = \{(p,q) \mid F(\{p\},\{q\}\}+    ​\forall x,​y,​z. ​(P(x,y) \rightarrow Q(y,z))
 \] \]
-where $Fare formulas of W1S1 How does this set compare to the set of all binary relations definable in Presburger arithmetic?+holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$.