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:simple_qe_for_integer_difference_inequalities [2009/04/21 19:19]
vkuncak
sav08:simple_qe_for_integer_difference_inequalities [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== Simple QE for Integer Difference Inequalities ====== ====== Simple QE for Integer Difference Inequalities ======
 +
  
  
Line 5: Line 6:
  
 Consider language: ${\cal L} = \{ {\le} \}$ and the theory of structure $I = (\mathbb{Z},​\alpha)$ where  Consider language: ${\cal L} = \{ {\le} \}$ and the theory of structure $I = (\mathbb{Z},​\alpha)$ where 
-\[+\begin{equation*}
     \alpha({\le}) = \{ (x,y) \mid x \le y \}     \alpha({\le}) = \{ (x,y) \mid x \le y \}
-\]+\end{equation*}
  
 **Lemma:** This theory does not admit quantifier elimination. **Lemma:** This theory does not admit quantifier elimination.
Line 16: Line 17:
  
 ++++|What is the quantifier-free formula equivalent to ++++|What is the quantifier-free formula equivalent to
-\[+\begin{equation*}
     \exists x. x \le y \land x \neq y     \exists x. x \le y \land x \neq y
-\]+\end{equation*}
 ++++ ++++
  
 ++++|It is formula with one free variable, $y$. ++++|It is formula with one free variable, $y$.
-So it must be built out of atomic formulas $y \leq y$ and $y=y$, and is therefore either true or false.+So it must be built out of atomic formulas $y \leq y$ and $y=y$, and is therefore ​it is either ​always ​true or always ​false, regardless of the value of $y$. It thus cannot be equivalent to the above formula.
 ++++ ++++
 **End.** **End.**
Line 31: Line 32:
 ++++| ++++|
 Consider quantifier-free formula $F(x,z)$ equivalent to Consider quantifier-free formula $F(x,z)$ equivalent to
-\[+\begin{equation*}
     \exists y_1. \ldots \exists y_n.\  x < y_1 < y_2 < \ldots < y_n < z     \exists y_1. \ldots \exists y_n.\  x < y_1 < y_2 < \ldots < y_n < z
-\]+\end{equation*}
 ++++ ++++
  
Line 42: Line 43:
  
 Theory of structure $I = (\mathbb{Z},​\alpha)$ where  Theory of structure $I = (\mathbb{Z},​\alpha)$ where 
-\[+\begin{equation*}
     \alpha(R_K) = \{ (x,y) \mid x + K \leq y \}     \alpha(R_K) = \{ (x,y) \mid x + K \leq y \}
-\]+\end{equation*}
 Note that $R_0$ is the less-than-equal relation on integers. Note that $R_0$ is the less-than-equal relation on integers.
  
 
sav08/simple_qe_for_integer_difference_inequalities.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice