%---------------------------------------------------------------------%
%   Clausal resolution                                                %
%   (C) 1998 Zdravko Markov                                           %
%---------------------------------------------------------------------%

% Examples

:- dynamic cl/2.

cl([woman(s(X))],[man(X)]).              % man(X) <- woman(s(X)). 
cl([loves(X,s(X))],[man(X)]).            % man(X) <- loves(X,s(X))
cl([man(john)],[]).                      % man(john) <-
cl([],[loves(john,_)]).                  % <- loves(john,X)

cl([lost(driver)],[]).                   % lost(driver) <- 
cl([get_out(X)],[use_phone(X)]).         % get_out(X) <- use_phone(X)
cl([get_out(X)],[use_map(X)]).           % get_out(X) <- use_map(X)
cl([use_map(X),use_phone(X)],[lost(X)]). % use_map(X);use_phone(X) <- lost(X)
cl([],[get_out(driver)]).

%---------------------------------------------------------------------%
resolve :-
    resolvent(C),                   % Find a resolvent
    write('Derived: '),             % print it out
    write(C), nl,                   % and
    resolve.                        % continue until no more 
resolve.                            % resolvents can be derived

resolvent(cl(P,N)) :-
    new_resolvent(P,N),             % Find a new resolvent.
    \+ cl(P,N),                     % If not already derived
    assertz(cl(P,N)).               % assert it in the database

new_resolvent(P,N) :-
    cl(P1,N1),                      % Retrieve clauses: P1<-N1
    cl(P2,N2),                      % and P2<-N2.
    del(L,P1,P3),                   % P3 = P1\{L}
    del(L,N2,N3),                   % N3 = N2\{L}
    append1(P2,P3,P),               % P = P2 U P3
    append1(N1,N3,N),               % N = N1 U N3
    \+ ((member(X,P),member(X,N))). % Remove tautologies

append1([],L,L) :- !.
append1([H|T],L,[H|V]) :-
    \+ member(H,L), !,
    append1(T,L,V).
append1([_|T],L,V) :-
    append1(T,L,V).

del(X,[X|T],T).
del(X,[Y|T],[Y|V]) :-
    del(X,T,V).

member(X,[X|_]).
member(X,[_|T]) :-
    member(X,T).

