/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Written 2006-2020 by Markus Triska, triska@metalevel.at Public domain code. Tested with Scryer Prolog. ---------------------------------------------------------------------- Resolution calculus for propositional logic. For more information about theorem proving with Prolog, see: https://www.metalevel.at/prolog/theoremproving ============================================== Input is a formula in conjunctive normal form, represented as a list of clauses; clauses are lists of atoms and terms not/1. Examples: ?- Clauses = [[p], [q]], pl_resolution(Clauses, Rs). %@ false. ?- Clauses = [[p,not(q)], [not(p),not(s)], [s,not(q)], [q]], pl_resolution(Clauses, Rs), maplist(portray_clause, Rs). %@ [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. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ :- use_module(library(dcgs)). :- use_module(library(dif)). :- use_module(library(lists)). :- use_module(library(format)). pl_resolution(Clauses0, Chain) :- maplist(sort, Clauses0, Clauses), % remove duplicates iterative_deepening([], Chain, Clauses). iterative_deepening(Limit, Chain, Clauses0) :- ( same_length(Ts, Limit), phrase(pl_chain(Clauses0, _), Ts) -> ( same_length(Chain, Limit), phrase(pl_chain(Clauses0, Clauses), Chain), member([], Clauses) -> true ; iterative_deepening([_|Limit], Chain, Clauses0) ) ; false ). pl_chain(Cs, Cs) --> []. pl_chain(Cs0, Cs) --> [Step], { pl_resolvent(Step, Cs0, Rs) }, pl_chain([Rs|Cs0], Cs). pl_resolvent(((As0-Bs0) --> Rs), Clauses, Rs) :- member(As0, Clauses), member(Bs0, Clauses), select(Q, As0, As), select(not(Q), Bs0, Bs), append(As, Bs, Rs0), sort(Rs0, Rs), % remove duplicates maplist(dif(Rs), Clauses).