List of Some Theories Admitting QE
As we have just seen in QE for Presburger Arithmetic.
Boolean Algebras with Presburger Arithmetic
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
The question of whether terms are unifiable,
becomes the truth value of
in this theory. We can express more complex constraints.
- On the Theory of Structural Subtyping (see also citations in there)
Related to term algebras.
Combines term algebras with products.
Extends term algebras with ordering that is used in paramodulation provers.
Products of Structures admiting QE
- 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:
Example: Consider logic that quantifies over pairs of integers and where addition is given by
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
where are positive integers and is multiplication.
Consider prime factor representation of integers:
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 ,
Observe that this also subsumes Presburger arithmetic.
- Wilfrid Hodges: Model Theory