Differences
This shows you the differences between two versions of the page.
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. | ||