• English only

# Differences

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

 sav08:homework11 [2008/05/08 18:54]vkuncak sav08:homework11 [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/15 12:58 vkuncak 2008/05/08 18:54 vkuncak 2008/05/08 18:51 vkuncak 2008/05/08 18:50 vkuncak 2008/05/08 18:50 vkuncak created Next revision Previous revision 2008/05/15 12:58 vkuncak 2008/05/08 18:54 vkuncak 2008/05/08 18:51 vkuncak 2008/05/08 18:50 vkuncak 2008/05/08 18:50 vkuncak created Line 30: Line 30: ===== Problem 2 ===== ===== Problem 2 ===== - Suppose you are given a set of predicates ${\cap P} = \{P_0,​P_1,​\ldots,​P_n\}$ in a decidable theory of first-order logic (for example, combination of uninterpreted function symbols with integer linear arithmetic) where $P_0$ is the predicate '​false'​.  ​ + Suppose you are given a set of predicates ${\cap P} = \{P_0,​P_1,​\ldots,​P_n\}$ in a decidable theory of first-order logic (for example, ​quantifier-free formulas in the combination of uninterpreted function symbols with integer linear arithmetic) where $P_0$ is the predicate '​false'​.  ​ **Part a)** Consider [[Conjunctions of Predicates]] as abstract interpretation domain. ​ Give example showing that it need not be the case that **Part a)** Consider [[Conjunctions of Predicates]] as abstract interpretation domain. ​ Give example showing that it need not be the case that - $+ \begin{equation*} a_1 \leq a_2 \leftrightarrow \gamma(a_1) \subseteq \gamma(a_2) a_1 \leq a_2 \leftrightarrow \gamma(a_1) \subseteq \gamma(a_2) -$ + \end{equation*} **Part b)** Describe how to construct from $A$ a new, smaller, lattice $B$, where the above equivalence holds. ​ Is there an algorithm to compute $B$ and the partial order on $B$ using a decision procedure for the logic of predicates? **Part b)** Describe how to construct from $A$ a new, smaller, lattice $B$, where the above equivalence holds. ​ Is there an algorithm to compute $B$ and the partial order on $B$ using a decision procedure for the logic of predicates?