• 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) Both sides previous revision Previous revision 2012/03/06 15:44 vkuncak 2010/02/22 11:30 vkuncak 2009/04/24 10:09 vkuncak 2009/04/23 14:16 vkuncak 2009/04/22 23:51 vkuncak 2009/04/22 23:50 vkuncak 2009/04/22 23:34 vkuncak 2009/04/22 23:27 vkuncak 2009/04/22 23:27 vkuncak 2009/04/22 23:26 vkuncak 2009/04/22 23:26 vkuncak 2009/04/22 18:52 vkuncak 2009/04/22 18:50 vkuncak 2008/04/18 18:35 pedagand 2008/04/17 18:24 pedagand 2008/04/17 12:14 vkuncak 2008/04/16 22:44 vkuncak 2008/04/16 22:44 vkuncak 2008/04/16 22:31 vkuncak 2008/04/16 22:26 vkuncak 2008/04/16 22:26 vkuncak 2008/04/16 10:04 vkuncak 2008/04/16 10:03 vkuncak created Next revision Previous revision 2012/03/06 15:44 vkuncak 2010/02/22 11:30 vkuncak 2009/04/24 10:09 vkuncak 2009/04/23 14:16 vkuncak 2009/04/22 23:51 vkuncak 2009/04/22 23:50 vkuncak 2009/04/22 23:34 vkuncak 2009/04/22 23:27 vkuncak 2009/04/22 23:27 vkuncak 2009/04/22 23:26 vkuncak 2009/04/22 23:26 vkuncak 2009/04/22 18:52 vkuncak 2009/04/22 18:50 vkuncak 2008/04/18 18:35 pedagand 2008/04/17 18:24 pedagand 2008/04/17 12:14 vkuncak 2008/04/16 22:44 vkuncak 2008/04/16 22:44 vkuncak 2008/04/16 22:31 vkuncak 2008/04/16 22:26 vkuncak 2008/04/16 22:26 vkuncak 2008/04/16 10:04 vkuncak 2008/04/16 10:03 vkuncak created 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: