- English only

# Lab for Automated Reasoning and Analysis LARA

# 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: |