This is an old revision of the document!
Applications 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.
In Homework08 you explore how you can (in principle) use quantifier elimination for optimization.
Example reference:
Interpolation
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.)