Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:applications_of_quantifier_elimination [2009/04/22 23:50] 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*} |
- | x \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 | ||
* $F'$ can be (more than) exponentially larger than $F$ | * $F'$ can be (more than) exponentially larger than $F$ | ||
* sometimes quantifiers naturally come up when encoding the problem | * sometimes quantifiers naturally come up when encoding the problem | ||
+ | |||
Line 75: | Line 76: | ||
What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | ||
- | ++++| Formulas in Presburger arithmetic. | + | ++++| The class given by formulas in Presburger arithmetic. |
++++ | ++++ | ||
Line 97: | 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 125: | 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: | ||
Line 143: | Line 141: | ||
* [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]] | * [[http://www.springerlink.com/content/n674875430157r80/|A New Approach for Automatic Theorem Proving in Real Geometry]] | ||
+ | * [[:Harrison textbook]] | ||