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:homework11 [2008/05/08 18:54]
vkuncak
sav08:homework11 [2015/04/21 17:30] (current)
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?
 
sav08/homework11.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice