1 Prove the following using resolution: (a) (A ! B) ^ (B ! C) ^ :(A ! C) j= ?
(b) (A _ B _ C) ^ (:B _ D) ^ (:A _ D) ^ (:C _ D) j= D
(c) A ! B; B ! C; D ! C; C _ D j= :A _ C
2 Which of the following sets are inconsistent? (a) ffp1; p2; p3g; fp1; :p3g; f:p1; :p2gg (b) ffp1; :p2; p3g; fp1; :p3g; fp1; p2gg
5 For each of the following set of clauses S, write down the Herbrand domain H, the Herbrand base HB, and two interpretations, one that satisfies S and one that does not. (a) S = ffA(x); :B(y; x)g; f:A(y); C(c)gg
(b) S = ffA(f(x)); :B(y; x)g; f:A(c); C(x)gg
6 Show, using Herbrand interpretations, that the following set of clauses is unsatisfiable. (a) S = ffA(x); :B(x; a)g; fA(a); B(y; a)g; f:A(y)gg
