Automated Reasoning II

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

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

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

  ∀X ∃Y ( r(Y) <= ( ∀X ∃T q(Y,X,T) => p(X,Y) ) )
  ∀X ∃Y ( r(Y) <= ( ∀X1 ∃T q(Y,X1,T) => p(X,Y) ) )
  ∀X ∃Y ( r(Y) | ~ ( ~ ∀X1 ∃T q(Y,X1,T) | p(X,Y) ) )
  ∀X ∃Y ( r(Y) | ( ∀X1 ∃T q(Y,X1,T) & ~p(X,Y) ) )
  ∀X ∃Y ∀X1 ∃T ( r(Y) | ( q(Y,X1,T) & ~p(X,Y) ) )
  ( r(y(X)) | ( q(y(X),X1,t(X,X1)) & ~p(X,y(X)) ) )
  r(y(X)) | q(y(X),X1,t(X,X1))
  r(y(X)) | ~p(X,y(X))
  

  Doing some resolutions ...

• List all the resolvants of the following two clauses:

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

  First rename X in the second clause to X1, to avoid confusion. Then ...

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

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

  p(a) | q(X)    + ~p(Y) | q(f(Y))   = q(X) | q(f(a))
  p(a) | ~q(T)   + ~p(A) | ~q(W)     = ~q(T) | ~q(W)
  q(X) | q(f(a)) + ~q(T) | ~q(W)     = FALSE