• English only

# Differences

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

 sav08:list_of_theories_admitting_qe [2008/04/23 15:28]vkuncak sav08:list_of_theories_admitting_qe [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/04/22 10:28 vkuncak 2008/04/23 15:28 vkuncak 2008/04/23 15:25 vkuncak 2008/04/16 22:36 vkuncak 2008/04/16 10:40 vkuncak 2008/04/16 10:39 vkuncak 2008/04/16 10:32 vkuncak 2008/04/16 10:32 vkuncak 2008/04/16 10:31 vkuncak 2008/04/16 10:30 vkuncak 2008/04/16 10:28 vkuncak 2008/04/16 10:16 vkuncak 2008/04/16 10:16 vkuncak 2008/04/16 10:15 vkuncak 2008/04/11 18:31 vkuncak 2008/04/11 18:26 vkuncak 2008/04/11 18:25 vkuncak 2008/04/10 13:11 vkuncak 2008/04/09 21:53 vkuncak 2008/04/09 21:52 vkuncak created Next revision Previous revision 2009/04/22 10:28 vkuncak 2008/04/23 15:28 vkuncak 2008/04/23 15:25 vkuncak 2008/04/16 22:36 vkuncak 2008/04/16 10:40 vkuncak 2008/04/16 10:39 vkuncak 2008/04/16 10:32 vkuncak 2008/04/16 10:32 vkuncak 2008/04/16 10:31 vkuncak 2008/04/16 10:30 vkuncak 2008/04/16 10:28 vkuncak 2008/04/16 10:16 vkuncak 2008/04/16 10:16 vkuncak 2008/04/16 10:15 vkuncak 2008/04/11 18:31 vkuncak 2008/04/11 18:26 vkuncak 2008/04/11 18:25 vkuncak 2008/04/10 13:11 vkuncak 2008/04/09 21:53 vkuncak 2008/04/09 21:52 vkuncak created 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.