33:- module(nfsdl,[nnf/2, pnf/2, cf/2]).   34
   35% SWI Prolog modules do not export operators by default
   36% so they must be explicitly placed in the user namespace
   37
   38:- ( prolog_engine(swi) ->
   39     op( 400, fy, user:(box) ),	% Necessity, Always
   40     op( 400, fy, user:(dia) ),	% Possibly, Eventually
   41     op( 400, fy, user:(cir) )	% Next time
   42   ;
   43     op(400,fy,box),		% Necessity, Always
   44     op(400,fy,dia),		% Possibly, Eventually
   45     op(400,fy,cir)		% Next time
   46   ).   47
   48
   49
   50%%% Negation Normal Form
   51
   52% Usage: nnf(+Fml, ?NNF)
   53
   54nnf(Fml,NNF) :- nnf(Fml,[],NNF,_).
   55
   56% -----------------------------------------------------------------
   57%  nnf(+Fml,+FreeV,-NNF,-Paths)
   58%
   59% Fml,NNF:    See above.
   60% FreeV:      List of free variables in Fml.
   61% Paths:      Number of disjunctive paths in Fml.
   62
   63nnf(box F,FreeV,BOX,Paths) :- !,
   64	nnf(F,FreeV,NNF,Paths), cnf(NNF,CNF), boxRule(box CNF, BOX).
   65
   66nnf(dia F,FreeV,DIA,Paths) :- !,
   67	nnf(F,FreeV,NNF,Paths), dnf(NNF,DNF), diaRule(dia DNF, DIA).
   68
   69nnf(cir F,FreeV,CIR,Paths) :- !,
   70	nnf(F,FreeV,NNF,Paths), cirRule(cir NNF, CIR).
   71
   72nnf(until(A,B),FreeV,NNF,Paths) :- !,
   73	nnf(A,FreeV,NNF1,Paths1),
   74	nnf(B,FreeV,NNF2,Paths2),
   75	Paths is Paths1 + Paths2,
   76	NNF = until(NNF1, NNF2).
   77
   78nnf(all(X,F),FreeV,all(X,NNF),Paths) :- !,
   79	nnf(F,[X|FreeV],NNF,Paths).
   80
   81nnf(exists(X,Fml),FreeV,NNF,Paths) :- !,
   82	skolem(Fml,X,FreeV,FmlSk),
   83	nnf(FmlSk,FreeV,NNF,Paths).
   84
   85/*
   86nnf(atleast(1,X,Fml),FreeV,NNF,Paths) :-
   87	!,
   88	nnf(exists(X,Fml),FreeV,NNF,Paths).
   89nnf(atleast(N,X,Fml),FreeV,NNF,Paths) :-
   90	!,
   91	NewN is N - 1,
   92	nnf(dland(exists(X,Fml),atleast(NewN,Y,Fml)),FreeV,NNF,Paths).
   93
   94nnf(atmost(1,X,Fml),FreeV,NNF,Paths) :-
   95	!,
   96	nnf(dlnot(dland(exists(Y,Fml),exists(Z,Fml))),FreeV,NNF,Paths).
   97nnf(atmost(N,X,Fml),FreeV,NNF,Paths) :-
   98	!,
   99	NewN is N - 1,
  100	nnf(dland(exists(Y,Fml),atmost(NewN,X,Fml)),FreeV,NNF,Paths).
  101*/
  102
  103nnf(dland(A,B),FreeV,NNF,Paths) :- !,
  104	nnf(A,FreeV,NNF1,Paths1),
  105	nnf(B,FreeV,NNF2,Paths2),
  106	Paths is Paths1 * Paths2,
  107	(Paths1 > Paths2 -> NNF = dland(NNF2,NNF1);
  108		            NNF = dland(NNF1,NNF2)).
  109
  110nnf(dlor(A,B),FreeV,NNF,Paths) :- !,
  111	nnf(A,FreeV,NNF1,Paths1),
  112	nnf(B,FreeV,NNF2,Paths2),
  113	Paths is Paths1 + Paths2,
  114	(Paths1 > Paths2 -> NNF = dlor(NNF2,NNF1);
  115		            NNF = dlor(NNF1,NNF2)).
  116
  117nnf(Fml,FreeV,NNF,Paths) :- 
  118	(Fml = dlnot(dlnot(A))   -> Fml1 = A;
  119	 Fml = dlnot(box F)      -> Fml1 = dia dlnot(F);
  120	 Fml = dlnot(dia F)      -> Fml1 = box dlnot(F);
  121	 Fml = dlnot(cir F)      -> Fml1 = cir dlnot(F);
  122	 Fml = dlnot(until(A,B)) -> (nnf(dlnot(A),FreeV,NNA,_), nnf(dlnot(B),FreeV,NNB,_),
  123                                     Fml1 = dlor( all(NNB), until(NNB,dland(NNA,NNB))));
  124	 Fml = dlnot(all(X,F))   -> Fml1 = exists(X,dlnot(F));
  125	 Fml = dlnot(exists(X,F))    -> Fml1 = all(X,dlnot(F));
  126/*
  127	 Fml = dlnot(atleast(N,X,F)) -> Fml1 = atmost(N,X,F);
  128	 Fml = dlnot(atmost(N,X,F)) -> Fml1 = atleast(N,X,F);
  129*/
  130	 Fml = dlnot(dlor(A,B))  -> Fml1 = dland( dlnot(A), dlnot(B) );
  131	 Fml = dlnot(dland(A,B)) -> Fml1 = dlor( dlnot(A), dlnot(B) );
  132	 Fml = dlimplies(A,B)        -> Fml1 = dlor( dlnot(A), B );
  133	 Fml = dlnot(dlimplies(A,B)) -> Fml1 = dland( A, dlnot(B) );
  134	 Fml = dlequiv(A,B)        -> Fml1 = dlor( dland(A, B), dland(dlnot(A), dlnot(B)) );
  135	 Fml = dlnot(dlequiv(A,B)) -> Fml1 = dlor( dland(A, dlnot(B)) , dland(dlnot(A), B) )
  136	),!,
  137	nnf(Fml1,FreeV,NNF,Paths).
  138
  139nnf(Lit,_,Lit,1).
  140
  141boxRule(box dland(A,B), dland(BA,BB)) :- !, boxRule(box A,BA), boxRule(box B,BB).
  142boxRule(BOX, BOX).
  143
  144diaRule(dia dlor(A,B), dlor(DA,DB)) :- !, diaRule(dia A,DA), diaRule(dia B,DB).
  145diaRule(DIA, DIA).
  146
  147cirRule(cir dlor(A,B), dlor(DA,DB)) :- !, cirRule(cir A,DA), cirRule(cir B,DB).
  148cirRule(cir dland(A,B), dland(DA,DB)) :- !, cirRule(cir A,DA), cirRule(cir B,DB).
  149cirRule(CIR, CIR).
  150
  151
  152%%%
  153%%%  Conjunctive Normal Form (CNF) -- assumes Fml in NNF
  154%%%
  155
  156% Usage: cnf( +NNF, ?CNF )
  157
  158cnf(dland(P,Q), dland(P1,Q1)):- !, cnf(P, P1), cnf(Q, Q1).
  159cnf(dlor(P,Q),     CNF):- !, cnf(P, P1), cnf(Q, Q1), cnf1( dlor(P1,Q1), CNF ).
  160cnf(CNF,       CNF).
  161
  162cnf1( dlor(dland(P,Q), R), dland(P1,Q1) ):- !, cnf1( dlor(P,R), P1), cnf1( dlor(Q,R), Q1).
  163cnf1( dlor(P, dland(Q,R)), dland(P1,Q1) ):- !, cnf1( dlor(P,Q), P1), cnf1( dlor(P,R), Q1).
  164cnf1( CNF,                 CNF).
  165
  166
  167%%%
  168%%% Disjunctive Normal Form (DNF) -- assumes Fml in NNF
  169%%%
  170% Usage: dnf( +NNF, ?DNF )
  171
  172dnf( dlor(P,Q),  dlor(P1,Q1) ) :- !, dnf(P, P1), dnf(Q, Q1).
  173dnf( dland(P,Q), DNF) :- !, dnf(P, P1), dnf(Q, Q1), dnf1( dland(P1,Q1), DNF).
  174dnf(DNF,       DNF).
  175
  176dnf1( dland(P, dlor(Q,R)),  dlor(P1,Q1) ):- !, dnf1( dland(P,Q), P1), dnf1( dland(P,R), Q1).
  177dnf1( dland( dlor(P,Q), R), dlor(P1,Q1) ):- !, dnf1( dland(P,R), P1), dnf1( dland(Q,R), Q1).
  178dnf1( DNF,                  DNF ).

  186% Usage: pnf( +Fml, ?PNF ) -- assumes Fml in NNF
  187
  188pnf(F,PNF) :- pnf(F,[],PNF).
  189
  190% pnf(+Fml, +Vars, ?PNF)
  191
  192pnf(     all(X,F),Vs,   all(X,PNF)) :- !, pnf(F,[X|Vs], PNF).
  193pnf(  exists(X,F),Vs,exists(X,PNF)) :- !, pnf(F,[X|Vs], PNF).
  194
  195pnf(  dland(exists(X,A) , B),Vs,  exists(Y,PNF)) :- !, copy_term((X,A,Vs),(Y,Ay,Vs)),
  196                                        pnf(dland(Ay,B),[Y|Vs], PNF).
  197pnf(  dlor(exists(X,A), B),Vs,  exists(Y,PNF)) :- !, copy_term((X,A,Vs),(Y,Ay,Vs)),
  198                                        pnf(dlor(Ay,B),[Y|Vs], PNF).
  199pnf( dland(all(X,A), B),Vs, all(Y,PNF)) :- !, copy_term((X,A,Vs),(Y,Ay,Vs)),
  200                                        pnf(dland(Ay , B),[Y|Vs], PNF).
  201pnf( dlor(all(X,A), B),Vs, all(Y,PNF)) :- !, copy_term((X,A,Vs),(Y,Ay,Vs)),
  202                                        pnf(dlor(Ay,B),[Y|Vs], PNF).
  203
  204pnf( dland(A,exists(X,B)),Vs,  exists(Y,PNF)) :- !, copy_term((X,B,Vs),(Y,By,Vs)),
  205                                        pnf(dland(A, By),[Y|Vs], PNF).
  206pnf( dlor(A,exists(X,B)),Vs,  exists(Y,PNF)) :- !, copy_term((X,B,Vs),(Y,By,Vs)),
  207                                        pnf(dlor(A,By),[Y|Vs], PNF).
  208pnf( dland(A,all(X,B)),Vs, all(Y,PNF)) :- !, copy_term((X,B,Vs),(Y,By,Vs)),
  209                                        pnf(dland(A,By),[Y|Vs], PNF).
  210pnf( dlor(A,all(X,B)),Vs, all(Y,PNF)) :- !, copy_term((X,B,Vs),(Y,By,Vs)),
  211                                        pnf(dlor(A,By),[Y|Vs], PNF).
  212
  213pnf( dland(A, B),Vs,       PNF ) :- pnf(A,Vs,Ap), pnf(B,Vs,Bp), 
  214                                     (A\=Ap; B\=Bp), pnf(dland(Ap,Bp),Vs,PNF).
  215pnf( dlor(A, B),Vs,       PNF ) :- pnf(A,Vs,Ap), pnf(B,Vs,Bp), 
  216                                     (A\=Ap; B\=Bp), pnf(dlor(Ap,Bp),Vs,PNF).
  217
  218pnf(          PNF, _,       PNF ).
  219
  220%%%  Clausal Form (CF) -- assumes Fml in PNF and
  221%                                 each quantified variable is unique
  222
  223% cf(+Fml, ?Cs)
  224% Cs is a list of the form: [cl(Head,Body), ...]
  225% Head and Body are lists.
  226
  227cf(PNF, Cla):- removeQ(PNF,[], UnQ), cnf(UnQ,CNF), clausify(CNF,Cla,[]).
  228
  229% removes quantifiers
  230removeQ( all(X,F),Vars, RQ) :- removeQ(F,[X|Vars], RQ).
  231removeQ(  exists(X,F),Vars, RQ) :-
  232	skolem(F,X,Vars,Fsk),
  233	removeQ(Fsk,Vars, RQ).
  234removeQ( F,_,F ).
  235
  236clausify( dland(P,Q), C1, C2 ) :-
  237	!,
  238	clausify( P, C1, C3 ),
  239	clausify( Q, C3, C2 ).
  240clausify( P, [cl(A,B)|Cs], Cs ) :-
  241	inclause( P, A, [], B, [] ),
  242	!.
  243clausify( _, C, C ).
  244
  245inclause( dlor(P,Q), A, A1, B, B1 ) :-
  246	!,
  247	inclause( P, A2, A1, B2, B1 ),
  248	inclause( Q, A,  A2, B,  B2 ).
  249inclause( dlnot(P), A,  A, B1, B ) :-
  250	!,
  251	notin( P, A ),
  252	putin( P, B, B1 ).
  253inclause( P,  A1, A, B,  B ) :-
  254	!,
  255	notin( P, B ),
  256	putin( P, A, A1 ).
  257
  258notin(X,[Y|_]) :- X==Y, !, fail.
  259notin(X,[_|Y]) :- !,notin(X,Y).
  260notin(_,[]).
  261
  262putin(X,[],   [X]   ) :- !.
  263putin(X,[Y|L],[Y|L] ) :- X == Y,!.
  264putin(X,[Y|L],[Y|L1]) :- putin(X,L,L1).
  265
  266
  267
  268%%%  Skolemizing -- method 1
  269
  270% Usage: skolemize(+Fml,+X,+FreeV,?FmlSk)
  271% Replaces existentially quantified variable with the formula
  272% VARIABLES MUST BE PROLOG VARIABLES
  273% ex(X,p(X)) --> p(p(ex))
  274
  275skolem(Fml,X,FreeV,FmlSk):-
  276	copy_term((X,Fml,FreeV),(Fml,Fml1,FreeV)),
  277	copy_term((X,Fml1,FreeV),(exists,FmlSk,FreeV)).
  278
  279
  280
  281%%%  Skolemizing -- method 2
  282
  283% Usage: skolem( +Fml, +X, +FreeV, ?FmlSk )
  284% Replaces existentially quantified variable with a unique function
  285% fN(Vars) N=1,...
  286% VARIABLES MAYBE EITHER PROLOG VARIABLES OR TERMS
  287
  288skolem_not( F, X, FreeV, FmlSk) :-
  289	genatom( Fun ),
  290	Sk =..[Fun|FreeV],
  291	subst( F, X, Sk, FmlSk ).
  292
  293
  294%%% generate new atomic symbols
  295
  296genatom( A ) :-
  297	db_recorded( nfsdl, Inc, Ref ),
  298	!,
  299	erase( Ref ),
  300	NewInc is Inc + 1,
  301	db_recordz( nfsdl, NewInc, _ ),
  302	atom_concat( f, NewInc, A ).
  303genatom( f1 ) :-
  304	db_recordz( nfsdl, 1, _ ).
  305
  306
  307%%% Substitution
  308
  309% Usage: subst(+Fml,+X,+Sk,?FmlSk)
  310
  311subst(   all(Y,P), X,Sk,   all(Y,P1) ) :- !, subst( P,X,Sk,P1 ).
  312subst(exists(Y,P), X,Sk,exists(Y,P1) ) :- !, subst( P,X,Sk,P1 ).
  313subst( dland(P,Q), X,Sk,dland(P1,Q1) ) :- !, subst( P,X,Sk,P1 ), subst( Q,X,Sk,Q1 ).
  314subst(  dlor(P,Q), X,Sk, dlor(P1,Q1) ) :- !, subst( P,X,Sk,P1 ), subst( Q,X,Sk,Q1 ).
  315subst(       P,    X,Sk,       P1    ) :- functor(P,_,N), subst1( X, Sk, P, N, P1 ).
  316
  317subst1( _,  _, P, 0, P  ).
  318subst1( X, Sk, P, N, P1 ) :- N > 0, P =..[F|Args], subst2( X, Sk, Args, ArgS ),
  319                             P1 =..[F|ArgS].
  320
  321subst2( _,  _, [], [] ).
  322subst2( X, Sk, [A|As], [Sk|AS] ) :- X == A, !, subst2( X, Sk, As, AS).
  323subst2( X, Sk, [A|As], [A|AS]  ) :- var(A), !, subst2( X, Sk, As, AS).
  324subst2( X, Sk, [A|As], [Ap|AS] ) :- subst( A,X,Sk,Ap ),
  325                                    subst2( X, Sk, As, AS)