flach@kub.nl (Peter Flach) (11/24/89)
I've implemented a resolution theorem prover for FULL First Order Predicate Logic, using (incomplete) input resolution and sound unification. Input resolution can be trivially changed to (complete) linear resolution, if desired. Also, factoring is omitted. Both depth-first and breadth-first versions are included. --Peter Peter A. Flach (flach@kub.nl) Institute for Language Technology UUCP: ..!mcvax!kubix!flach and Artificial Intelligence (ITK) BITNET: flach@htikub5 Tilburg University, PObox 90153 (+31) (13) 66 3119 5000 LE Tilburg, the Netherlands %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %%% %%% RESOLUTION THEOREM PROVER %%% %%% for FULL First Order Predicate Logic %%% %%% %%% %%% Author: Peter A. Flach %%% %%% Date: November 23, 1989 %%% %%% %%% %%% Inst. for Language Technology & AI %%% %%% Tilburg University, PObox 90153, %%% %%% 5000 LE Tilburg, the Netherlands %%% %%% %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% What follows is a Quintus Prolog implementation of a %%% resolution theorem prover for the full First Order %%% Predicate Logic. Included are both a depth-first %%% (refute_df/2) and a breadth-first (refute_bf/3) %%% version. %%% Both provers are sound, due to unification with %%% occur check. However, neither one of them is %%% refutation complete, due to %%% 1. Omission of factoring %%% 2. The use of input resolution, which is %%% complete for Horn logic but incomplete %%% in general. %%% Of course, the breadth-first version is somewhat %%% `less incomplete' than the depth-first version %%% (and also less efficient). %%% Clauses assume the format (AtomList1 :- AtomList2), %%% where AtomList1 and AtomList2 are lists of Prolog %%% atoms. The axioms of the theory are assumed to be %%% given by the predicate cl/1. E.g., %%% cl(([mother(X,Y),father(X,Y)]:-[parent(X,Y)])). :- compile(library(basics)). :- compile(library(unify)). % refute_df(Clause,Proof) is true if Clause can be % refuted by resolution using depth-first search % from the clauses defined by the predicate cl/1; % the corresponding prooftree (a list of pairs % (Resolvent,InputClause)) is collected in Proof. refute_df(([]:-[]),[]). refute_df(Clause,[(Clause,InputClause)|Proof]) :- cl(InputClause), resolve(Clause,InputClause,Resolvent), refute_df(Resolvent,Proof). % refute_bf(Clause,Proof) is true if Clause can be % refuted by resolution using breadth-first search % from the clauses defined by the predicate cl/1; % the corresponding prooftree (a list of pairs % (Resolvent,InputClause)) is collected in Proof. refute_bf(Clause,Proof) :- refute_bf([Clause/Clause/[]],Clause,Proof). % refute_bf(List,Clause,Proof) is true if one of % the clauses in List can be refuted by resolution % from the clauses defined by the predicate cl/1; % the corresponding prooftree (a list of pairs % (Resolvent,InputClause)) is collected in Proof, % and Clause gives the toplevel Clause to be refuted. % List consists of structures Cl/C/P, where Cl is % the clause to be refuted, C is a copy of Clause % with the correct variable bindings, and P is % a partial prooftree from C to Cl. refute_bf([([]:-[])/Clause/Proof|_],Clause,Proof). refute_bf([Clause/C2/Proof|L],C,P) :- resolvents(Clause/C2/Proof,L1), append(L,L1,L2), refute_bf(L2,C,P). refute_bf([_|L],C,P) :- refute_bf(L,C,P). % resolvents(Clause/C/Proof,L) is true if L contains % the resolvents of Clause with some axiom, each with % the appropriate copy of the toplevel goal, and a % partial prooftree. resolvents(Clause/C/Proof,L) :- mybagof(ResClause/C/[(Clause,Cl)|Proof], (cl(Cl),resolve(Clause,Cl,ResClause)), L). % resolve(Clause1,Clause2,Resolvent) is true if % Resolvent is the resolvent of Clause1 and Clause2. resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)) :- resolve(H1,B2,R1,R2), append(R1,H2,ResHead), append(B1,R2,ResBody). resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)) :- resolve(H2,B1,R2,R1), append(H1,R2,ResHead), append(R1,B2,ResBody). resolve([A|B],C,B,E) :- delete(A,C,E). resolve([A|B],C,[A|D],E) :- resolve(B,C,D,E). delete(A,[B|C],C) :- unify(A,B). delete(A,[B|C],[B|D]) :- delete(A,C,D). % version of bagof/3 which succeeds with the empty % list if there are no solutions. mybagof(X,G,L) :- bagof(X,G,L),!. mybagof(_,_,[]).