- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:homework08 [2008/09/15 15:56] vkuncak |
sav08:homework08 [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 6: | Line 6: | ||

Consider a language $L$ that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language). Consider formulas interpreted over some theory $T$ that has an effective quantifier elimination algorithm $qe$. Then show that there is an algorithm for solving optimization problems such as | Consider a language $L$ that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language). Consider formulas interpreted over some theory $T$ that has an effective quantifier elimination algorithm $qe$. Then show that there is an algorithm for solving optimization problems such as | ||

- | \[ | + | \begin{equation*} |

\max \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \} | \max \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \} | ||

- | \] | + | \end{equation*} |

where $t(x_1,\ldots,x_n)$ denotes a term of the language whose value is an integer, and where $F(x_1,\ldots,x_n)$ is an arbitrary formula in language $L$. The meaning of //solution// for constraints is the following. Let $S = \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \}$. Then the solution is an element $y^*$ of $\mathbb{Z} \cup \{-\infty,+\ifnty\}$ such that | where $t(x_1,\ldots,x_n)$ denotes a term of the language whose value is an integer, and where $F(x_1,\ldots,x_n)$ is an arbitrary formula in language $L$. The meaning of //solution// for constraints is the following. Let $S = \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \}$. Then the solution is an element $y^*$ of $\mathbb{Z} \cup \{-\infty,+\ifnty\}$ such that | ||

* if $y^* = -\infty$ then $S=\emptyset$ | * if $y^* = -\infty$ then $S=\emptyset$ | ||

Line 15: | Line 15: | ||

Your answer will show, given $qe$, how to solve optimization problems for any theory that has quantifier elimination. For example, taking Presburger arithmetic, we can solve linear optimization problems such as | Your answer will show, given $qe$, how to solve optimization problems for any theory that has quantifier elimination. For example, taking Presburger arithmetic, we can solve linear optimization problems such as | ||

- | \[ | + | \begin{equation*} |

\max \{ 2x + 3y \mid x + y \le 10 \land (7 \mid y+1) \} | \max \{ 2x + 3y \mid x + y \le 10 \land (7 \mid y+1) \} | ||

- | \] | + | \end{equation*} |

Taking BAPA as a theory with QE, we can solve problems such as finding | Taking BAPA as a theory with QE, we can solve problems such as finding | ||

- | \[ | + | \begin{equation*} |

\max \{ |A|+3|B|+|C|\ \mid\ C \subseteq A \cup B \land |A| \le |B| \land |C| \le 100 \} | \max \{ |A|+3|B|+|C|\ \mid\ C \subseteq A \cup B \land |A| \le |B| \land |C| \le 100 \} | ||

- | \] | + | \end{equation*} |

By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals. | By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals. | ||

Line 28: | Line 28: | ||

Consider language ${\cal L} = \{ {\le} \}$ and the theory $T = Conseq(T_0)$ where $T_0$ is the set of following axioms (axioms of linear order): | Consider language ${\cal L} = \{ {\le} \}$ and the theory $T = Conseq(T_0)$ where $T_0$ is the set of following axioms (axioms of linear order): | ||

- | \[ | + | \begin{equation*} |

\begin{array}{l} | \begin{array}{l} | ||

\forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\ | \forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\ | ||

Line 34: | Line 34: | ||

\forall x.\forall y. x \le y \lor y \le x | \forall x.\forall y. x \le y \lor y \le x | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where $\le$ is interpreted as the usual less-than-equal relation on such numbers. | Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where $\le$ is interpreted as the usual less-than-equal relation on such numbers. | ||

Line 42: | Line 42: | ||

Solution (added afterwards): | Solution (added afterwards): | ||

- | * {{sav08:laeuchlileonard66linearorder.pdf|Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}} (Thanks to Yuri Gurevich, who also mentions that result follows from decidability of S2S) | + | * {{sav08:laeuchlileonard66linearorder.pdf|Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}} |

- | * [[http://www.jstor.org/sici?sici=0022-4812%28196806%2933%3A2%3C287%3AOTETOL%3E2%2E0%2ECO%3B2-I&origin=euclid|review]], {{sav08:review-linearorder.pdf|review pdf}} | + | * {{sav08:rabin69s2s.pdf|Decidability of Second-Order Theories and Automata on Infinite Trees, by Michael O. Rabin}} |

Somewhat related papers: | Somewhat related papers: |