Lab for Automated Reasoning and Analysis 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:
 
sav08/applications_of_quantifier_elimination.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice