Lab for Automated Reasoning and Analysis 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
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