LARA

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

\begin{equation*} \alpha(f)(t_1,\ldots,t_n) = \end{equation*}

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))) \end{equation*}

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))) \end{equation*}

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:

  • 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

\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

$(\mathbb{Z}_{+},\cdot)$ where $\mathbb{Z}_{+}$ are positive integers and $\cdot$ is multiplication.

Consider prime factor representation of integers:

\begin{equation*} 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$.

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}$,

\begin{equation*} \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \} \end{equation*}

Observe that this also subsumes Presburger arithmetic.

References