/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   Written by Markus Triska, triska@gmx.at, Sept. 5th 2006
   Public domain code.
   ----------------------------------------------------------------------

   Resolution calculus for propositional logic.

   Input is a formula in conjunctive normal form, represented as a
   list of clauses; clauses are lists of atoms and terms not/1.

   Example:

   ?- Clauses = [[p,not(q)], [not(p),not(s)], [s,not(q)], [q]],
      pl_resolution(Clauses, R).

   R = [ ([[p, not(q)], [not(p), not(s)]]-->[not(q), not(s)]),
         ([[s, not(q)], [not(q), not(s)]]-->[not(q)]),
         ([[q],[not(q)]]-->[])] ;

   Iterative deepening is used to find a shortest refutation.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */


pl_resolution(Clauses0, Chain) :-
	maplist(sort, Clauses0, Clauses), % remove duplicates
	length(Chain, _),
	pl_derive_empty_clause(Chain, Clauses).

pl_derive_empty_clause([], Clauses) :- memberchk([], Clauses).
pl_derive_empty_clause([C|Cs], Clauses) :-
	pl_resolvent(C, Clauses, R),
	pl_derive_empty_clause(Cs, [R|Clauses]).

pl_resolvent([C1,C2] --> R, Clauses, R) :-
	member(C1, Clauses),
	member(C2, Clauses),
	select(Q, C1, C1Rest),
	select(not(Q), C2, C2Rest),
	append(C1Rest, C2Rest, R0),
	sort(R0, R), % remove duplicates
	\+ memberchk(R, Clauses).