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