• Home
  • Textbooks
  • Decision Procedures: An Algorithmic Point of View
  • Deciding a Combination of Theories

Decision Procedures: An Algorithmic Point of View

Daniel Kroening, Ofer Strichman

Chapter 10

Deciding a Combination of Theories - all with Video Answers

Educators

Chapter Questions

Problem 1

Prove that the following formula is unsatisfiable using the Nelson-Oppen procedure, where the variables are interpreted over the integers:

$$
g\left(f\left(x_1-2\right)\right)=x_1+2 \wedge g\left(f\left(x_2\right)\right)=x_2-2 \wedge\left(x_2+1=x_1-1\right) .
$$

Check back soon!

Problem 2

A simple improvement to Algorithm 10.3.1 is to restrict the propagation of equalities in step 3 as follows. We call a variable local if it appears only in a single theory. Then, if an equality $v_i=v_j$ is implied by $F_i$ and not by $F_j$, we propagate it to $F_j$ only if $v_i, v_j$ are not local to $F_i$. Prove the correctness of this improvement.

Check back soon!

Problem 3

Prove the correctness of Algorithm 10.3.2 by generalizing the proof of Algorithm 10.3.1 given in Sect. 10.3.3.

Check back soon!