Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:simple_qe_for_integer_difference_inequalities [2009/04/22 00:04] vkuncak |
sav08:simple_qe_for_integer_difference_inequalities [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 6: | 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 17: | 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*} |
++++ | ++++ | ||
Line 32: | 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 43: | 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. | ||