%
%  Resolution procedure for the propositional calculus
%

user:file_search_path(common,'../common').
:- ensure_loaded(common(cnf)).
:- ensure_loaded(common(io)).

%
%  resolve(S) - resolve the set of clauses S.
%

resolve([]) :-
  write('The empty set of clauses is valid.').

resolve(S) :-
  member([], S),
  write_clauses(S), nl,
  write('The empty clause is in the set of clauses so it is unsatisfiable.').

resolve(S) :-
  member(C1, S),              % choose two clauses
  member(C2, S),
  clashing(C1, L1, C2, L2),   % check that they clash
  delete(C1, L1, C1P),        % delete the clashing literals
  delete(C2, L2, C2P),
  union(C1P, C2P, C),         % new clause is their union
                              % do not add:
  \+ clashing(C, _, C, _),    % a clause that clashes with itself (valid)
  \+ member(C, S),            % a clause that already exists

  write_clauses(S), nl,
  resolve([C | S]).           % add the resolvent to the set

resolve(_) :-
  write('The set of clauses is not unsatisfiable.').

clashing(C1, L, C2, neg L) :-
  member(L, C1),
  member(neg L, C2), !.
clashing(C1, neg L, C2, L) :-
  member(neg L, C1),
  member(L, C2),  !.