Differences
This shows you the differences between two versions of the page.
sav08:applications_of_quantifier_elimination [2009/04/22 23:27] vkuncak |
sav08:applications_of_quantifier_elimination [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Applications of Quantifier Elimination ====== | ||
- | |||
- | Quantifier elimination works by eliminating quantifiers and produces an equivalent formula. | ||
- | |||
- | **Example:** By eliminating quantifier over $x$ 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 $\forall D$ 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 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. | ||
- | \[ | ||
- | S = \{ (x,y) \mid F(x,y) \} | ||
- | \] | ||
- | Then there is equivalent formula $F'(x,y)$ that contains no quantifiers, so it defines same set of states: | ||
- | \[ | ||
- | S = \{ (x,y) \mid F'(x,y) \} | ||
- | \] | ||
- | Are quantifiers useless? | ||
- | * to an extent | ||
- | * $F'$ can be (more than) exponentially larger than $F$ | ||
- | * 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]] ? | ||
- | |||
- | ++++| 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. | ||
- | |||
- | This [[Homework08|homework problem 1]] shows how to (in principle) use quantifier elimination for optimization. | ||
- | |||
- | Example reference: | ||
- | * [[http://dx.doi.org/10.1006/jsco.1997.0122|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)$ | ||
- | |||
- | |||
- | 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, | ||
- | \[ | ||
- | {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} | ||
- | \] | ||
- | |||
- | **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.) | ||
- | |||
- | ===== Reasoning in Geometry ===== | ||
- | |||
- | * [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]] | ||