%% Version: 1.11tptp  -  Date: 24/08/2019  -  File: nnf_mm.pl
%%
%% Purpose: - computes Skolemized negation normal form for a
%%            first-order formula (based on leanTAP's nnf.pl)
%%          - computes disjunctive normal form for a formula
%%            in Skolemized negational normal form
%%          - computes a matrix form (and applies MULT and TAUT
%%            reductions) for a formula in disjunctive normal form
%%          - renames variables so that a unique variable name
%%            is assigned to each quantifier in a formula
%%
%% Author:  Jens Otten
%% Web:     www.leancop.de
%%
%% Usage:   make_matrix(F,M). % where F is a first-order formula
%%                            % and its clausal form M is returned
%%
%% Example: make_matrix(?[Y]: (![X]: ((p(Y) => p(X))) ), Matrix).
%%          Matrix = [[-(p(X1))], [p(f_sk(1,[X1]))]]
%%
%% Copyright: (c) 2019 by Jens Otten
%% License:   GNU General Public License


% connectives and quantifiers

:- op(1130, xfy, <=>).  % equivalence
:- op(1110, xfy, =>).   % implication
:- op(1100, xfy, '|').  % disjunction
:- op(1000, xfy, &).    % conjunction
:- op( 500, fy, ~).     % negation

:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).

% -----------------------------------------------------------------
%  nnf(+Fml,?NNF)
%
% Fml is a first-order formula and NNF its Skolemized negation
% normal form (where quantifiers have been removed from NNF).
%
% Syntax of Fml:
%  negation: '~', disj: '|', conj: '&', impl: '=>', eqv: '<=>',
%  quant. '![X]:<Formula>', '?[X]:<Formula>' where 'X' is a
%  prolog variable.
%
% Syntax of NNF: negation: '~', disj: '|', conj: '&'.
%
% Example:  nnf(?[Y]: (![X]: ((p(Y) => p(X))) ),NNF).
%           NNF = (~ p(X1) | p(f_sk(1,[X1]))

nnf(Fml,NNF) :- nnf(Fml,[],NNF,_,1,_).

% -----------------------------------------------------------------
%  nnf(+Fml,+FreeV,-NNF,-Paths,+I,-I1)
%
% Fml,NNF:    See above.
% FreeV:      List of free variables in Fml.
% Paths:      Number of disjunctive paths in Fml.

nnf(Fml,FreeV,NNF,Paths,I,I1) :-
    (Fml = ~(~A)       -> Fml1 = A;
     Fml = ~(![X]:F)   -> Fml1 = (?[X]: ~F);
     Fml = ~(?[X]:F)   -> Fml1 = (![X]: ~F);
     Fml = ~((A | B))  -> Fml1 = ((~A & ~B));
     Fml = ~((A & B))  -> Fml1 = (~A | ~B);
     Fml = (A => B)    -> Fml1 = (~A | B);
     Fml = ~((A => B)) -> Fml1 = ((A & ~B));
     Fml = (A <=> B)   -> Fml1 = ((A & B) ; (~A & ~B));
     Fml = ~((A<=>B))  -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
    nnf(Fml1,FreeV,NNF,Paths,I,I1).

nnf((?[X]:F),FreeV,NNF,Paths,I,I1) :- !,
    nnf(F,[X|FreeV],NNF,Paths,I,I1).

nnf((![X]:Fml),FreeV,NNF,Paths,I,I1) :- !,
    copy_term((X,Fml,FreeV),(f_sk(I,FreeV),Fml1,FreeV)), I2 is I+1,
    nnf(Fml1,FreeV,NNF,Paths,I2,I1).

nnf((A | B),FreeV,NNF,Paths,I,I1) :- !,
    nnf(A,FreeV,NNF1,Paths1,I,I2),
    nnf(B,FreeV,NNF2,Paths2,I2,I1),
    Paths is Paths1 * Paths2,
    (Paths1 > Paths2 -> NNF = (NNF2|NNF1);
                        NNF = (NNF1|NNF2)).

nnf((A & B),FreeV,NNF,Paths,I,I1) :- !,
    nnf(A,FreeV,NNF1,Paths1,I,I2),
    nnf(B,FreeV,NNF2,Paths2,I2,I1),
    Paths is Paths1 + Paths2,
    (Paths1 > Paths2 -> NNF = (NNF2&NNF1);
                        NNF = (NNF1&NNF2)).

nnf(Lit,_,Lit,1,I,I).

% -----------------------------------------------------------------
%  make_matrix(+Fml,-Matrix)
%
% Syntax of Fml:
%  negation: '~', disj: '|', conj: '&', impl: '=>', eqv: '<=>',
%  quant. '![X]:<Formula>', '?[X]:<Formula>' where 'X' is a
%  prolog variable.
%
% Syntax of Matrix:
%  Matrix is a list of clauses; a clause is a list of literals.
%
% Example:  make_matrix(?[Y]: (![X]: ((p(Y) => p(X))) ),Matrix).
%           Matrix = [[-(p(X1))], [p(f_sk(1,[X1]))]]

make_matrix(Fml,Matrix) :-
    univar(Fml,[],Fml1), nnf(Fml1,NNF), dnf(NNF,DNF), mat(DNF,Matrix).

% -----------------------------------------------------------------
%  dnf(+NNF,-DNF)
%
% NNF:    See above.
%
% Syntax of DNF: negation: '~', disj: '|', conj: '&' .
%
% Example:  dnf(((p | ~p) & (q | ~q)),DNF).
%           DNF = (p & q | p & ~ q) | ~ p & q | ~ p & ~ q

dnf(((A|B)&C),(F1|F2)) :- !, dnf((A&C),F1), dnf((B&C),F2).
dnf((A&(B|C)),(F1|F2)) :- !, dnf((A&B),F1), dnf((A&C),F2).
dnf((A&B),F) :- !, dnf(A,A1), dnf(B,B1),
    ( (A1=(C|D);B1=(C|D)) -> dnf((A1&B1),F) ; F=(A1&B1) ).
dnf((A|B),(A1|B1)) :- !, dnf(A,A1), dnf(B,B1).
dnf(Lit,Lit).

% -----------------------------------------------------------------
%  mat(+DNF,-Matrix)
%
% DNF,Matrix:    See above.
%
% Example:  mat(((p & q | p & ~ q) | ~ p & q | ~ p & ~ q),Matrix).
%           Matrix = [[p, q], [p, -(q)], [-(p), q], [-(p), -(q)]]

mat((A|B),M) :- !, mat(A,MA), mat(B,MB), append(MA,MB,M).
mat((A&B),M) :- !,
    ( mat(A,[CA]), mat(B,[CB]) -> union2(CA,CB,M) ; M=[] ).
mat(~Lit,[[-Lit]]) :- !.
mat(Lit,[[Lit]]).

% -----------------------------------------------------------------
%  union2/member2  (realizes MULT/TAUT reductions)

union2([],L,[L]).
union2([X|L1],L2,M) :- member2(X,L2), !, union2(L1,L2,M).
union2([X|_],L2,M)  :- (-Xn=X;-X=Xn) -> member2(Xn,L2), !, M=[].
union2([X|L1],L2,M) :- union2(L1,[X|L2],M).

member2(X,[Y|_]) :- X==Y, !.
member2(X,[_|T]) :- member2(X,T).

% -----------------------------------------------------------------
%  univar (unique variable names)

univar(X,_,X)  :- (atomic(X);var(X);X==[[]]), !.
univar(F,Q,F1) :-
    F=..[A,B|T], ( (A=(?);A=!), B=[X]:C -> delete2(Q,X,Q1),
    copy_term((X,C,Q1),(Y,D,Q1)), univar(D,[Y|Q],D1), F1=..[A,[Y]:D1];
    univar(B,Q,B1), univar(T,Q,T1), F1=..[A,B1|T1] ).

% -----------------------------------------------------------------
%  delete2 (deletes variable from list)

delete2([],_,[]).
delete2([X|T],Y,T1) :- X==Y, !, delete2(T,Y,T1).
delete2([X|T],Y,[X|T1]) :- delete2(T,Y,T1).