%% Version: 1.1tptp  -  Date: 24/08/2019  -  File: nnf_pure.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
%%          - renames variables so that a unique variable name
%%            is assigned to each quantifier in a formula
%%          - adapted to work with leanTAP
%%
%% Author:  Jens Otten
%% Web:     www.leancop.de
%%
%% 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) :- univar(Fml,[],Fml1), nnf(Fml1,[],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,(?[X]: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).

% -----------------------------------------------------------------
%  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).