- English only

# Lab for Automated Reasoning and Analysis LARA

# 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. | ||