Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:applications_of_quantifier_elimination [2008/04/16 22:44] vkuncak |
sav08:applications_of_quantifier_elimination [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Applications of Quantifier Elimination ====== | ====== Applications of Quantifier Elimination ====== | ||
- | ===== Deciding Formulas ===== | + | 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:** | **Quantified formulas:** | ||
Line 15: | Line 46: | ||
* Check satisfiability of negation | * 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) | ||
- | ===== Do we need quantifiers? ===== | + | 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. | 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) | + | 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: | 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) \} | S = \{ (x,y) \mid F'(x,y) \} | ||
- | \] | + | \end{equation*} |
- | Are quantifiers useless? | + | Are quantifiers useful when there is qe? |
- | * to an extent | + | * to an extent, qe does show quantifiers are not necessary |
* $F'$ can be (more than) exponentially larger than $F$ | * $F'$ can be (more than) exponentially larger than $F$ | ||
- | * sometimes quantifiers are natural | + | * sometimes quantifiers naturally come up when encoding the problem |
+ | |||
===== Quantifier Elimination in Relation Composition ===== | ===== Quantifier Elimination in Relation Composition ===== | ||
Line 38: | Line 76: | ||
What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | ||
- | ++++| Formulas in Presburger arithmetic. | + | ++++| The class given by formulas in Presburger arithmetic. |
++++ | ++++ | ||
Line 52: | Line 90: | ||
What does quantifier elimination tell us about representations of such formulas? | What does quantifier elimination tell us about representations of such formulas? | ||
+ | |||
===== Quantifier Elimination for Optimization ===== | ===== Quantifier Elimination for Optimization ===== | ||
Line 59: | Line 98: | ||
//Optimization problems// try to find a maximum or minimum of some function, subject to given constraints. | //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. | + | [[Homework08|problem 1]] in this homework shows how to (in principle) use quantifier elimination for optimization. |
Example reference: | Example reference: | ||
Line 66: | Line 105: | ||
===== Interpolation ===== | ===== Interpolation ===== | ||
- | We have observed before that, if a theory has has quantifier elimination, then it also has interpolants. | + | **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)$ | ||
+ | |||
+ | {{sav08:mcmillaninterpolation.pdf|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.) | Therefore, all theories in the [[List of Theories Admitting QE]] have interpolants. (But interpolants may exist even if there is no quantifier elimination.) | ||
Line 73: | Line 141: | ||
* [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]] | * [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]] | ||
+ | * [[:Harrison textbook]] | ||