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? | ||