%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A propositional resolution calculus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% inference_rules: THEORY BEGIN IMPORTING interpretation_defs A: VAR symbol C, D, Factor, Resolvent, FactRes: VAR clause Cs: VAR set[clause] I: VAR interpret factor(C, Factor): bool = EXISTS A: count(pos(A), C) > 1 AND Factor = remove(pos(A), C) factor_sound: LEMMA true?(I,C) AND factor(C, Factor) IMPLIES true?(I, Factor) resolve(C, D, Resolvent): bool = EXISTS A: member(pos(A), C) AND member(neg(A), D) AND Resolvent = union(remove(pos(A), C), remove(neg(A), D)) resolve_sound: LEMMA true?(I,C) AND true?(I, D) AND resolve(C, D, Resolvent) IMPLIES true?(I, Resolvent) consequence(Cs)(FactRes): bool = (EXISTS (C: (Cs)): factor(C, FactRes)) OR (EXISTS (C, D: (Cs)): resolve(C, D, FactRes)) consequence_sound: LEMMA true?(I,Cs) AND member(FactRes, consequence(Cs)) IMPLIES true?(I, FactRes) consequences(Cs)(C): INDUCTIVE bool = member(C,Cs) OR member(C, consequence(consequences(Cs))) consequences_sound: LEMMA true?(I,Cs) IMPLIES true?(I, consequences(Cs)) END inference_rules