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:list_of_theories_admitting_qe [2008/04/23 15: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 50: Line 50:
  
   * [[http://​theory.stanford.edu/​~tingz/​papers/​jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]   * [[http://​theory.stanford.edu/​~tingz/​papers/​jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]
 +
  
 ===== Products of Structures admiting QE ====== ===== Products of Structures admiting QE ======
  
-Fefeman-Vaught theorem: ​if we have decidable theories.+Fefeman-Vaught theorem: ​ 
 +  * reduce the truth value of quantified formulas over sequences of elements to truth value of formulas over elements 
 +  * the operations on sequences are defined point-wise
  
 +More information in references cited here:
   * [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]   * [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]
 +
 +**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)
 +\end{equation*}
 +\begin{equation*}
 +   (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.
 +
 +Moreover, such reduction can be done even when variables range over infinite sequences of integers
  
 ===== Positive Integers with Multiplication ===== ===== Positive Integers with Multiplication =====
Line 62: 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 84: 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.
 
sav08/list_of_theories_admitting_qe.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice