Automated Reasoning II

• ∀X ∀Y ( ∀Z ( p(X,Y) | q(X,Z) ) => ∃T ( p(X,T) & q(Y,T) & r(X,Y) ) )

• ∀X ∃Y ( r(Y) <= ( ∀X ∃T q(Y,X,T) => p(X,Y) ) )

Doing some resolutions ...

• List all the resolvants of the following two clauses:

  p(X) | p(f(Y)) | q(X,Y)
  
  ~p(f(a)) | ~p(Z) | ~q(c,d) 

• Use resolution to derive the empty clause from the set

  S = { p(a) | q(X),
        ~p(Y) | q(f(Y)),
        p(a) | ~q(T),
        ~p(A) | ~q(W) }