• English only

# Differences

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

sav08:applications_of_quantifier_elimination [2010/02/22 11:30]
vkuncak
sav08:applications_of_quantifier_elimination [2015/04/21 17:30] (current)
Line 4: Line 4:

**Example:​** By eliminating quantifier over $x$ from the formula **Example:​** By eliminating quantifier over $x$ from the formula
-$+\begin{equation*} \exists x. x \ge 0 \land x + y = z \exists x. x \ge 0 \land x + y = z -$+\end{equation*}
we obtain formula we obtain formula
-$+\begin{equation*} y \le z y \le z -$+\end{equation*}

**Example:​** By eliminating all quantifiers from the formula **Example:​** By eliminating all quantifiers from the formula
-$+\begin{equation*} \forall x. \forall y. (x \le y \rightarrow (x+1 \le y+1)) \forall x. \forall y. (x \le y \rightarrow (x+1 \le y+1)) -$+\end{equation*}
we obtain the formula '​true'​. we obtain the formula '​true'​.

**Example:​** By eliminating quantifier $\forall D$ from the formula **Example:​** By eliminating quantifier $\forall D$ from the formula
-$+\begin{equation*} \begin{array}{l} \begin{array}{l} (\forall D. (\forall D. A \subseteq D \land B \subseteq D\ \rightarrow\ C \subseteq D) A \subseteq D \land B \subseteq D\ \rightarrow\ C \subseteq D) \end{array} \end{array} -$+\end{equation*}
we obtain formula we obtain formula
-$+\begin{equation*} C \subseteq A \cup B C \subseteq A \cup B -$+\end{equation*}

We review several uses of quantifier elimination. We review several uses of quantifier elimination.
Line 58: Line 58:

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.
-$+\begin{equation*} S = \{ (x,y) \mid F(x,y) \} 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: 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) \} S = \{ (x,y) \mid F'​(x,​y) \} -$+\end{equation*}
Are quantifiers useful when there is qe? Are quantifiers useful when there is qe?
* to an extent, qe does show quantifiers are not necessary   * to an extent, qe does show quantifiers are not necessary
Line 98: 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 126: Line 123:

**Definition:​** ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, **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) \} {\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: **Theorem:​** The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above: