LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:list_of_theories_admitting_qe [2009/04/22 10:28]
vkuncak 		sav08:list_of_theories_admitting_qe [2015/04/21 17:30] (current)
Line 14: Line 14:
  
 A language containing arbitrary function symbols and constants. ​ If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where A language containing arbitrary function symbols and constants. ​ If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where
-\[+\begin{equation*}
     \alpha(f)(t_1,​\ldots,​t_n) =      \alpha(f)(t_1,​\ldots,​t_n) = 
-\]+\end{equation*}
  
 The question of whether terms are unifiable, The question of whether terms are unifiable,
-\[+\begin{equation*}
     r(x,f(x,y)) \doteq r(f(a,​v),​f(f(u,​b),​f(u,​u)))     r(x,f(x,y)) \doteq r(f(a,​v),​f(f(u,​b),​f(u,​u)))
-\]+\end{equation*}
 becomes the truth value of becomes the truth value of
-\[+\begin{equation*}
     \exists x,y,u, v. r(x,f(x,y)) = r(f(a,​v),​f(f(u,​b),​f(u,​u)))     \exists x,y,u, v. r(x,f(x,y)) = r(f(a,​v),​f(f(u,​b),​f(u,​u)))
-\]+\end{equation*}
 in this theory. ​ We can express more complex constraints. in this theory. ​ We can express more complex constraints.
  
Line 62: Line 62:
  
 **Example:​** Consider logic that quantifies over pairs of integers and where addition is given by **Example:​** Consider logic that quantifies over pairs of integers and where addition is given by
-\[+\begin{equation*}
    (x,y) + (u,v) = (x+u,y+v)    (x,y) + (u,v) = (x+u,y+v)
-\] +\end{equation*} 
-\[+\begin{equation*}
    (x,y) < (u,v) \ \leftrightarrow\ ​ (x < y \land y < v)    (x,y) < (u,v) \ \leftrightarrow\ ​ (x < y \land y < v)
-\]+\end{equation*}
 Formulas in such logic, where variables range over pairs, can be reduced to Presburger arithmetic. Formulas in such logic, where variables range over pairs, can be reduced to Presburger arithmetic.
  
Line 77: Line 77:
  
 Consider prime factor representation of integers: Consider prime factor representation of integers:
-\[+\begin{equation*}
     x = \prod_{i=1}^n p_i^{\alpha_i}     x = \prod_{i=1}^n p_i^{\alpha_i}
-\]+\end{equation*}
 where $p_1,​p_2,​\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$. where $p_1,​p_2,​\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$.
  
Line 99: Line 99:
  
 Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$,​ Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$,​
-\[+\begin{equation*}
     \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \}     \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \}
-\]+\end{equation*}
  
 Observe that this also subsumes Presburger arithmetic. Observe that this also subsumes Presburger arithmetic.