Introduction to Logic

Use resolution to show that the clauses {¬p(x,y), q(x,y,f(x,y))}, {¬r(y,z), q(a,y,z)}, {r(y,z), ¬q(a,y,z)}, {p(x,g(x)), q(x,g(x),z)}, and {¬r(x,y), ¬q(x,w,z)} are unsatisfiable. This one is a little tricky. Be careful about factoring.

Show Instructions
Resolution
Goal  Incomplete