Applications of Quantifier Elimination

Quantifier elimination works by eliminating quantifiers and produces an equivalent formula.

Example: By eliminating quantifier over $x$ from the formula

$\begin{equation*} \exists x. x \ge 0 \land x + y = z \end{equation*}$

we obtain formula

$\begin{equation*} y \le z \end{equation*}$

Example: By eliminating all quantifiers from the formula

$\begin{equation*} \forall x. \forall y. (x \le y \rightarrow (x+1 \le y+1)) \end{equation*}$

we obtain the formula 'true'.

Example: By eliminating quantifier $\forall D$ from the formula

$\begin{equation*} \begin{array}{l} (\forall D. A \subseteq D \land B \subseteq D\ \rightarrow\ C \subseteq D) \end{array} \end{equation*}$

we obtain formula

$\begin{equation*} C \subseteq A \cup B \end{equation*}$

We review several uses of quantifier elimination.

Deciding Formula Validity and Satisfiability using Quantifier Elimination

Quantified formulas:

eliminate quantifiers
obtain ground formula
evaluate ground formula

Satisfiability:

add existential quantifiers
check the resulting quantified formula

Validity:

Check satisfiability of negation

Often we have better algorithms for quantifier-free fragments.

In such cases, we stop when we obtain formulas that has only existential quantifiers.

for quantified formula the goal becomes to remove all quantifiers except for innermost existential quantifiers

The Purpose of Quantifiers

Suppose we want to describe a set of states of an integer program manipulating varibles $x,y$ . We describe it by a formula $F(x,y)$ in theory admitting QE.

$\begin{equation*} S = \{ (x,y) \mid F(x,y) \} \end{equation*}$

Then there is equivalent formula $F'(x,y)$ that contains no quantifiers, so it defines same set of states:

$\begin{equation*} S = \{ (x,y) \mid F'(x,y) \} \end{equation*}$

Are quantifiers useful when there is qe?

to an extent, qe does show quantifiers are not necessary
$F'$ can be (more than) exponentially larger than $F$
sometimes quantifiers naturally come up when encoding the problem

Quantifier Elimination in Relation Composition

What class of relations is defined by integer programs without loops in the syntax of Simple Programming Language ?

The class given by formulas in Presburger arithmetic.

Assignment:

Havoc:

Assume:

Non-deterministic choice:

Relation composition:

What does quantifier elimination tell us about representations of such formulas?

Quantifier Elimination for Optimization

We considered validity and satisfiability problems, which produce solutions or proofs.

Optimization problems try to find a maximum or minimum of some function, subject to given constraints.

problem 1 in this homework shows how to (in principle) use quantifier elimination for optimization.

Example reference:

Simulation and Optimization by Quantifier Elimination

Interpolation

Definition of Interpolant: Given two formulas $F$ and $G$ , such that $\models F \rightarrow G$ , an interpolant for $(F,G)$ is a formula $H$ such that:
1) $\models F \rightarrow H$
2) $\models H \rightarrow G$
3) $FV(H)\subseteq FV(F) \cap FV(G)$

Paper on Interpolation in Verification

Here are two simple ways to construct an interpolant:

We can quantify existentially all variables in $F$ that are not in $G$ .

$H_{min} \equiv elim(\exists p_1, p_2, ..., p_n.\ F)$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$

We can quantify universally all variables in $G$ that are not in $F$ .

$H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$

Definition: ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$ , that is,

$\begin{equation*} {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} \end{equation*}$

Theorem: The following properties hold for $H_{min}$ , $H_{max}$ , ${\cal I}(F,G)$ defined above:

$H_{min} \in {\cal I}(F,G)$
$\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$
$H_{max} \in {\cal I}(F,G)$
$\forall H \in {\cal I}(F,G).\ \models (H \rightarrow H_{max})$

We have observed before that, if a theory has quantifier elimination, then it also has interpolants.

Therefore, all theories in the List of Theories Admitting QE have interpolants. (But interpolants may exist even if there is no quantifier elimination.)

LARA