Quantified formulas:

• eliminate quantifiers
• obtain ground formula
• evaluate ground formula

Satisfiability:

• add existential quantifiers
• check the resulting quantified formula

Validity:

• Check satisfiability of negation

Reduction to satisfiability:

• often we have better algorithms for quantifier-free fragments
• then for quantified formula we just reduce remove “quantifier alternations” (obtain only one block of existential quantifiers)

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

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?

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:

• Simulation and Optimization by Quantifier Elimination

We have observed before that, if a theory has 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.)

• A New Approach for Automatic Theorem Proving in Real Geometry