LARA

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 $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.

Feature Trees

Term Powers

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

$(\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!

The Field of Complex and Real Numbers

Over complex numbers, we get decidability for both multiplication and addition - theory of polynomials.

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.

References