LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:applications_of_quantifier_elimination [2010/02/22 11:30]
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 
-\[ 
-    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:​** ​ 
-  * 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 useful when there is qe? 
-  * to an extent, qe does show quantifiers are not necessary 
-  * $F'$ can be (more than) exponentially larger than $F$ 
-  * sometimes quantifiers naturally come up when encoding the problem 
- 
- 
- 
-===== Quantifier Elimination in Relation Composition ===== 
- 
-What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? 
- 
-++++|  The class given by 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)$ ​ 
- 
-{{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, 
-\[ 
-   {\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]] 
-  * [[:Harrison textbook]]