- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

msol_over_strings [2008/05/14 19:23] vkuncak |
msol_over_strings [2008/05/15 09:26] (current) vkuncak |
||
---|---|---|---|

Line 66: | Line 66: | ||

\exists C.\ 0 \notin i\ \land \forall i.\ | \exists C.\ 0 \notin i\ \land \forall i.\ | ||

\big(\begin{array}[t]{rcl} | \big(\begin{array}[t]{rcl} | ||

- | ((i \in Z) &\leftrightarrow& ((i \in X \oplus i \in Y) \oplus i \in C))\ \land\\ | + | ((i \in Z) &\leftrightarrow& ((i \in X) \oplus (i \in Y) \oplus (i \in C))\ \land\\ |

- | ((i+1 \in C) &\leftrightarrow& \mbox{twoOrMore}(i \in X,i \in Y,i \in C)\big) | + | ((i+1 \in C) &\leftrightarrow& \mbox{atLeastTwo}(i \in X,i \in Y,i \in C)\big) |

\end{array} | \end{array} | ||

\end{equation*} | \end{equation*} | ||

Line 73: | Line 73: | ||

\begin{eqnarray*} | \begin{eqnarray*} | ||

x \oplus y &=& (x \lor y) \land \lnot (x \land y) \\ | x \oplus y &=& (x \lor y) \land \lnot (x \land y) \\ | ||

- | \mbox{twoOrMore}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z) | + | \mbox{atLeastTwo}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z) |

\end{eqnarray*} | \end{eqnarray*} | ||

This way we can represent entire Presburger arithmetic in MSOL over strings. Moreover, we have more expressive power because $X \subseteq Y$ means that the one bits of $N(X)$ are included in the bits of $N(Y)$, that is, the bitwise or of $N(X)$ and $N(Y)$ is equal to $N(Y)$. In fact, if we add the relation of bit inclusion into Presburger arithmetic, we obtain precisely the expressive power of MSOL when sets are treated as binary representations of integers (Indeed, taking the minimal syntax of MSOL from the beginning, the bit inclusion gives us the subset, whereas the successor relation $s(x,y)$ is expressible using $y=x+1$.) | This way we can represent entire Presburger arithmetic in MSOL over strings. Moreover, we have more expressive power because $X \subseteq Y$ means that the one bits of $N(X)$ are included in the bits of $N(Y)$, that is, the bitwise or of $N(X)$ and $N(Y)$ is equal to $N(Y)$. In fact, if we add the relation of bit inclusion into Presburger arithmetic, we obtain precisely the expressive power of MSOL when sets are treated as binary representations of integers (Indeed, taking the minimal syntax of MSOL from the beginning, the bit inclusion gives us the subset, whereas the successor relation $s(x,y)$ is expressible using $y=x+1$.) | ||