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]
@@ Line 1: / Line 1: @@
-====== List of Some Theories Admitting QE ======
-===== Presburger Arithmetic ======
-As we have just seen in [[QE for Presburger Arithmetic]].
-===== Boolean Algebras with Presburger Arithmetic =====
-  * [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.html|Deciding Boolean Algebra with Presburger Arithmetic]]
-===== Term Algebra ======
-Formulas that are true in Herbrand interpretations of a language with no relation symbols (only equality).
-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
-\[
-    \alpha(f)(t_1,\ldots,t_n) =
-\]
-The question of whether terms are unifiable,
-\[
-    r(x,f(x,y)) \doteq r(f(a,v),f(f(u,b),f(u,u)))
-\]
-becomes the truth value of
-\[
-    \exists x,y,u, v. r(x,f(x,y)) = r(f(a,v),f(f(u,b),f(u,u)))
-\]
-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/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]]
-===== Feature Trees =====
-Related to term algebras.
-  * [[http://www.pps.jussieu.fr/~treinen/teaching/mpri/main.ps|Constraint Solving and Decision Problems of First-Order Theories of Concrete Domains]]
-===== Term Powers =====
-Combines term algebras with products.
-  * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]
-  * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable.html|Structural Subtyping of Non-Recursive Types is Decidable]]
-===== Knuth-Bendix Orders =====
-Extends term algebras with ordering that is used in paramodulation provers.
-  * [[http://theory.stanford.edu/~tingz/papers/jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]
-===== Products of Structures admiting QE ======
-Fefeman-Vaught theorem: if we have decidable theories.
-  * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]
-===== Positive Integers with Multiplication =====
-$(\mathbb{Z}_{+},\cdot)$ where $\mathbb{Z}_{+}$ are positive integers and $\cdot$ is multiplication.
-Consider prime factor representation of integers:
-\[
-    x = \prod_{i=1}^n p_i^{\alpha_i}
-\]
-where $p_1,p_2,\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$.
-The structure is isomorphic to: $(\mathbb{N}^*,\oplus)$ where $\mathbb{N}^*$ are finite sequences of exponents.  Operation $\oplus$ is vector addition.
-We can have only addition or only multiplication, but not both!
-  * [[wk>Hilbert's 10th problem]]
-===== The Field of Complex and Real Numbers =====
-Over complex numbers, we get decidability for both multiplication and addition - theory of polynomials.
-  * [[http://www.springerlink.com/content/74kn4ql49178g673/|Quantifier elimination for real closed fields by cylindrical algebraic decompostion]]
-  * [[wk>Real_closed_field#Decidability_and_quantifier_elimination]]
-  * Upcoming excellent book by John Harrison
-  * [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]]
-===== Mixed Linear and Integer Constraints =====
-Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$,
-\[
-    \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \}
-\]
-Observe that this also subsumes Presburger arithmetic.
-  * [[http://doi.acm.org/10.1145/309831.309888|Mixed real-integer linear quantifier elimination]]
-====== References ======
-  * Wilfrid Hodges: Model Theory
-  * [[http://www.pps.jussieu.fr/~treinen/teaching/mpri/main.ps|Constraint Solving and Decision Problems of First-Order Theories of Concrete Domains]]