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:39] vkuncak |
sav08:definition_of_presburger_arithmetic [2008/04/15 20:13] vkuncak |
||
---|---|---|---|
Line 17: | Line 17: | ||
* 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} \} | ||
+ | \] | ||