# Differences

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

 sav08:definition_of_presburger_arithmetic [2008/04/15 20:15]vkuncak sav08:definition_of_presburger_arithmetic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/04/22 17:11 piskac 2008/04/15 20:15 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:13 vkuncak 2008/04/15 19:57 vkuncak 2008/04/15 19:39 vkuncak 2008/04/15 19:27 vkuncak 2008/04/15 16:00 vkuncak created Next revision Previous revision 2009/04/22 17:11 piskac 2008/04/15 20:15 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:14 vkuncak 2008/04/15 20:13 vkuncak 2008/04/15 19:57 vkuncak 2008/04/15 19:39 vkuncak 2008/04/15 19:27 vkuncak 2008/04/15 16:00 vkuncak created Line 7: Line 7: This theory is very simple to describe, but it is very far from allowing quantifier-elimination. ​ For example, it does not have a name for zero, so we cannot express $\forall x. x+y=x$. ​ It also does not have a way to express $\exists y. x+y=z$. This theory is very simple to describe, but it is very far from allowing quantifier-elimination. ​ For example, it does not have a name for zero, so we cannot express $\forall x. x+y=x$. ​ It also does not have a way to express $\exists y. x+y=z$. + ===== Language of Presburger Arithmetic that Admits QE ===== ===== Language of Presburger Arithmetic that Admits QE ===== Line 15: Line 16: * introduce not only addition but also subtraction ​ * introduce not only addition but also subtraction ​ * to conveniently express certain expressions,​ introduce function $m_K$ for each $K \in {\cal Z}$, to be interpreted as multiplication by a constant, $m_K(x)= K \cdot x$.  We write $m_K$ as $K \cdot x$ * to conveniently express certain expressions,​ introduce function $m_K$ for each $K \in {\cal Z}$, to be interpreted as multiplication by a constant, $m_K(x)= K \cdot x$.  We write $m_K$ as $K \cdot x$ - * to enable quantifier elimination from $\exists x. y= K \cdot x$ introduce for each $K$ predicate $d_K(y)$ (divisibility by constant) + * to enable quantifier elimination from $\exists x. y= K \cdot x$ introduce for each $K$ predicate $K|y$ (divisibility by constant) The resulting language The resulting language - $+ \begin{equation*} L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} -$ + \end{equation*}