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)
|
|