This is an old revision of the document!
List of Some Theories Admitting QE
Presburger Arithmetic
As we have just seen in QE for Presburger Arithmetic.
Boolean Algebras 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 is set of ground terms over , we consider the class of interpretations 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.
Feature Trees
Related to term algebras.
Term Powers
Combines term algebras with products.
Knuth-Bendix Orders
Extends term algebras with ordering that is used in paramodulation provers.
Products of Structures admiting QE
Fefeman-Vaught theorem: if we have decidable theories.
Positive Integers with Multiplication
where are positive integers and is multiplication.
Consider prime factor representation of integers: \[
x = \prod_{i=1}^n p_i^{\alpha_i}
\] where is sequence of prime numbers and .
The structure is isomorphic to: where are finite sequences of exponents. Operation is vector addition.
We can have only addition or only multiplication, but not both!
The Field of Complex and Real Numbers
Over complex numbers, we get decidability for both multiplication and addition - theory of polynomials.
- Upcoming excellent book by John Harrison
Mixed Linear and Integer Constraints
Linear arithmetic over rationals (, , multiplication by rational constants) with operator, for , \[
\lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \}
\]
Observe that this also subsumes Presburger arithmetic.
References
- Wilfrid Hodges: Model Theory