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