- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:definition_of_presburger_arithmetic [2008/04/15 20:15] vkuncak |
sav08:definition_of_presburger_arithmetic [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 7: | Line 7: | ||

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$. | 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$. | ||

+ | |||

===== Language of Presburger Arithmetic that Admits QE ===== | ===== Language of Presburger Arithmetic that Admits QE ===== | ||

Line 15: | Line 16: | ||

* 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 $K|y$ (divisibility by constant) |

The resulting language | The resulting language | ||

- | \[ | + | \begin{equation*} |

L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} | L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} | ||

- | \] | + | \end{equation*} |