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)