• English only

# Differences

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

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.