This is an old revision of the document!
Applications of Quantifier Elimination
Quantifier elimination works by eliminating quantifiers and produces an equivalent formula.
Example: By eliminating quantifier over from the formula \[
\exists x. x \ge 0 \land x + y = z
\] we obtain formula \[
x \le z
\]
Example: By eliminating all quantifiers from the formula \[
\forall x. \forall y. (x \le y \rightarrow (x+1 \le y+1))
\] we obtain the formula 'true'.
Example: By eliminating quantifier from the formula \[ \begin{array}{l}
(\forall D. A \subseteq D \land B \subseteq D\ \rightarrow\ C \subseteq D)
\end{array} \] we obtain formula \[
C \subseteq A \cup B
\]
We review several uses of quantifier elimination.
Deciding Formulas
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
Do we need quantifiers when there is QE?
Suppose we want to describe a set of states of an integer program manipulating varibles . We describe it by a formula in theory admitting QE. \[
S = \{ (x,y) \mid F(x,y) \}
\] Then there is equivalent formula that contains no quantifiers, so it defines same set of states: \[
S = \{ (x,y) \mid F'(x,y) \}
\] Are quantifiers useless?
- to an extent
- can be (more than) exponentially larger than
- sometimes quantifiers are natural
Quantifier Elimination in Relation Composition
What class of relations is defined by integer programs without loops in the syntax of Simple Programming Language ?
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.
This homework problem 1 shows how to (in principle) use quantifier elimination for optimization.
Example reference:
Interpolation
Definition of Interpolant:
Given two formulas and , such that , an interpolant for is a formula such that:
1)
2)
3)
Here are two simple ways to construct an interpolant:
- We can quantify existentially all variables in that are not in .
where
- We can quantify universally all variables in that are not in .
where
Definition: denote the set of all interpolants for , that is, \[
{\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \}
\]
Theorem: The following properties hold for , , defined above:
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.)