18% definitions of logical connectives and quantifiers
   19
   20% leanCoP syntax
   21:- op(1130, xfy, <=>). % equivalence
   22:- op(1110, xfy, =>).  % implication
   23%                      % disjunction (;)
   24%                      % conjunction (,)
   25:- op( 500, fy, ~).    % negation
   26:- op( 500, fy, all).  % universal quantifier
   27:- op( 500, fy, ex).   % existential quantifier
   28:- op( 500,xfy, :).   29
   30% TPTP syntax
   31:- op(1130, xfy, <~>).  % negated equivalence
   32:- op(1110, xfy, <=).   % implication
   33:- op(1100, xfy, '|').  % disjunction
   34:- op(1100, xfy, '~|'). % negated disjunction
   35:- op(1000, xfy, &).    % conjunction
   36:- op(1000, xfy, ~&).   % negated conjunction
   37:- op( 500, fy, !).     % universal quantifier
   38:- op( 500, fy, ?).     % existential quantifier
   39:- op( 400, xfx, =).    % equality
   40:- op( 300, xf, !).     % negated equality (for !=)
   41:- op( 299, fx, $).     % for $true/$false
   42
   43% TPTP syntax to leanCoP syntax mapping
   44
   45op_tptp2((A<=>B),(A1<=>B1),   [A,B],[A1,B1]).
   46op_tptp2((A<~>B),~((A1<=>B1)),[A,B],[A1,B1]).
   47op_tptp2((A=>B),(A1=>B1),     [A,B],[A1,B1]).
   48op_tptp2((A<=B),(B1=>A1),     [A,B],[A1,B1]).
   49op_tptp2((A|B),(A1;B1),       [A,B],[A1,B1]).
   50op_tptp2((A'~|'B),~((A1;B1)), [A,B],[A1,B1]).
   51op_tptp2((A&B),(A1,B1),       [A,B],[A1,B1]).
   52op_tptp2((A~&B),~((A1,B1)),   [A,B],[A1,B1]).
   53op_tptp2(~A,~A1,[A],[A1]).
   54op_tptp2((! [V]:A),(all V:A1),     [A],[A1]).
   55op_tptp2((! [V|Vars]:A),(all V:A1),[! Vars:A],[A1]).
   56op_tptp2((? [V]:A),(ex V:A1),      [A],[A1]).
   57op_tptp2((? [V|Vars]:A),(ex V:A1), [? Vars:A],[A1]).
   58op_tptp2($true,(true___=>true___),      [],[]).
   59op_tptp2($false,(false___ , ~ false___),[],[]).
   60op_tptp2(A=B,~(A1=B),[],[]) :- \+var(A), A=(A1!).
   61op_tptp2(P,P,[],[]).
   62
   63
   64%%% translate into leanCoP syntax
   65
   66leancop_tptp2(File,F) :- leancop_tptp2(File,'',[_],F,_).
   67
   68leancop_tptp2(File,AxPath,AxNames,F,Con) :-
   69    open(File,read,Stream), ( fof2cop(Stream,AxPath,AxNames,A,Con)
   70    -> close(Stream) ; close(Stream), fail ),
   71    ( Con=[] -> F=A ; A=[] -> F=Con ; F=(A=>Con) ).
   72
   73fof2cop(Stream,AxPath,AxNames,F,Con) :-
   74    read(Stream,Term),
   75    ( Term=end_of_file -> F=[], Con=[] ;
   76      ( Term=..[fof,Name,Type,Fml|_] ->
   77        ( \+member(Name,AxNames) -> true ; fml2cop([Fml],[Fml1]) ),
   78        ( Type=conjecture -> Con=Fml1 ; Con=Con1 ) ;
   79        ( Term=include(File), AxNames2=[_] ;
   80          Term=include(File,AxNames2) ) -> name(AxPath,AL),
   81          name(File,FL), append(AL,FL,AxL), name(AxFile,AxL),
   82          leancop_tptp2(AxFile,'',AxNames2,Fml1,_), Con=Con1
   83      ), fof2cop(Stream,AxPath,AxNames,F1,Con1),
   84      ( Term=..[fof,N,Type|_], (Type=conjecture;\+member(N,AxNames))
   85      -> (F1=[] -> F=[] ; F=F1) ; (F1=[] -> F=Fml1 ; F=(Fml1,F1)) )
   86    ).
   87
   88fml2cop([],[]).
   89fml2cop([F|Fml],[F1|Fml1]) :-
   90    op_tptp2(F,F1,FL,FL1) -> fml2cop(FL,FL1), fml2cop(Fml,Fml1).
   91
   92
   93%%% add equality axioms
   94
   95leancop_equal(F,F1) :-
   96    collect_predfunc([F],PL,FL), append(PL2,[(=,2)|PL3],PL),
   97    append(PL2,PL3,PL1) -> basic_equal_axioms(F0),
   98    subst_pred_axioms(PL1,F2), (F2=[] -> F3=F0 ; F3=(F0,F2)),
   99    subst_func_axioms(FL,F4), (F4=[] -> F5=F3 ; F5=(F3,F4)),
  100    ( F=(A=>C) -> F1=((F5,A)=>C) ; F1=(F5=>F) ) ; F1=F.
  101
  102basic_equal_axioms(F) :-
  103    F=(( all X:(X=X) ),
  104       ( all X:all Y:((X=Y)=>(Y=X)) ),
  105       ( all X:all Y:all Z:(((X=Y),(Y=Z))=>(X=Z)) )).
  106
  107% generate substitution axioms
  108
  109subst_pred_axioms([],[]).
  110subst_pred_axioms([(P,I)|PL],F) :-
  111    subst_axiom(A,B,C,D,E,I), subst_pred_axioms(PL,F1), P1=..[P|C],
  112    P2=..[P|D], E=(B,P1=>P2), ( F1=[] -> F=A ; F=(A,F1) ).
  113
  114subst_func_axioms([],[]).
  115subst_func_axioms([(P,I)|FL],F) :-
  116    subst_axiom(A,B,C,D,E,I), subst_func_axioms(FL,F1), P1=..[P|C],
  117    P2=..[P|D], E=(B=>(P1=P2)), ( F1=[] -> F=A ; F=(A,F1) ).
  118
  119subst_axiom((all X:all Y:E),(X=Y),[X],[Y],E,1).
  120subst_axiom(A,B,[X|C],[Y|D],E,I) :-
  121    I>1, I1 is I-1, subst_axiom(A1,B1,C,D,E,I1),
  122    A=(all X:all Y:A1), B=((X=Y),B1).
  123
  124% collect predicate & function symbols
  125
  126collect_predfunc([],[],[]).
  127collect_predfunc([F|Fml],PL,FL) :-
  128    ( ( F=..[<=>|F1] ; F=..[=>|F1] ; F=..[;|F1] ; F=..[','|F1] ;
  129        F=..[~|F1] ; (F=..[all,_:F2] ; F=..[ex,_:F2]), F1=[F2] ) ->
  130      collect_predfunc(F1,PL1,FL1) ; F=..[P|Arg], length(Arg,I),
  131      I>0 ->  PL1=[(P,I)], collect_func(Arg,FL1) ; PL1=[], FL1=[] ),
  132    collect_predfunc(Fml,PL2,FL2),
  133    union1(PL1,PL2,PL), union1(FL1,FL2,FL).
  134
  135collect_func([],[]).
  136collect_func([F|FunL],FL) :-
  137    ( \+var(F), F=..[F1|Arg], length(Arg,I), I>0 ->
  138      collect_func(Arg,FL1), union1([(F1,I)],FL1,FL2) ; FL2=[] ),
  139    collect_func(FunL,FL3), union1(FL2,FL3,FL).
  140
  141union1([],L,L).
  142union1([H|L1],L2,L3) :- member(H,L2), !, union1(L1,L2,L3).
  143union1([H|L1],L2,[H|L3]) :- union1(L1,L2,L3)