Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:applications_of_quantifier_elimination [2009/04/22 23:26] vkuncak |
sav08:applications_of_quantifier_elimination [2009/04/24 10:09] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
we obtain formula | we obtain formula | ||
\[ | \[ | ||
- | x \le z | + | y \le z |
\] | \] | ||
Line 30: | Line 30: | ||
\] | \] | ||
- | ===== Deciding Formulas ===== | + | We review several uses of quantifier elimination. |
+ | |||
+ | ===== Deciding Formula Validity and Satisfiability using Quantifier Elimination ===== | ||
**Quantified formulas:** | **Quantified formulas:** | ||
Line 51: | 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 61: | 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 70: | 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 96: | Line 102: | ||
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]] | ||
+ | |||
Line 107: | Line 114: | ||
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 136: | Line 144: | ||
* [[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]] | ||
+ | * [[http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521899574|Harrison textbook]] |