Introduction to Logic

Exercise 12.3 - Resolution Principle

In each of the following questions, say which of the answers best characterizes a result of applying resolution to the clauses shown.

1.{p(x,f(x)), q(x)} and {¬p(a,y), r(y)} 
  {q(x), r(y)} 
  {q(a), r(f(x))} 
  {q(a), r(f(a))} 
  There are no resolvents. 
 
2.{p(x,b), q(x)} and {¬p(a,x), r(x)} 
  {q(x), r(y)} 
  {q(b), r(a)} 
  {q(a), r(b)} 
  There are no resolvents. 
 
3.{p(x), p(a), q(x)} and {¬p(y), r(y)} 
  {p(x), q(x), r(x)}
  {p(a), q(x), r(x)}
  {p(a), q(a), r(a)}
  There are no resolvents.
 
4.{p(x), p(a), q(x)} and {¬p(y), r(y)} 
  {q(x), r(x)}
  {q(x), r(a)}
  {q(a), r(a)}
  There are no resolvents.
 
5.{p(a), q(y)} and {¬p(x), ¬q(b)} 
  {q(b), ¬q(b)}
  {q(y), ¬q(b)}
  {}
  There are no resolvents.
 
6.{p(x), q(x,x)} and {¬q(a, f(a))} 
  {p(a)}
  {p(f(a))}
  {p(a), p(f(a))}
  There are no resolvents.