Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:definition_of_presburger_arithmetic [2008/04/15 16:00] vkuncak created |
sav08:definition_of_presburger_arithmetic [2008/04/15 20:14] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| ===== Minimalistic Language of Presburger Arithmetic ===== | ===== Minimalistic Language of Presburger Arithmetic ===== | ||
| - | $(\mathbb{N},+)$ where $\mathbb{N} = \{0,1,2,\ldots\}$ and $+$ is addition of natural numbers. We consider of all interpretations with domain $\mathbb{N}$ where $+$ is interpreted as addition of natural numbers (these interpretations differ only in values for free variables, not in truth value for sentences). | + | 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 language is a good motivation, illustrates the simplicity, but is very far from allowing QE. For example, it does not have a name for zero, so we cannot express $\forall x. x+y=x$. | + | 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$. |
| - | We instead look at $(\mathbb{Z},+,\le,0)$ where $\mathbb{Z}$ is the set of integers. | + | ===== 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} \} | ||
| + | \] | ||