module aux.
import fol.
type eq_form form -> form -> o.
eq_form truth truth.
eq_form false false.
eq_form (neg A) (neg A') :- eq_form A A'.
eq_form (A and B) (A' and B') &
eq_form (A or B) (A' or B') &
eq_form (A imp B) (A' imp B') :- eq_form A A', eq_form B B'.
eq_form (forall _ A) (forall _ B) &
eq_form (exists _ A) (exists _ B) :- pi x\(eq_form (A x) (B x)).
eq_form A A.
type not_atomic, atomic form -> o.
not_atomic truth & not_atomic false.
not_atomic (_ and _) & not_atomic (_ or _) & not_atomic (_ imp _).
not_atomic (forall _ _) & not_atomic (exists _ _).
atomic B :- not (not_atomic B).
type rem_vac form -> form -> o.
rem_vac (forall _ x\B) C &
rem_vac (exists _ x\B) C :- !, rem_vac B C.
rem_vac (forall Name B) (forall Name C) &
rem_vac (exists Name B) (exists Name C) :- !, pi x\ (rem_vac (B x) (C x)).
rem_vac (B and C) (B' and C') &
rem_vac (B or C) (B' or C') &
rem_vac (B imp C) (B' imp C') :- !, rem_vac B B', rem_vac C C'.
rem_vac (neg B) (neg B') :- !, rem_vac B B'.
rem_vac truth truth :- !.
rem_vac false false :- !.
rem_vac A A.
type select_pos, select_neg form -> form -> form -> form -> o.
select_pos A A H H :- atomic A.
select_pos A (C and D) H (E and D) & select_pos A (D and C) H (D and E) &
select_pos A (C or D) H (E or D) & select_pos A (D or C) H (D or E) &
select_pos A (D imp C) H (D imp E) :- select_pos A C H E.
select_pos A (C imp D) H (E imp D) &
select_pos A (neg C) H (neg E) :- select_neg A C H E.
select_neg A (C and D) H (E and D) & select_neg A (D and C) H (D and E) &
select_neg A (C or D) H (E or D) & select_neg A (D or C) H (D or E) &
select_neg A (D imp C) H (D imp E) :- select_neg A C H E.
select_neg A (C imp D) H (E imp D) &
select_neg A (neg C) H (neg E) :- select_pos A C H E.
type rem_truth form -> form -> o.
rem_truth (truth imp B) C :- !, rem_truth B C.
rem_truth (B imp truth) truth :- !.
rem_truth (truth and B) C &
rem_truth (B and truth) C :- !, rem_truth B C.
rem_truth (truth or B) truth :- !.
rem_truth (B or truth) truth :- !.
rem_truth (neg truth) false :- !.
rem_truth (forall Name B) (forall Name C) &
rem_truth (exists Name B) (exists Name C) :- !, pi x\ (rem_truth (B x) (C x)).
rem_truth (B and C) (B' and C') &
rem_truth (B or C) (B' or C') &
rem_truth (B imp C) (B' imp C') :- !, rem_truth B B', rem_truth C C'.
rem_truth (neg B) (neg B') :- !, rem_truth B B'.
rem_truth truth truth :- !.
rem_truth false false :- !.
rem_truth A A.
type instan_forall form -> list i -> form -> o.
instan_forall (forall _ B) (T::Ts) Result :- instan_forall (B T) Ts Result.
instan_forall Result nil Result.
type instan_exists form -> list i -> form -> o.
instan_exists (exists _ B) (T::Ts) Result :- instan_exists (B T) Ts Result.
instan_exists Result nil Result.
type delete_member A -> list A -> list A -> o.
delete_member _ nil nil.
delete_member X (X::L) K :- !, delete_member X L K.
delete_member X (Y::L) (Y::K) :- !, delete_member X L K.