Differences

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

--- sav08:applications_of_quantifier_elimination [2008/04/18 18:35]
pedagand
+++ sav08:applications_of_quantifier_elimination [2015/04/21 17:30] (current)
@@ Line 1: / Line 1: @@
 ====== 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:**
@@ 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.
-\[
+\begin{equation*}
     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:
-\[
+\begin{equation*}
     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$
-  * sometimes quantifiers are natural
+  * sometimes quantifiers naturally come up when encoding the problem
 ===== 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]] ?
-++++|  Formulas in Presburger arithmetic.
+++++|  The class given by formulas in Presburger arithmetic.
 ++++
@@ Line 55: / Line 90: @@
 What does quantifier elimination tell us about representations of such formulas?
 ===== Quantifier Elimination for Optimization =====
@@ Line 62: / Line 98: @@
 //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:
   * [[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: \\
+) $\models F \rightarrow H$ \\
+) $\models H \rightarrow G$ \\
+) $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.
@@ Line 77: / Line 141: @@
   * [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]]
+  * [[:Harrison textbook]]