Lecture 2:
  • slide 45: Distribute disjunctions --> Distribute conjunctions
  • slide 49: \psi_{12} --> \phi_{12} in the body of Dist
  • slides 70 and 72: Add (1 -2) to \phi 
  • slide 72: the derivation of (1 3) is superfluous as (1 3) is already in \phi.

Lecture 3a:

  • slide 77: step 1 should be p implies q instead of p and q

Lecture 4:

  • slide 11: Resolution order --> Implication order (resolution order -- the order used for constructing a conflict clause is "reverse" of the implication order).

Lectrure 5a:

  • slide 16: For the BDD, f : (x1 \/ x2) \/ x3 to be read as (x1 \/ x2) /\ x3

Lecture 6:

  • slide 4: The signature should include '+' also.

Lecture 7:

  • slide 13: l --> d
  • slide 20: F(G(a) --> F(G(a))

Lecture 16:

  • slide 1: the formula for the first example should be ~a /\ [ ] (b \/ O ~a)