Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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