1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003-5, Renate Schmidt, University of Manchester
    4%
    5% Adaptation of normalise.pl of ml2dfg translator
    6% The primistive operators are assumed to be
    7%     or, not, dia, comp, test, conv
    8%
    9%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   10
   11normalise([], []).
   12normalise([Fml|FmlList], [NFFml|NFList]) :-
   13    normalise(Fml, [], NFFml, Paths),
   14    write('             '), print(NFFml), nl, 
   15    write('Paths = '), print(Paths), nl,
   16    normalise(FmlList, NFList).
   17
   18%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   19%
   20% Elimination of implies, equiv, dia, plus
   21% Simplification &
   22% Transformation into normal form
   23%
   24%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   25
   26% Eliminating implies
   27
   28normalise(implies(A, B), FreeV, NF, Paths) :- !,
   29    normalise(or(not(A), B), FreeV, NF, Paths).
   30
   31normalise(not(implies(A, B)), FreeV, NF, Paths) :- !,
   32    normalise(not(or(not(A), B)), FreeV, NF, Paths).
   33
   34normalise(conv(implies(A, B)), FreeV, NF, Paths) :- !,
   35    normalise(or(not(conv(A)), conv(B)), FreeV, NF, Paths).
   36
   37% Eliminating implied
   38
   39normalise(implied(B, A), FreeV, NF, Paths) :- !,
   40    normalise(or(not(A), B), FreeV, NF, Paths).
   41
   42normalise(not(implied(B, A)), FreeV, NF, Paths) :- !,
   43    normalise(not(or(not(A), B)), FreeV, NF, Paths).
   44
   45normalise(conv(implied(B, A)), FreeV, NF, Paths) :- !,
   46    normalise(or(not(conv(A)), conv(B)), FreeV, NF, Paths).
   47
   48% Eliminating equiv
   49
   50normalise(equiv(A, B), FreeV, NF, Paths) :- !,
   51    normalise(not(or(not(or(not(A), B)), not(or(not(B), A)))), FreeV, NF, Paths).
   52
   53normalise(not(equiv(A, B)), FreeV, NF, Paths) :- !,
   54    normalise(or(not(or(not(A), B)), not(or(not(B), A))), FreeV, NF, Paths).
   55
   56normalise(conv(equiv(A, B)), FreeV, NF, Paths) :- !,
   57    normalise(not(or(not(or(not(conv(A)), conv(B))), not(or(not(conv(A)), conv(B))))), FreeV, NF, Paths).
   58
   59% Eliminating box
   60
   61normalise(box(R,A), FreeV, NF, Paths) :- !,
   62    normalise(not(dia(R,not(A))), FreeV, NF, Paths).
   63
   64normalise(not(box(R,A)), FreeV, NF, Paths) :- !,
   65    normalise(dia(R,not(A)), FreeV, NF, Paths).
   66
   67% Eliminating and
   68
   69normalise(and(A,B), FreeV, NF, Paths) :- !,
   70    normalise(not(or(not(A),not(B))), FreeV, NF, Paths).
   71
   72normalise(not(and(A,B)), FreeV, NF, Paths) :- !,
   73    normalise(or(not(A),not(B)), FreeV, NF, Paths).
   74
   75% Eliminating false
   76
   77normalise(false, FreeV, NF, Paths) :- !,
   78    normalise(not(true), FreeV, NF, Paths).
   79
   80normalise(not(false), FreeV, NF, Paths) :- !,
   81    normalise(true, FreeV, NF, Paths).
   82
   83normalise(conv(false), FreeV, NF, Paths) :- !,
   84    normalise(not(true), FreeV, NF, Paths).
   85
   86% Eliminating id
   87% model with p? | -p?
   88
   89normalise(id, FreeV, NF, Paths) :- !,
   90    normalise(or(test('ID'),test(not('ID'))), FreeV, NF, Paths).
   91
   92normalise(dia(id,A), FreeV, NF, Paths) :- !,
   93    normalise(A, FreeV, NF, Paths).
   94
   95normalise(dia(conv(id),A), FreeV, NF, Paths) :- !,
   96    normalise(A, FreeV, NF, Paths).
   97
   98normalise(not(dia(id,A)), FreeV, NF, Paths) :- !,
   99    normalise(not(A), FreeV, NF, Paths).
  100
  101normalise(not(dia(conv(id),A)), FreeV, NF, Paths) :- !,
  102    normalise(not(A), FreeV, NF, Paths).
  103
  104normalise(comp(id,R), FreeV, NF, Paths) :- !,
  105    normalise(R, FreeV, NF, Paths).
  106
  107normalise(comp(R,id), FreeV, NF, Paths) :- !,
  108    normalise(R, FreeV, NF, Paths).
  109
  110normalise(comp(conv(id),R), FreeV, NF, Paths) :- !,
  111    normalise(R, FreeV, NF, Paths).
  112
  113normalise(comp(R,conv(id)), FreeV, NF, Paths) :- !,
  114    normalise(R, FreeV, NF, Paths).
  115
  116normalise(or(conv(id),R), FreeV, NF, Paths) :- !,
  117    normalise(or(id,R), FreeV, NF, Paths).
  118
  119normalise(or(R,conv(id)), FreeV, NF, Paths) :- !,
  120    normalise(or(R,id), FreeV, NF, Paths).
  121
  122normalise(star(id), FreeV, NF, Paths) :- !,
  123    normalise(id, FreeV, NF, Paths).
  124
  125normalise(star(conv(id)), FreeV, NF, Paths) :- !,
  126    normalise(id, FreeV, NF, Paths).
  127
  128normalise(conv(id), FreeV, NF, Paths) :- !,
  129    normalise(id, FreeV, NF, Paths).
  130
  131% Eliminating plus
  132
  133normalise(plus(R), FreeV, NF, Paths) :- !,
  134    normalise(comp(R,star(R)), FreeV, NF, Paths).
  135
  136normalise(conv(plus(R)), FreeV, NF, Paths) :- !,
  137    normalise(conv(comp(R,star(R))), FreeV, NF, Paths).
  138
  139%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  140% Simplification & pushing not inwards
  141
  142% Negation
  143
  144normalise(not(not(A)), FreeV, NF, Paths) :- !,
  145    normalise(A, FreeV, NF, Paths).
  146
  147normalise(not(test(A)), FreeV, NF, Paths) :- !,
  148    normalise(test(not(A)), FreeV, NF, Paths).
  149
  150% Disjunction
  151
  152normalise(or(A, A), FreeV, NF, Paths) :- !,
  153    normalise(A, FreeV, NF, Paths).
  154
  155normalise(or(not(A), A), FreeV, NF, Paths) :- !,
  156    normalise(true, FreeV, NF, Paths).
  157
  158normalise(or(A, not(A)), FreeV, NF, Paths) :- !,
  159    normalise(true, FreeV, NF, Paths).
  160
  161normalise(or(_,true), FreeV, NF, Paths) :- !,
  162    normalise(true, FreeV, NF, Paths).
  163
  164normalise(or(true,_), FreeV, NF, Paths) :- !,
  165    normalise(true, FreeV, NF, Paths).
  166
  167normalise(or(A, not(true)), FreeV, NF, Paths) :- !,
  168    normalise(A, FreeV, NF, Paths).
  169
  170normalise(or(not(true), A), FreeV, NF, Paths) :- !,
  171    normalise(A, FreeV, NF, Paths).
  172
  173normalise(or(test(not(A)), test(A)), FreeV, NF, Paths) :- !,
  174    normalise(test(true), FreeV, NF, Paths).
  175
  176normalise(or(test(A), test(not(A))), FreeV, NF, Paths) :- !,
  177    normalise(test(true), FreeV, NF, Paths).
  178
  179normalise(or(A, test(not(true))), FreeV, NF, Paths) :- !,
  180    normalise(A, FreeV, NF, Paths).
  181
  182normalise(or(test(not(true)), A), FreeV, NF, Paths) :- !,
  183    normalise(A, FreeV, NF, Paths).
  184
  185normalise(or(A, B), FreeV, NF, Paths) :- !,
  186    normalise(A, FreeV, NF1, Paths1),
  187    normalise(B, FreeV, NF2, Paths2),
  188    (Paths1 > Paths2  ->  
  189         OrdNF = or(NF2, NF1);
  190         OrdNF = or(NF1, NF2)),
  191    (A = NF1, B = NF2 ->
  192         (NF = OrdNF,
  193          Paths is Paths1 + Paths2);
  194         normalise(OrdNF, FreeV, NF, Paths)).
  195
  196% not or, i.e. Conjunction
  197
  198normalise(not(or(A, A)), FreeV, NF, Paths) :- !,
  199    normalise(not(A), FreeV, NF, Paths).
  200
  201normalise(not(or(not(A), A)), FreeV, NF, Paths) :- !,
  202    normalise(not(true), FreeV, NF, Paths).
  203
  204normalise(not(or(A, not(A))), FreeV, NF, Paths) :- !,
  205    normalise(not(true), FreeV, NF, Paths).
  206
  207normalise(not(or(A,not(true))), FreeV, NF, Paths) :- !,
  208    normalise(not(A), FreeV, NF, Paths).
  209
  210normalise(not(or(not(true),A)), FreeV, NF, Paths) :- !,
  211    normalise(not(A), FreeV, NF, Paths).
  212
  213normalise(not(or(_, true)), FreeV, NF, Paths) :- !,
  214    normalise(not(true), FreeV, NF, Paths).
  215
  216normalise(not(or(true, _)), FreeV, NF, Paths) :- !,
  217    normalise(not(true), FreeV, NF, Paths).
  218
  219normalise(not(or(A,test(not(true)))), FreeV, NF, Paths) :- !,
  220    normalise(not(A), FreeV, NF, Paths).
  221
  222normalise(not(or(test(not(true)),A)), FreeV, NF, Paths) :- !,
  223    normalise(not(A), FreeV, NF, Paths).
  224
  225normalise(not(or(A, B)), FreeV, NF, Paths) :- !,
  226    normalise(A, FreeV, NF1, Paths1),
  227    normalise(B, FreeV, NF2, Paths2),
  228    (Paths1 > Paths2  ->  
  229         OrdNF = not(or(NF2, NF1));
  230         OrdNF = not(or(NF1, NF2))),
  231    (A = NF1, B = NF2 ->
  232         (NF = OrdNF,
  233          Paths is Paths1 + Paths2);
  234         normalise(OrdNF, FreeV, NF, Paths)).
  235
  236% dia
  237
  238normalise(dia(_,not(true)), FreeV, NF, Paths) :- !,
  239    normalise(not(true), FreeV, NF, Paths).
  240
  241normalise(dia(test(not(true)),_), FreeV, NF, Paths) :- !,
  242    normalise(not(true), FreeV, NF, Paths).
  243
  244normalise(dia(test(true),A), FreeV, NF, Paths) :- !,
  245    normalise(A, FreeV, NF, Paths).
  246
  247normalise(dia(comp(R,S),A), FreeV, NF, Paths) :- !,
  248    normalise(dia(R,dia(S,A)), FreeV, NF, Paths).
  249
  250normalise(dia(or(R,S),A), FreeV, NF, Paths) :- !,
  251    normalise(or(dia(R,A),dia(S,A)), FreeV, NF, Paths).
  252
  253normalise(dia(R,A), FreeV, NF, Paths) :- !,
  254    normalise(R, FreeV, NF1, Paths1),
  255    normalise(A, FreeV, NF2, Paths2),
  256    (R = NF1, A = NF2 ->
  257        (NF = dia(NF1, NF2),
  258            Paths is Paths1 * Paths2);
  259        normalise(dia(NF1, NF2), FreeV, NF, Paths)).
  260
  261% not box, i.e. dia
  262
  263normalise(not(dia(_,not(true))), FreeV, NF, Paths) :- !,
  264    normalise(true, FreeV, NF, Paths).
  265
  266normalise(not(dia(not(true),_)), FreeV, NF, Paths) :- !,
  267    normalise(true, FreeV, NF, Paths).
  268
  269normalise(not(dia(test(true),A)), FreeV, NF, Paths) :- !,
  270    normalise(not(A), FreeV, NF, Paths).
  271
  272normalise(not(dia(comp(R,S),A)), FreeV, NF, Paths) :- !,
  273    normalise(not(dia(R,dia(S,A))), FreeV, NF, Paths).
  274
  275normalise(not(dia(or(R,S),A)), FreeV, NF, Paths) :- !,
  276    normalise(not(or(dia(R,A),dia(S,A))), FreeV, NF, Paths).
  277
  278normalise(not(dia(R,A)), FreeV, NF, Paths) :- !,
  279    normalise(R, FreeV, NF1, Paths1),
  280    normalise(A, FreeV, NF2, Paths2),
  281    (R = NF1, A = NF2 ->
  282        (NF = not(dia(NF1, NF2)),
  283            Paths is Paths1 * Paths2);
  284        normalise(not(dia(NF1, NF2)), FreeV, NF, Paths)).
  285
  286% test
  287
  288%normalise(test(not(true)), FreeV, NF, Paths) :- !,
  289%    normalise(not(true), FreeV, NF, Paths).
  290
  291normalise(test(A), FreeV, NF, Paths) :- !,
  292    normalise(A, FreeV, NF1, Paths1),
  293    (A = NF1 ->
  294        (NF = test(NF1),
  295         Paths = Paths1);    % not sure if this is necessary
  296        normalise(test(NF1), FreeV, NF, Paths)).
  297
  298% not test
  299
  300normalise(not(test(not(true))), FreeV, NF, Paths) :- !,
  301    normalise(test(true), FreeV, NF, Paths).
  302
  303normalise(not(test(A)), FreeV, NF, Paths) :- !,
  304    normalise(A, FreeV, NF1, Paths1),
  305    (A = NF1 ->
  306        (NF = not(test(NF1)),
  307         Paths = Paths1);    % not sure if this is necessary
  308        normalise(not(test(NF1)), FreeV, NF, Paths)).
  309
  310% comp
  311
  312normalise(comp(true,true), FreeV, NF, Paths) :- !,
  313    normalise(true, FreeV, NF, Paths).
  314
  315normalise(comp(_,not(true)), FreeV, NF, Paths) :- !,
  316    normalise(not(true), FreeV, NF, Paths).
  317
  318normalise(comp(not(true),_), FreeV, NF, Paths) :- !,
  319    normalise(not(true), FreeV, NF, Paths).
  320
  321normalise(comp(test(true),R), FreeV, NF, Paths) :- !,
  322    normalise(R, FreeV, NF, Paths).
  323
  324normalise(comp(R,test(true)), FreeV, NF, Paths) :- !,
  325    normalise(R, FreeV, NF, Paths).
  326
  327normalise(comp(_,test(not(true))), FreeV, NF, Paths) :- !,
  328    normalise(test(not(true)), FreeV, NF, Paths).
  329
  330normalise(comp(test(not(true)),_), FreeV, NF, Paths) :- !,
  331    normalise(test(not(true)), FreeV, NF, Paths).
  332
  333normalise(comp(R,S), FreeV, NF, Paths) :- !,
  334    normalise(R, FreeV, NF1, Paths1),
  335    normalise(S, FreeV, NF2, Paths2),
  336    (R = NF1, S = NF2 ->
  337        (NF = comp(NF1, NF2),
  338            Paths is Paths1 * Paths2);
  339        normalise(comp(NF1, NF2), FreeV, NF, Paths)).
  340
  341% not comp
  342
  343normalise(not(comp(true,true)), FreeV, NF, Paths) :- !,
  344    normalise(test(not(true)), FreeV, NF, Paths).
  345
  346normalise(not(comp(_,not(true))), FreeV, NF, Paths) :- !,
  347    normalise(true, FreeV, NF, Paths).
  348
  349normalise(not(comp(not(true),_)), FreeV, NF, Paths) :- !,
  350    normalise(true, FreeV, NF, Paths).
  351
  352normalise(not(comp(test(true),R)), FreeV, NF, Paths) :- !,
  353    normalise(not(R), FreeV, NF, Paths).
  354
  355normalise(not(comp(R,test(true))), FreeV, NF, Paths) :- !,
  356    normalise(not(R), FreeV, NF, Paths).
  357
  358normalise(not(comp(_,test(not(true)))), FreeV, NF, Paths) :- !,
  359    normalise(test(true), FreeV, NF, Paths).
  360
  361normalise(not(comp(test(not(true)),_)), FreeV, NF, Paths) :- !,
  362    normalise(test(true), FreeV, NF, Paths).
  363
  364normalise(not(comp(R,S)), FreeV, NF, Paths) :- !,
  365    normalise(R, FreeV, NF1, Paths1),
  366    normalise(S, FreeV, NF2, Paths2),
  367    (R = NF1, S = NF2 ->
  368        (NF = not(comp(NF1, NF2)),
  369            Paths is Paths1 + Paths2);
  370        normalise(not(comp(NF1, NF2)), FreeV, NF, Paths)).
  371
  372% star
  373
  374normalise(star(not(true)), FreeV, NF, Paths) :- !,
  375    normalise(test(not(true)), FreeV, NF, Paths).
  376
  377normalise(star(true), FreeV, NF, Paths) :- !,
  378    normalise(test(true), FreeV, NF, Paths).
  379
  380normalise(star(test(not(true))), FreeV, NF, Paths) :- !,
  381    normalise(test(not(true)), FreeV, NF, Paths).
  382
  383normalise(star(test(true)), FreeV, NF, Paths) :- !,
  384    normalise(test(true), FreeV, NF, Paths).
  385
  386normalise(star(A), FreeV, NF, Paths) :- !,
  387    normalise(A, FreeV, NF1, Paths1),
  388    (A = NF1 ->
  389        (NF = star(NF1),
  390         Paths = Paths1);    % not sure if this is necessary
  391        normalise(star(NF1), FreeV, NF, Paths)).
  392
  393% conv
  394
  395normalise(conv(R), FreeV, NF, Paths) :- !,
  396    normalise(R, FreeV, NF1, Paths1),
  397    (R = NF1 ->
  398        (NF = conv(NF1),
  399         Paths = Paths1);    % not sure if this is necessary
  400        normalise(conv(NF1), FreeV, NF, Paths)).
  401
  402%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  403% Literals
  404
  405normalise(Lit, _, Lit, 1)