LARA

Differences

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

Link to this comparison view

sav08:definition_of_presburger_arithmetic [2008/04/15 20:15]
vkuncak
sav08:definition_of_presburger_arithmetic [2015/04/21 17:30]
Line 1: Line 1:
-====== Definition of Presburger Arithmetic ====== 
- 
- 
-===== Minimalistic Language of Presburger Arithmetic ===== 
- 
-Consider $L=\{+\}$ and consider as ${\cal I}$ the set of all interpretations with domain $\mathbb{N} = \{0,​1,​2,​\ldots\}$ where $+$ is interpreted as addition of natural numbers (these interpretations differ only in values for free variables. ​ This is one definition of Presburger arithmetic over natural numbers. 
- 
-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 ===== 
- 
-We look at the theory of integers with addition. 
-  * introduce constant for each integer constant 
-  * to be able to restrict values to natural numbers when needed: ++|we introduce $<$++ 
-  * 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 enable quantifier elimination from $\exists x. y= K \cdot x$ introduce for each $K$ predicate $d_K(y)$ (divisibility by constant) 
- 
-The resulting language 
-\[ 
-    L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} 
-\]