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:34] 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 69: | Line 69: | ||
| * $F'$ can be (more than) exponentially larger than $F$ | * $F'$ can be (more than) exponentially larger than $F$ | ||
| * sometimes quantifiers naturally come up when encoding the problem | * sometimes quantifiers naturally come up when encoding the problem | ||
| + | |||
| Line 75: | 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 101: | 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 112: | 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 141: | 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]] | ||