Assignment 7 
60 points


1. [30 points] Problem 5.4(b). Follow algorithm SAT on slide 13-24. (Ignore the discussion on 
   terminal MSCS -- slides 13-32 to 13-36 -- that was not covered in class.)

Follow these steps:
 (i) List the formulas in the closure of phi.
 (ii) List the basic formulas.
 (iii) List the atoms.
 (iv) Generate the tableau Tphi.  DO THIS STEP BEFORE (v).
 (v) Generate T(minus)phi by removing all atoms from Tphi that are not reachable from phi-atoms.
 (vi) Mark the MSCS in the tableau of (v). 
     Say which (if any) are transient.
 (vii) Is phi satisfiable? If yes, indicate a fulfilling 
     phi-reachable MSCS. If no, say for each phi-reachable 
     MSCS (if any) why it is not fulfilling.

2. [30 points] Problem 5.4 (c).  Answer the same parts (i)-(vii) as above.