Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:homework12 [2008/05/15 10:23]
vkuncak
sav08:homework12 [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Write a regular expression in alphabet $\{x,y,z\} \to \{0,1\}$ denoting relation $z = x + y$ using [[:Regular expressions for automata with parallel inputs]]. ​ Try to make your regular expression as concise and understandable as possible. Write a regular expression in alphabet $\{x,y,z\} \to \{0,1\}$ denoting relation $z = x + y$ using [[:Regular expressions for automata with parallel inputs]]. ​ Try to make your regular expression as concise and understandable as possible.
 +
  
 ===== Problem 2 ===== ===== Problem 2 =====
  
 Describe the set of all binary relations $r^s_F$ definable through singleton sets Describe the set of all binary relations $r^s_F$ definable through singleton sets
-\[+\begin{equation*}
    r^s_F = \{(p,q) \mid F(\{p\},​\{q\}) \}    r^s_F = \{(p,q) \mid F(\{p\},​\{q\}) \}
-\]+\end{equation*}
 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 ​ 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 ​
-\[+\begin{equation*}
    r^p_F = \{ (p,q) \mid G(p,q) \}    r^p_F = \{ (p,q) \mid G(p,q) \}
-\] +\end{equation*} 
-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?​+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 ​of the other, or are they incomparable?​
  
 ===== Optional Problem 3 ===== ===== Optional Problem 3 =====
Line 22: Line 23:
  
 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
-\[+\begin{equation*}
     \forall x,y,z. (P(x,y) \rightarrow Q(y,z))     \forall x,y,z. (P(x,y) \rightarrow Q(y,z))
-\]+\end{equation*}
 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)$.
  
 
sav08/homework12.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice