LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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.