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:13] 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} \} | ||
+ | \] | ||