19% definitions of logical connectives and quantifiers
   20
   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
   31% ------------------------------------------------------------------
   32%  make_matrix(+Fml,-Matrix,+Settings)
   33%    -  transform first-order formula into set of clauses (matrix)
   34%
   35%  Fml, Matrix: first-order formula and matrix
   36%
   37%  Settings: list of settings, which can contain def, nodef and conj;
   38%            if it contains nodef/def, no definitional transformation
   39%            or a complete definitional transformation is done,
   40%            otherwise a definitional transformation is done for
   41%            the conjecture and the standard transformation is done
   42%            for the axioms; conjecture is marked if conj is given
   43%
   44%  Syntax of Fml: negation '~', disjunction ';', conjunction ',',
   45%      implication '=>', equivalence '<=>', universal/existential
   46%      quantifier 'all X:<Formula>'/'ex X:<Formula>' where 'X' is a
   47%      Prolog variable, and atomic formulae are Prolog atoms.
   48%
   49%  Example: make_matrix(ex Y:(all X:((p(Y) => p(X)))),Matrix,[]).
   50%           Matrix = [[-(p(X1))], [p(1 ^ [X1])]]
   51
   52make_matrix(Fml,Matrix,Set) :-
   53    univar(Fml,[],F1),
   54    ( member(conj,Set), F1=(A=>C) -> F2=((A,#)=>(#,C)) ; F2=F1 ),
   55    ( member(nodef,Set) ->
   56       def_nnf(F2,NNF,1,_,nnf), dnf(NNF,DNF)
   57       ;
   58       \+member(def,Set), F2=(B=>D) ->
   59        def_nnf(~(B),NNF,1,I,nnf), dnf(NNF,DNF1),
   60        def_nnf(D,DNF2,I,_,def), DNF=(DNF2;DNF1)
   61        ;
   62        def_nnf(F2,DNF,1,_,def)
   63    ),
   64    mat(DNF,M),
   65    ( member(reo(I),Set) -> mreorder(M,Matrix,I) ; Matrix=M ).
   66
   67% ------------------------------------------------------------------
   68%  def_nnf(+Fml,-DEF)  -  transform formula into a definitional
   69%                         Skolemized negation normal form (DEF)
   70%  Fml, DEF: first-order formula and formula in DEF
   71%
   72%  Example: def_nnf(ex Y:(all X:((p(Y) => p(X)))),DEF,def).
   73%           DEF = ~ p(X1) ; p(1 ^ [X1])
   74
   75def_nnf(Fml,DEF,I,I1,Set) :-
   76    def(Fml,[],NNF,DEF1,_,I,I1,Set), def(DEF1,NNF,DEF).
   77
   78def([],Fml,Fml).
   79def([(A,(B;C))|DefL],DEF,Fml) :- !, def([(A,B),(A,C)|DefL],DEF,Fml).
   80def([A|DefL],DEF,Fml) :- def(DefL,(A;DEF),Fml).
   81
   82def(Fml,FreeV,NNF,DEF,Paths,I,I1,Set) :-
   83    ( Fml = ~(~A)      -> Fml1 = A;
   84      Fml = ~(all X:F) -> Fml1 = (ex X: ~F);
   85      Fml = ~(ex X:F)  -> Fml1 = (all X: ~F);
   86      Fml = ~((A ; B)) -> Fml1 = ((~A , ~B));
   87      Fml = ~((A , B)) -> Fml1 = (~A ; ~B);
   88      Fml = (A => B)   -> Fml1 = (~A ; B);
   89      Fml = ~((A => B))-> Fml1 = ((A , ~B));
   90      Fml = (A <=> B)  ->
   91      ( Set=def        -> Fml1 = ((A => B) , (B => A));
   92                          Fml1 = ((A , B) ; (~A , ~B)) );
   93      Fml = ~((A<=>B)) -> Fml1 = ((A , ~B) ; (~A , B)) ), !,
   94    def(Fml1,FreeV,NNF,DEF,Paths,I,I1,Set).
   95
   96def((ex X:F),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
   97    def(F,[X|FreeV],NNF,DEF,Paths,I,I1,Set).
   98
   99def((all X:Fml),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
  100    copy_term((X,Fml,FreeV),((I^FreeV),Fml1,FreeV)), I2 is I+1,
  101    def(Fml1,FreeV,NNF,DEF,Paths,I2,I1,Set).
  102
  103def((A ; B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
  104    def(A,FreeV,NNF1,DEF1,Paths1,I,I2,Set),
  105    def(B,FreeV,NNF2,DEF2,Paths2,I2,I1,Set),
  106    append(DEF1,DEF2,DEF), Paths is Paths1 * Paths2,
  107    (Paths1 > Paths2 -> NNF = (NNF2;NNF1);
  108                        NNF = (NNF1;NNF2)).
  109
  110def((A , B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
  111    def(A,FreeV,NNF3,DEF3,Paths1,I,I2,Set),
  112    ( NNF3=(_;_), Set=def -> append([(~I2^FreeV,NNF3)],DEF3,DEF1),
  113                             NNF1=I2^FreeV, I3 is I2+1 ;
  114                             DEF1=DEF3, NNF1=NNF3, I3 is I2 ),
  115    def(B,FreeV,NNF4,DEF4,Paths2,I3,I4,Set),
  116    ( NNF4=(_;_), Set=def -> append([(~I4^FreeV,NNF4)],DEF4,DEF2),
  117                             NNF2=I4^FreeV, I1 is I4+1 ;
  118                             DEF2=DEF4, NNF2=NNF4, I1 is I4 ),
  119    append(DEF1,DEF2,DEF), Paths is Paths1 + Paths2,
  120    (Paths1 > Paths2 -> NNF = (NNF2,NNF1);
  121                        NNF = (NNF1,NNF2)).
  122
  123def(Lit,_,Lit,[],1,I,I,_).
  124
  125% ------------------------------------------------------------------
  126%  dnf(+NNF,-DNF)  -  transform formula in NNF into formula in DNF
  127%  NNF, DNF: formulae in NNF and DNF
  128%
  129%  Example: dnf(((p;~p),(q;~q)),DNF).
  130%           DNF = (p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q
  131
  132dnf(((A;B),C),(F1;F2)) :- !, dnf((A,C),F1), dnf((B,C),F2).
  133dnf((A,(B;C)),(F1;F2)) :- !, dnf((A,B),F1), dnf((A,C),F2).
  134dnf((A,B),F) :- !, dnf(A,A1), dnf(B,B1),
  135    ( (A1=(C;D);B1=(C;D)) -> dnf((A1,B1),F) ; F=(A1,B1) ).
  136dnf((A;B),(A1;B1)) :- !, dnf(A,A1), dnf(B,B1).
  137dnf(Lit,Lit).
  138
  139% ------------------------------------------------------------------
  140%  mat(+DNF,-Matrix)  -  transform formula in DNF into matrix
  141%  DNF, Matrix: formula in DNF, matrix
  142%
  143%  Example: mat(((p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q),Matrix).
  144%           Matrix = [[p, q], [p, -(q)], [-(p), q], [-(p), -(q)]]
  145
  146mat((A;B),M) :- !, mat(A,MA), mat(B,MB), append(MA,MB,M).
  147mat((A,B),M) :- !, (mat(A,[CA]),mat(B,[CB]) -> union2(CA,CB,M);M=[]).
  148mat(~Lit,[[-Lit]]) :- !.
  149mat(Lit,[[Lit]]).
  150
  151% ------------------------------------------------------------------
  152%  univar(+Fml,[],-Fml1)  -  rename variables
  153%  Fml, Fml1: first-order formulae
  154%
  155%  Example: univar((all X:(p(X) => (ex X:p(X)))),[],F1).
  156%           F1 = all Y : (p(Y) => ex Z : p(Z))
  157
  158univar(X,_,X)  :- (atomic(X);var(X);X==[[]]), !.
  159univar(F,Q,F1) :-
  160    F=..[A,B|T], ( (A=ex;A=all) -> B=(X:C), delete2(Q,X,Q1),
  161    copy_term((X,C,Q1),(Y,D,Q1)), univar(D,[Y|Q],D1), F1=..[A,Y:D1] ;
  162    univar(B,Q,B1), univar(T,Q,T1), F1=..[A,B1|T1] ).
  163
  164% ------------------------------------------------------------------
  165%  union2/member2 - union and member for lists without unification
  166
  167union2([],L,[L]).
  168union2([X|L1],L2,M) :- member2(X,L2), !, union2(L1,L2,M).
  169union2([X|_],L2,M)  :- (-Xn=X;-X=Xn) -> member2(Xn,L2), !, M=[].
  170union2([X|L1],L2,M) :- union2(L1,[X|L2],M).
  171
  172member2(X,[Y|_]) :- X==Y, !.
  173member2(X,[_|T]) :- member2(X,T).
  174
  175% ------------------------------------------------------------------
  176%  delete2 - delete variable from list
  177
  178delete2([],_,[]).
  179delete2([X|T],Y,T1) :- X==Y, !, delete2(T,Y,T1).
  180delete2([X|T],Y,[X|T1]) :- delete2(T,Y,T1).
  181
  182% ------------------------------------------------------------------
  183%  mreorder - reorder clauses
  184
  185mreorder(M,M,0) :- !.
  186mreorder(M,M1,I) :-
  187    length(M,L), K is L//3, append(A,D,M), length(A,K),
  188    append(B,C,D), length(C,K), mreorder2(C,A,B,M2), I1 is I-1,
  189    mreorder(M2,M1,I1).
  190
  191mreorder2([],[],C,C).
  192mreorder2([A|A1],[B|B1],[C|C1],[A,B,C|M1]) :- mreorder2(A1,B1,C1,M1)