LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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: