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]
@@ Line 1: / Line 1: @@
-====== Simple QE for Integer Difference Inequalities ======
-===== Language of Less-Than-Equals Over Integers =====
-Consider language: ${\cal L} = \{ {\le} \}$ and the theory of structure $I = (\mathbb{Z},\alpha)$ where
-\[
-    \alpha({\le}) = \{ (x,y) \mid x \le y \}
-\]
-**Lemma:** This theory does not admit quantifier elimination.
-**Proof.**
-Suppose the theory admits quantifier elimination.
-++++|What is the quantifier-free formula equivalent to
-\[
-    \exists x. x \le y \land x \neq 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.
-++++
-**End.**
-So $<$ must be expressible.  Let us extend the language: consider theory in language ${\cal L} = \{ \le, < \}$ with $<$ interpreted as $<$ on integers.
-Does the theory of this structure admit quantifier elimination?
-++++|
-Consider quantifier-free formula $F(x,z)$ equivalent to
-\[
-    \exists y_1. \ldots \exists y_n.\  x < y_1 < y_2 < \ldots < y_n < z
-\]
-++++
-===== Extending the Language =====
-Language: ${\cal L} = \{ R_K \mid K \in \mathbb{Z} \}$
-Theory of structure $I = (\mathbb{Z},\alpha)$ where
-\[
-    \alpha(R_K) = \{ (x,y) \mid x + K \leq y \}
-\]
-Note that $R_0$ is the less-than-equal relation on integers.
-In other words, we look at the language of this syntax, where $V$ is the set of variables:
-<code>
-F ::= A | (F&F) | (F|F) | ~F | ALL V.F | EX V.F
-A ::= v=v | v + K ≤ v | true | false
-K ::= ... -2 | -1 | 0 | 1 | 2 | ...
-</code>
-Equality is expressed by ++| $x + 0 \leq y \wedge y + 0 \leq x$ ++
-===== Quantifier Elimination in the Extended Language =====
-Quantifier elimination for this language is similar to [[Simple QE for Dense Linear Orders]].
-What is $\lnot (x + K \le y)$ equivalent to?++|\\
-$y < x + K$\\
-$y + 1 \le x + K$\\
-$y + (1-K) \le x$++
-What are conjunctions of literals equivalent to? ++|$\exists y. \bigwedge_{i=1}^n x_i+K_i \le y \land \bigwedge_{j=1}^m y + L_j \le z_j$ ++
-How do we eliminate existential quantifier? ++++ |\\
-Using $x_i + K_1 \le y$ and $y \le z_j - L_j$\\
-$\bigwedge_{i,j} x_i + K_i \le z_j - L_j$\\
-$\bigwedge_{i,j} x_i + (K_i + L_j) \le z_j$
-++++
-==Example==
-Prove:\\
-$\forall y \exists x . x \leq y \wedge x \neq y $
-++++|\\
-$\exists x . x \leq y \wedge (x < y \vee y  < x)$\\
-$\exists x . x \leq y \wedge (x + 1 \leq y \vee y + 1 \leq x)$\\
-$(\exists x . x \leq y \wedge x + 1 \leq y) \vee (\exists x . x \leq y \wedge y + 1 \leq x)$\\
-$true \vee false$\\
-$true$
-++++
-If we apply this technique to a closed formula in this theory, what formulas do we obtain as a result?