Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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*}
  
 
sav08/definition_of_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice