Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:definition_of_presburger_arithmetic [2008/04/15 19:27] vkuncak |
sav08:definition_of_presburger_arithmetic [2008/04/15 20:15] vkuncak |
||
|---|---|---|---|
| Line 14: | Line 14: | ||
| * to be able to restrict values to natural numbers when needed: ++|we introduce $<$++ | * to be able to restrict values to natural numbers when needed: ++|we introduce $<$++ | ||
| * 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 $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} \} | ||
| + | \] | ||