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 [2009/04/22 18:52] vkuncak |
sav08:applications_of_quantifier_elimination [2012/03/06 15:44] vkuncak |
||
|---|---|---|---|
| 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 | ||
| + | \[ | ||
| + | \exists x. x \ge 0 \land x + y = z | ||
| + | \] | ||
| + | we obtain formula | ||
| + | \[ | ||
| + | y \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:** | **Quantified formulas:** | ||
| Line 22: | Line 53: | ||
| - | ===== Do we need quantifiers when there is QE? ===== | + | |
| + | |||
| + | ===== 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. | ||
| Line 32: | Line 65: | ||
| S = \{ (x,y) \mid F'(x,y) \} | S = \{ (x,y) \mid F'(x,y) \} | ||
| \] | \] | ||
| - | 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 41: | 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 63: | 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. | ||
| - | This [[Homework08|homework problem 1]] shows how to (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: | ||
| * [[http://dx.doi.org/10.1006/jsco.1997.0122|Simulation and Optimization by Quantifier Elimination]] | * [[http://dx.doi.org/10.1006/jsco.1997.0122|Simulation and Optimization by Quantifier Elimination]] | ||
| - | |||
| - | |||
| ===== Interpolation ===== | ===== Interpolation ===== | ||
| Line 78: | Line 111: | ||
| 3) $FV(H)\subseteq FV(F) \cap FV(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:** | Here are two **simple ways to construct an interpolant:** | ||
| Line 107: | 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]] | ||