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.