Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:list_of_theories_admitting_qe [2008/04/23 15:25] 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. | ||
* [[http://lara.epfl.ch/~kuncak/lectures/Maher88CompleteAxiomatizationsofFiniteRational.pdf|Michael J. Maher: Complete Axiomatizations of Algebras of Finite, Infinite, and Rational Trees]] | * [[http://lara.epfl.ch/~kuncak/lectures/Maher88CompleteAxiomatizationsofFiniteRational.pdf|Michael J. Maher: Complete Axiomatizations of Algebras of Finite, Infinite, and Rational Trees]] | ||
- | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]] | + | * [[http://lara.epfl.ch/~kuncak/lectures/ComonDelor94EquationalFormulaeMembershipConstraints.pdf|H. Comon, C. Delor: Equational Formulae with Membership Constraints]] |
+ | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]] (see also citations in there) | ||
* [[http://theory.stanford.edu/~tingz/papers/cade05.html|The Decidability of the First-order Theory of Knuth-Bendix Order]] | * [[http://theory.stanford.edu/~tingz/papers/cade05.html|The Decidability of the First-order Theory of Knuth-Bendix Order]] | ||
Line 49: | 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 61: | 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 83: | 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. |