1/* ************************************************************** */
    2/* Operators                                                      */
    3/* ************************************************************** */
    4
    5/*  propositional operators are: */
    6
    7:-op(140, fy, ~).    8:-op(160, xfy, and).    9:-op(160, xfy, or).   10:-op(180, xfy, =>).   11
   12/*  unary temporal operators are: */
   13
   14:-op(140, fy, sometimes).   15:-op(140, fy, always).   16:-op(140, fy, next).   17
   18/*  binary temporal operators are: */
   19
   20:-op(160, xfy, until).   21:-op(160, xfy, unless).   22
   23/*  knowledge operator: */
   24
   25:-op(140, fy, k).   26
   27/**********************************************/
   28/*                                            */
   29/*  Modal Literals                            */
   30/*                                            */
   31/**********************************************/
   32
   33is_new(new(_)).
   34
   35is_snl_literal(unknown(_)).
   36
   37is_snl_literal(~ unknown(_)).
   38
   39is_modal(k L):-
   40  is_literal(L).
   41
   42is_modal(~ k L):-
   43  is_literal(L).
   44
   45is_modal_literal(L):-
   46  is_modal(L).
   47
   48is_modal_literal(L):-
   49  is_literal(L).
   50
   51/*****************************************************************************/
   52/* is_literal(X).                                                            */
   53/*                                                                           */
   54/* Returns true if X is a proposition or negation of a proposition.          */
   55/*****************************************************************************/
   56
   57is_literal([_]):- !,fail.       % The exclusion of lists is needed for some predicates 
   58                                % in ntempres.pl (eg includes_or).
   59is_literal([_|_]):-!,fail.
   60
   61is_literal(~ X):-
   62  is_literal(X).
   63
   64is_literal(X):-
   65  is_proposition(X).
   66
   67is_literal(X):-
   68  is_constant(X).
   69
   70is_not_literal(~ X):- !,
   71   is_not_proposition(X).
   72
   73is_not_literal(X):-
   74   is_not_proposition(X).
   75
   76
   77/**********************************************/
   78/*                                            */
   79/* Constants                                  */
   80/*                                            */
   81/**********************************************/
   82
   83is_constant(true).
   84is_constant(false).
   85is_constant(start).
   86
   87/*****************************************************************************/
   88/* is_proposition(X).                                                        */
   89/*                                                                           */
   90/* Returns true if X is a proposition.                                       */
   91/*****************************************************************************/
   92
   93is_proposition(Formula) :- 
   94   \+(is_not_proposition(Formula)).
   95
   96/*****************************************************************************/
   97/* is_not_proposition(X).                                                    */
   98/*                                                                           */
   99/* Returns true if X is not a proposition ie. X is a formula which includes  */
  100/* temporal operators, boolean operators, or are true or false.              */
  101/*****************************************************************************/
  102
  103is_not_proposition([]).
  104is_not_proposition(X) :- is_constant(X).
  105is_not_proposition(_ and _).
  106is_not_proposition(_ or _).
  107is_not_proposition(~ _).
  108is_not_proposition(sometimes _).
  109is_not_proposition(always _).
  110is_not_proposition(_ => _).
  111is_not_proposition(next _).
  112is_not_proposition(k _).
  113is_not_proposition(_ until _).
  114is_not_proposition(_ unless _).
  115
  116/*****************************************************************************/
  117/*  conjunctive(X) :- X is an alpha formula                                  */
  118/*                                                                           */
  119/*****************************************************************************/
  120
  121conjunctive(_ and _).
  122conjunctive(~(_ or _)).
  123conjunctive(~(_ => _)).
  124
  125/*****************************************************************************/
  126/* disjunctive(X) :- X is a beta formula                                     */
  127/*                                                                           */
  128/*****************************************************************************/
  129
  130disjunctive(~(_ and _)).
  131disjunctive(_ or _).
  132disjunctive(_ => _).
  133
  134/**********************************************/
  135/*                                            */
  136/*  Counters: definitions, functions          */
  137/*                                            */
  138/**********************************************/
  139
  140/* for renaming predicates */
  141
  142:-dynamic predcount/1. /* for sicstus only */
  143
  144/* for skolem functions/constants */
  145
  146:-dynamic rulecount/1. /* for sicstus only */
  147
  148:-dynamic clear/0.     /* for sicstus only */
  149
  150/* predcount(N) :- N is the current Skolem function index */
  151
  152predcount(1).
  153rulecount(1).
  154
  155clear :-retract(predcount(_)), 
  156        assert(predcount(1)).
  157
  158
  159/*****************************************************************************/
  160/*        newpredcount(N)                                                    */
  161/*                                                                           */
  162/*        N is the current new predicate index, and as a                     */
  163/*        side effect, the remembered value is incremented.                  */
  164/*                                                                           */
  165/*****************************************************************************/
  166
  167newpredcount(N) :- predcount(N),
  168	           retract(predcount(N)),
  169		   M is N+1,
  170		   assert(predcount(M)).
  171
  172startrulecount(N) :- rulecount(N),
  173                     retract(rulecount(N)),
  174                     assert(rulecount(1)).
  175startrulecount(1).
  176
  177newrulecount(N) :- rulecount(N),
  178	          retract(rulecount(N)),
  179		  M is N+1,
  180		  assert(rulecount(M)).
  181
  182/********************************************************/
  183/* New propositions                                     */
  184/********************************************************/
  185
  186new_temp_prop(V):- newpredcount(N),
  187                   term_to_atom(N,NN),
  188                   string_concat('tmpp',NN,NV),
  189                   atom_to_term(NV,V,_).
  190
  191new_dontknow_prop(X,X):- is_snl_literal(X).
  192new_dontknow_prop(V,X):- V=.. [unknown|[X]].
  193
  194new_conj_prop(V,true):-V=[true].
  195new_conj_prop(V,X):- V=.. [new|[X]].
  196
  197/* ************************************************************** */
  198/* OUTPUT UTILITIES FOR CLAUSES                                   */
  199/* ************************************************************** */
  200
  201/* Remove comments if you do not wish a very verbose output */
  202
  203% my_writef(_X,_Y):-true,!.
  204% my_write(_X):-true,!.
  205% write_ruleset(_X):-true,!.
  206
  207/* For very verbose output */
  208
  209 my_writef(X,Y):-writef(X,Y).
  210 my_write(X):-write(X).
  211
  212/* ************************************************************** */
  213/* Formatted output of the prover: lists of clauses               */
  214/* ************************************************************** */
  215
  216write_ruleset((Initial,Literal,Modal,Temporal)) :-
  217        nl,write('Initial Clauses'),nl, 
  218	write('['), nl, write_ruleset1(Initial),!, write(']'), nl,
  219        nl,write('Literal Clauses'),nl, 
  220	write('['), nl, write_ruleset1(Literal),!, write(']'), nl,
  221        nl,write('Modal Clauses'),nl, 
  222	write('['), nl, write_ruleset1(Modal),!, write(']'), nl,
  223        nl,write('Temporal Clauses'),nl, 
  224	write('['), nl, write_ruleset1(Temporal),!, write(']'), nl.
  225
  226write_ruleset(Ruleset) :- 
  227	write('['), nl, write_ruleset1(Ruleset),!, write(']'), nl.
  228
  229write_ruleset1([Rule | Rest]) :- 
  230	write('  '), write_form(Rule), nl, write_ruleset1(Rest).
  231
  232write_ruleset1([]).
  233
  234/* ************************************************************** */
  235/* Formatted output of the prover: clauses                        */
  236/* ************************************************************** */
  237
  238write_form(r(X,Y,false)) :- 
  239        write(X), 
  240        write(' '), 
  241        write(Y), 
  242        write(' '), 
  243        write(' false ').
  244
  245write_form(r(X,Y,P)) :-
  246        write(X), 
  247        write(' '), 
  248        write(Y), 
  249        write(' '), 
  250        write_form(P).
  251
  252write_form(P => F) :- 
  253        write_form(P), 
  254        write(' => '), 
  255        write_form(F).
  256
  257%write_form(neg X) :- write('~'), !, write_form(X).
  258write_form(~ X) :- 
  259        write('~'), !, 
  260        write_form(X).
  261write_form(- X) :- 
  262        write('~'), !, 
  263        write_form(X).
  264
  265
  266write_form(X and Y) :-
  267	write('('),
  268	!,
  269	write_form(X), 
  270	write(' & '),
  271	write_form(Y),
  272	write(')').
  273
  274write_form(X or Y) :- 
  275	write('('),
  276	!,
  277	write_form(X),
  278	write(' | '),
  279	write_form(Y),
  280	write(')').
  281
  282write_form(X until Y) :- 
  283	write('('),
  284	!,
  285	write_form(X),
  286	write(' U '),
  287	write_form(Y),
  288	write(')').
  289
  290write_form(X unless Y) :- 
  291	write('('),
  292	!,
  293	write_form(X),
  294	write(' W '),
  295	write_form(Y),
  296	write(')').
  297
  298write_form(next X) :- write('O'), !, write_form(X).
  299write_form(sometimes X) :- write('<>'), !, write_form(X).
  300write_form(always X) :- write('[]'), !, write_form(X).
  301write_form(k X) :- write('k'), !, write_form(X).
  302write_form(new(X)) :- write('new('),!,write_form(X),write(')').
  303write_form(unknown(X)) :- write('unknown('),!,write_form(X),write(')').
  304write_form(X) :- write(X).
  305
  306
  307/**********************************************************************/
  308/* write_otter_rules(Rules)                                           */
  309/*                                                                    */
  310/* Takes a list of clauses (Rules) of the Prolog form r(No,List,Rule) */
  311/* where Rule is true => F or P => next F and rewrites              */
  312/* them in an Otter format i.e. if F is a or b in the above two rules */
  313/* the first rules would be output as s_a | s_b. and the second as    */
  314/* -slast_P | s_a | s_b.                                              */
  315/*                                                                    */
  316/**********************************************************************/
  317
  318write_otter_rules(X,Y,Z):-
  319  write_otter_rules(X),
  320  write_otter_rules(Y),
  321  write_otter_rules(Z).
  322
  323write_otter_rules(X,Y):-
  324  write_otter_rules(X),
  325  write_otter_rules(Y).
  326
  327write_otter_rules([]).
  328
  329write_otter_rules([r(_,_,Rule)|RRest]):-
  330  write_otter_rule(Rule),
  331  write_otter_rules(RRest).
  332
  333write_otter_rules([Rule|RRest]):-
  334  write_otter_rule(Rule),
  335  write_otter_rules(RRest).
  336
  337/**********************************************************************/
  338/* write_otter_rule(Rule)                                             */
  339/*                                                                    */
  340/* Takes a claue (Rule) of the Prolog form r(No,List,Rule) where Rule */
  341/* is true => F or P => next F and rewrites them in an              */
  342/* Otter format i.e. if F is a or b in the above two rules the first  */
  343/* rules would be output as s_a | s_b.                                */
  344/* and the second as -slast_P | s_a | s_b.                            */
  345/*                                                                    */
  346/**********************************************************************/
  347
  348write_otter_rule(B):-
  349  disjunction_of_literals(B),!,
  350  write_otter_disjunct(B),
  351  write('.'),nl.
  352
  353write_otter_rule(A => next B):-
  354  write_otter_conjunct(A),
  355  write(' | '),
  356  write_otter_disjunct(B),
  357  write('.'),nl.
  358
  359/**********************************************************************/
  360/* write_otter_conjunct(Conj)                                         */
  361/*                                                                    */
  362/* Takes a literal or conjunction of literals (Conj) of the Prolog    */
  363/* form a and b and c from the lhs of global rules and rewrites them  */
  364/* as -slast_a | -slast_b | -slast_c.                                 */
  365/*                                                                    */
  366/**********************************************************************/
  367
  368write_otter_conjunct(false):-
  369  write('$F').
  370
  371write_otter_conjunct(tmp_p(X)):-
  372  write('-slast_tmp_p_'),
  373  write(X).
  374
  375write_otter_conjunct(~ A):-
  376  write('-slast_neg_'),
  377  write(A).
  378
  379write_otter_conjunct(new(X)):-
  380  trace,
  381  write('-slast_new_'),
  382  write_otter_and_proposition(X).
  383
  384write_otter_conjunct(unknown(X)):-
  385  write('-slast_nkn_'),
  386  write_otter_proposition(X).
  387
  388write_otter_conjunct(A):-
  389  is_literal(A),
  390  write('-slast_'),
  391  write(A).
  392
  393write_otter_conjunct(A and B):-
  394  write_otter_conjunct(A),
  395  write(' | '),
  396  write_otter_conjunct(B).
  397
  398
  399/**********************************************************************/
  400/* write_otter_disjunct(Disj)                                         */
  401/*                                                                    */
  402/* Takes a literal or disjunction of literals (Disj) of the Prolog    */
  403/* form a or b or ~ c from the rhs of step clauses and rewrites them*/
  404/* as s_a | s_b | -s_c. We are assuming the disjunct is from the rhs  */
  405/* of a step clause or a literal clause.                              */
  406/*                                                                    */
  407/**********************************************************************/
  408
  409write_otter_disjunct(false):-
  410  write('$F').
  411
  412write_otter_disjunct(~ A):-
  413  write('-'),
  414  write_otter_disjunct(A).
  415
  416write_otter_disjunct(tmp_p(X)):-
  417  write('s_tmp_p_'),
  418  write(X).
  419
  420write_otter_disjunct(new(X)):-
  421  write('s_new_'),
  422  write_otter_and_proposition(X).
  423
  424write_otter_disjunct(unknown(X)):-
  425  write('s_nkn_'),
  426  write_otter_proposition(X).
  427
  428write_otter_disjunct(A):-
  429  is_literal(A),
  430  write('s_'),
  431  write(A).
  432
  433write_otter_disjunct(A or B):-
  434  write_otter_disjunct(A),
  435  write(' | '),
  436  write_otter_disjunct(B).
  437
  438/*********************************************/
  439/* Write the different kind of propositions  */
  440/* in the Otter format                       */
  441/*********************************************/
  442
  443write_otter_proposition(~ X):-
  444  write('neg_'),
  445  write_otter_proposition(X).
  446
  447write_otter_proposition(new(X)):-
  448  write('new_'),
  449  write_otter_and_proposition(X).
  450
  451write_otter_proposition(unknown(X)):-
  452  write('nkn_'),
  453  write_otter_proposition(X).
  454
  455write_otter_proposition(X):-
  456  is_literal(X),
  457  write(X).
  458
  459/************************************************/
  460/* The following is needed in order to write    */
  461/* the conjunctions that label the propositions */
  462/* that rename conjunctions                     */
  463/************************************************/
  464
  465write_otter_and_proposition(tmp_p(X) and B):-
  466  write_otter_and_proposition(B and tmp_p(X)).
  467
  468write_otter_and_proposition(A and B):-
  469  write_otter_and_proposition(A),
  470  write('_'),
  471  write_otter_and_proposition(B).
  472
  473write_otter_and_proposition(A):-
  474  write_otter_proposition(A).
  475
  476/*****************************************************************************/
  477/* write_list(ERulePaths)                                                    */
  478/*                                                                           */
  479/* Takes a list comprising of eventualites paired with a list of loop paths  */
  480/* already found (ERulePaths). It writes out the eventuality and the paths   */
  481/* already found.                                                            */
  482/*****************************************************************************/
  483
  484write_list([]).
  485
  486write_list([[Rule,Path]|Rest]):-
  487   write('     ['),
  488   write_form(Rule),
  489   write(', '),
  490   write(Path),
  491   write('     ]\n'),
  492   write_list(Rest).
  493
  494
  495/*****************************************************************************/
  496/*  number_rules(RuleList,FromList,NewRuleList).                             */
  497/*                                                                           */
  498/*  Takes the Rulelist and makes it into the format Number,From,Text)        */
  499/*  and stuffs it in NewRuleList.                                            */
  500/*****************************************************************************/
  501
  502number_rules([],_FromList,[]):-!.
  503
  504number_rules([Rule|Rest],FromList,[NewRule|NewRest]):-
  505   number_rule(Rule,FromList,NewRule),
  506   number_rules(Rest,FromList,NewRest).
  507
  508number_rule(r(N1,N2,Clause),_,r(N1,N2,Clause)).
  509number_rule(Rule,FromList,r(N,FromList,Rule)):-
  510   newrulecount(N).
  511
  512/****************************************************************************/
  513/*                                                                          */
  514/* because of the new normal form, modal subsumption takes place if:        */
  515/*                                                                          */
  516/* (1) a modal literal is implied by true                                   */
  517/* (2) the clauses are exactly the same                                     */
  518/* (3) a literal clause is a unit clause                                    */
  519/*     and the negated literal is the antecedent of the modal clause        */
  520/*                                                                          */
  521/****************************************************************************/
  522
  523dis_implies(true => B, _C => B):-!.
  524dis_implies(_A => B, true => B):-!.
  525dis_implies(A => B, A => B):-!.
  526
  527/* 
  528   this only fails: 
  529   cut introduced to prevent redo 
  530   there will never be a modal literal in a literal clause 
  531*/
  532
  533dis_implies(_A => _B, _C):-fail,!.
  534
  535dis_implies(A, NegA => _C):-
  536  is_literal(A),!,
  537  snff_negate(A,NegA).
  538
  539/* literal subsumption takes place as usual */
  540
  541dis_implies(A,B):-!,
  542  list_strip_or(A,A1),
  543  list_strip_or(B,B1),
  544  subset(A1,B1).
  545
  546/***************************************************/
  547   
  548set_implies([],_):-!.
  549
  550set_implies(X,X):-!.
  551
  552set_implies(_,[[true]]):-!.
  553
  554set_implies(_,[true]):-!.
  555
  556set_implies([[false]],_):-!.
  557
  558set_implies([false],_):-!.
  559
  560set_implies([H|Tail],[H1]):-
  561    is_literal(H1),
  562    is_literal(H),!,
  563    member(H1,[H|Tail]).
  564
  565set_implies([H1|Tail1],[H2|Tail2]):-
  566    is_literal(H1),
  567    is_literal(H2),!,
  568    subset([H2|Tail2],[H1|Tail1]).
  569
  570set_implies([H1],[H|Tail]):-
  571    is_modal_literal(H1),
  572    is_modal_literal(H),!,
  573    modal_member(H1,[H|Tail]).
  574
  575set_implies([H1|Tail1],[H2|Tail2]):-
  576    is_modal_literal(H1),
  577    is_modal_literal(H2),!,
  578    modal_subset([H1|Tail1],[H2|Tail2]).
  579
  580set_implies([H1],[H2|Tail2]):-
  581    is_literal(H1),!,
  582    is_superset_of_member_of_list([H1],[H2|Tail2]).
  583
  584set_implies([H1|Tail1],[H2|Tail2]):-
  585    is_literal(H1),!,
  586    is_superset_of_member_of_list([H1|Tail1],[H2|Tail2]).
  587
  588set_implies([H1|Tail1],[H2|Tail2]):-
  589    is_literal(H2),!,
  590    set_implies(H1,[H2|Tail2]),
  591    set_implies(Tail1,[H2|Tail2]).
  592
  593set_implies([H1|List1],List2):-
  594    set_implies(H1,List2),
  595    set_implies(List1,List2).
  596
  597/*******************************************************************************/
  598/* strip(Clause, List)                                                         */
  599/*                                                                             */
  600/*   This predicate removes all ands or ors from the clause (they should be    */
  601/*   all ands or all ors) and sticks remaining propositions in a list.         */
  602/*******************************************************************************/
  603
  604strip(X or Y, AList):-
  605   strip(X, XList),
  606   strip(Y, YList),
  607   append(XList, YList, AList), !. % Added cuts to stop choosing alternative rules on failure
  608
  609strip(X and Y, AList):-
  610   strip(X, XList),
  611   strip(Y, YList),
  612   append(XList, YList, AList), !. % Added cuts to stop choosing alternative rules on failure
  613
  614strip(X, [X]).
  615
  616/******************************************************************************/
  617
  618list_strip_or(X or Y,NewXY):-
  619  list_strip_or(X,NewX),
  620  list_strip_or(Y,NewY),
  621  append(NewX,NewY,NewXY),!.
  622
  623list_strip_or(X,[NewX]):-
  624  simplify_and(X,NewX).
  625
  626/*******************************************************************************/
  627/* strip_or(Clause, List)                                                      */
  628/*                                                                             */
  629/*   This predicate removes all ands or ors from Clause which is disjunctive   */
  630/*   and puts them on a bracketed List eg (a and b) or c would be [[a,b],[c]]  */
  631/*******************************************************************************/
  632
  633strip_or(X or Y, NewXY):-
  634  strip_or(X, NewX),
  635  strip_or(Y, NewY),
  636  append(NewX, NewY, NewXY),!.
  637
  638strip_or(X and Y, [NewXY]):-
  639   strip(X and Y, NewXY),!.
  640
  641strip_or(X,[[X]]) :- !.
  642
  643/*******************************************************************************/
  644/* strip_and(Clause, List)                                                     */
  645/*                                                                             */
  646/*   This predicate removes all ands or ors from Clause which is disjunctive   */
  647/*   and puts them on a bracketed List eg (a and b) or c would be [[a,b],[c]]  */
  648/*******************************************************************************/
  649
  650strip_and(X and Y, NewXY):-
  651  strip_and(X, NewX),
  652  strip_and(Y, NewY),
  653  append(NewX, NewY, NewXY),!.
  654
  655strip_and(X or Y, [NewXY]):-
  656   strip(X or Y, NewXY),!.
  657
  658strip_and(X,[[X]]) :- !.
  659
  660/**************************************************************************/
  661
  662member_of_2nd_is_subset_of_1st([],List1,[_|Tail2]):-
  663    member_of_2nd_is_subset_of_1st(List1,List1,Tail2),!.
  664
  665member_of_2nd_is_subset_of_1st([H1|_],_,[H2|_]):-
  666    subset(H2,H1),!.
  667
  668member_of_2nd_is_subset_of_1st([_|Tail1],List1, [H2|Tail2]):-
  669    member_of_2nd_is_subset_of_1st(Tail1,List1, [H2|Tail2]),!.
  670
  671/********************************************************************************/
  672
  673modal_subset([],_):-!.
  674
  675modal_subset(X, X):-!.
  676
  677modal_subset([H |Tail], BList) :-
  678   modal_member(H, BList),!,
  679   modal_subset(Tail, BList).
  680
  681/* modal_member(Item, List) :- Item occurs in List. */
  682/* Note X must be instantiated for this to work otherwise we will just
  683   return the head of our clause.
  684*/
  685
  686modal_member(X, [X | _]):- !.
  687
  688modal_member(X, [sometimes X|_]):- !.
  689
  690modal_member(X, [~ always ~ X|_]):- !.
  691
  692modal_member(X, [_ | Tail]) :- modal_member(X, Tail).
  693
  694/* ******************
  695   * SIMPLIFICATION *
  696   ****************** */
  697
  698/******************************************************************************/
  699/*   simplify(Rules, NewRules)                                                */
  700/*                                                                            */
  701/*  Looks at every rule in Rules and performs standard simplification ie.     */
  702/*            1. replacing a conjunction with complementary literals by false */
  703/*            2. replacing a disjunction with complementary literals by true  */
  704/*            3. removing true from a list of conjuncts                       */
  705/*            4. removing false from a list of conjuncts                      */
  706/******************************************************************************/
  707
  708simplify([],[]).
  709simplify([Rule | Rest], NewRules) :-
  710	simplify_rule(Rule, SRule),
  711	simplify(Rest, NewRest),
  712	append(SRule, NewRest, NewRules).
  713
  714/*****************************************************************************/
  715/* simplify_rule (Rule, NewRules)                                            */
  716/*                                                                           */ 
  717/* Performs various simplifications on Rule. These are                       */
  718/*   - dealing with true and false in conjunctions/disjunctions              */
  719/*   - removing duplicate literals                                           */
  720/*   - dealing with complemetary literals                                    */
  721/*   - getting rid of rules which are always true                            */
  722/*   - expanding rules of the form slast P => false                         */
  723/*****************************************************************************/
  724
  725simplify_rule(r(N1,N2,X => Y),[r(N1,N2,NewR)]):-
  726        is_modal_rule(X => Y),
  727        snff_negate(X, NegX),
  728        simplify_rule(r(N1,N2,NegX or Y),[r(N1,N2,R)]),
  729        change_form(R,[NewR]).
  730
  731simplify_rule(r(N1,N2,R), FinalSet) :-
  732	simplify_true_false(R,U),
  733	remove_true_rules(r(N1,N2,U),RuleSet),   % Ruleset can either be empty, 
  734                                                 % or the single rule as a list
  735	expand_false_rules(RuleSet, FinalSet).   
  736
  737/*****************************************************************************/
  738/*  simplify_rule(Rule, NewRule)                                             */ 
  739/*                                                                           */ 
  740/*  Simplifies Rule by                                                       */
  741/*   - dealing with true and false in conjunctions/disjunctions              */
  742/*   - removing duplicate literals                                           */
  743/*   - dealing with complemetary literals                                    */
  744/*****************************************************************************/
  745
  746simplify_true_false(P => next F, NewP => next NewF ) :-
  747        simplify_and(P, NewishP),
  748        simplify_and_dup(NewishP, NewP),
  749	simplify_or(F,NewishF),
  750        simplify_or_dup(NewishF, NewList),
  751        disjoin(NewList,NewF).
  752
  753simplify_true_false(F, NewF) :-
  754        disjunction_of_modal_literals(F),
  755	simplify_or(F,NewishF),
  756        simplify_or_dup(NewishF, NewerF),
  757        simplify_or_modal(NewerF,NewList),
  758        disjoin(NewList, NewF).
  759
  760/***********************************************************************/
  761/*    simplify_and(Conj,NewConj)                                       */
  762/*                                                                     */ 
  763/*   Takes a conjunction Conj and if true is a conjunct it removes it  */
  764/*   or if false is a conjunct false is returned in NewConj, otherwise */
  765/*   NewConj returns what is left.                                     */
  766/***********************************************************************/
  767
  768simplify_and(A and true, NewA) :- simplify_and(A, NewA),!.
  769
  770simplify_and(true and A, NewA) :- simplify_and(A, NewA),!.
  771
  772simplify_and(_ and false, false):-!.
  773
  774simplify_and(false and _, false):-!.
  775
  776simplify_and(A and _, false) :- simplify_and(A, false),!.
  777
  778simplify_and(_ and B, false) :- simplify_and(B, false),!.
  779
  780simplify_and(A and B, NewB) :- 
  781	simplify_and(A, true),!,
  782	simplify_and(B, NewB).
  783
  784simplify_and(A and B, NewA) :- 
  785	simplify_and(B, true),!,
  786	simplify_and(A, NewA).
  787
  788simplify_and(A and B, NewA and NewB) :- 
  789	simplify_and(A, NewA),
  790	simplify_and(B, NewB),!.
  791
  792simplify_and(~ ~ P, NewP):-
  793        simplify_and(P, NewP).
  794
  795simplify_and(~ true,false).
  796
  797simplify_and(~ false,true).
  798
  799simplify_and(P, P).
  800
  801
  802/*************************************************************************/
  803/*  simplify_and_dup(OldConj,NewConj)                                    */
  804/*                                                                       */ 
  805/*   Takes a conjunction, removes and duplicate literals or              */
  806/*   complementary literals and returns the remaining conjunction in     */
  807/*   NewConj.                                                            */
  808/*************************************************************************/
  809
  810simplify_and_dup(A, false):-   % If we have complementary literals in a conjunct return false
  811   strip(A, AList),
  812   comp_lits_and(AList),!.
  813
  814simplify_and_dup(A, NewA):-
  815   strip(A, AList),
  816   remove_duplicate(AList, NewList),
  817   conjoin(NewList, NewA).
  818
  819/***********************************************************************/
  820/*  remove_duplicate(List, NewList)                                    */
  821/*                                                                     */ 
  822/*  Takes a list of nodes (List) of the form [a,b,c,d] and returns a   */
  823/*  second list with any duplicates removed.                           */
  824/***********************************************************************/
  825
  826remove_duplicate(false,false):- !.
  827
  828remove_duplicate(List1,List2):-
  829  list_to_set(List1,List2).
  830
  831
  832/***********************************************************************/
  833/*    simplify_or(Disj,NewDisj)                                        */
  834/*                                                                     */ 
  835/*   Takes a disjunction Disj and if false is a disjunct it removes it */
  836/*   or if true is a disjunct true is returned in NewDisj, otherwise   */
  837/*   NewDisj returns what is left.                                     */
  838/***********************************************************************/
  839
  840simplify_or(A or false, NewA) :- simplify_or(A, NewA).
  841
  842simplify_or(false or A, NewA) :- simplify_or(A, NewA).
  843
  844simplify_or(_ or true, true).
  845
  846simplify_or(true or _, true).
  847
  848simplify_or(A or _, true) :- simplify_or(A, true).
  849
  850simplify_or(_ or B, true) :- simplify_or(B, true).
  851
  852simplify_or(A or B, NewB) :- 
  853	simplify_or(A, false),
  854	simplify_or(B, NewB).
  855
  856simplify_or(A or B, NewA) :- 
  857	simplify_or(B, false),
  858	simplify_or(A, NewA).
  859
  860simplify_or(A or B, NewA or NewB) :- 
  861	simplify_or(A, NewA),
  862	simplify_or(B, NewB).
  863
  864simplify_or(~ ~ P, NewP):-
  865        simplify_or(P,NewP).
  866
  867simplify_or(~ true,false).
  868
  869simplify_or(~ false,true).
  870
  871simplify_or(P, P).
  872
  873/*************************************************************************/
  874/*  simplify_or_dup(OldDisj,NewDisj)                                     */
  875/*                                                                       */ 
  876/*   Takes a disjunction, OldDisj removes and duplicate literals, deals  */
  877/*   with complementary literals and returns the remaining disjunction   */
  878/*   in NewDisj.                                                         */
  879/*************************************************************************/
  880
  881simplify_or_dup(A, [true]):-        % If we have complementary literals in a disjunct return true.
  882   strip(A, AList),
  883   check_comp_lits(AList).
  884
  885simplify_or_dup(A, [true]):-        % If we have complementary literals in a disjunct return true.
  886   strip(A, AList),
  887   check_modal_lits(AList).
  888
  889simplify_or_dup(A, NewList):-
  890   strip(A, AList),
  891   remove_duplicate(AList, NewList).
  892
  893/****************************************************/
  894
  895check_comp_lits(AList):-
  896   comp_lits_and(AList).
  897
  898/***************************************************/
  899
  900check_modal_lits(AList):-
  901   modal_lits_and(AList).
  902
  903/**************************************************/
  904
  905simplify_or_modal([],[]):-!.
  906
  907simplify_or_modal([~ k ~ L|Rest],[~ k ~ L |Final]):-
  908   remove_member(L,Rest, NewerRest), !,          % Because p -> ~K~p
  909   remove_member(k L,NewerRest, NewestRest),     % Because K p -> p
  910   simplify_or_modal(NewestRest,Final).         
  911
  912simplify_or_modal([k L|Rest],Final):-
  913   member(L,Rest), !,                            % Because K p -> p
  914   simplify_or_modal(Rest,Final).            
  915
  916simplify_or_modal([k L|Rest],Final):-
  917   member(~ k ~ L,Rest), !,                  % Because K p -> ~K~p
  918   simplify_or_modal(Rest,Final).            
  919
  920simplify_or_modal([k L|Rest],[k L|Final]):-
  921   simplify_or_modal(Rest,Final).            
  922
  923simplify_or_modal([L|Rest],Final):-
  924   member(~ k ~ L,Rest), !,            % Because p -> ~K~p
  925   remove_member(k L,Rest, NewerRest),     % Because K p -> p
  926   simplify_or_modal(NewerRest,Final).            
  927
  928simplify_or_modal([L|Rest],[L|Final]):-
  929   remove_member(k L,Rest, NewerRest),     % Because K p -> p
  930   simplify_or_modal(NewerRest,Final).            
  931
  932simplify_or_modal([L|Rest],[L|Final]):-
  933   simplify_or_modal(Rest,Final).
  934
  935/**********************************************/
  936
  937comp_lits(X,Y):-
  938  negate_modal_lit(X,Y).
  939
  940/***************************************************************/
  941/*  comp_lits_and(List)                                        */
  942/*                                                             */ 
  943/* Returns true if complementary literals are found in List    */
  944/***************************************************************/
  945
  946comp_lits_and([H|Tail]):-
  947    negate_modal_lit(H, NegH),
  948    member(NegH,Tail).
  949
  950comp_lits_and([_|Tail]):-
  951  comp_lits_and(Tail).
  952
  953/**************************************************************/
  954
  955modal_lits_and([sometimes X|List]):- !,
  956  negate_modal_lit(X,NegX),
  957  member(NegX,List).
  958
  959modal_lits_and([always _|List]):- !,
  960  modal_lits_and(List).
  961
  962modal_lits_and([X|List]):- !,
  963  negate_modal_lit(X,NegX),
  964  member(sometimes NegX,List).
  965
  966modal_lits_and([_|List]):- !,
  967   modal_lits_and(List).
  968
  969/***************************************************************/
  970/*  comp_lits_or(List)                                         */
  971/*                                                             */ 
  972/* Returns true if complementary literals are found in List    */
  973/***************************************************************/
  974
  975comp_lits_or([H|Tail]):-
  976     negate_all(H, NegH),
  977     node_is_member_of(NegH,Tail).
  978
  979comp_lits_or([_|Tail]):-
  980  comp_lits_or(Tail).
  981
  982/***************************************************************/
  983/*  negate_all(OldList,NewList)                                */
  984/*                                                             */ 
  985/* Negate all takes a list OldList which represents part of a  */
  986/* disjunct and negates all its members which are returned in  */
  987/* NewList.                                                    */
  988/***************************************************************/
  989
  990negate_all([],[]).
  991
  992negate_all([H|Tail],[NegH|NewTail]):-
  993   negate_modal_lit(H, NegH),
  994   negate_all(Tail,NewTail).
  995
  996/*****************************************************************/
  997/* remove_true_rules(Rule,NewRule)                               */
  998/*                                                               */
  999/* Takes a rule in the form r(Number,FromList,Text) and if it is */
 1000/* always true ie of the form ...=> next true                   */
 1001/*                       or   ...=> true                        */
 1002/* NewRule is return with the Text set to [], otherwise the rule */
 1003/* is returned as it is.                                         */
 1004/*****************************************************************/
 1005
 1006remove_true_rules( r(N1,N2,_ => true), r(N1,N2,[])).
 1007remove_true_rules( r(N1,N2,_ => next true), r(N1,N2,[])).
 1008remove_true_rules( r(N1,N2,true),r(N1,N2,[])).
 1009remove_true_rules( R, [R] ).
 1010
 1011/**********************************************************************/
 1012/*  expand_false_rules(Rules, NewRules)                               */
 1013/*                                                                    */
 1014/* Takes the ruleset ie rules to be simplified which is currently     */
 1015/* either a rule of the form r(_,_,[]) ie the text bit is empty as    */
 1016/* rule has been removed as it is always true or it is a list with a  */
 1017/* single rule in. If the rule is of the form                         */
 1018/*               P => next false                                     */
 1019/* then this is rewritten into two new rules                          */
 1020/*               true => next ~P                                     */
 1021/*               start => ~P                                         */
 1022/* The FromList of the original rule is just copied into the FromList */
 1023/* of these two new rules to avoid having to save the rule which is   */
 1024/* going to disappear. Otherwise the rule remains as it is.           */
 1025/**********************************************************************/
 1026
 1027expand_false_rules(r(_,_,[]),[]):-!.
 1028
 1029expand_false_rules([],[]):-!.
 1030
 1031expand_false_rules( [r(_,N2, P => next false)|Rest ], [r(NewR1,N2,NegP)|NewRules ] ) :-
 1032       snff_negate(P, NegP),
 1033       newrulecount(NewR1),
 1034       expand_false_rules(Rest, NewRules).
 1035
 1036expand_false_rules( [ Other | Rest ], [ Other | NewRest ] ) :-
 1037	expand_false_rules(Rest, NewRest).
 1038
 1039/*********************************************************/
 1040/* disjoin(List, Disjunction)                            */
 1041/*                                                       */ 
 1042/* Takes a list of nodes (List) eg [a,b,c] and returns   */
 1043/* them separated by or eg a or b or c in Disjunction    */
 1044/*********************************************************/
 1045
 1046disjoin([], false):-!.
 1047disjoin(List, Form) :- disjoin2(List, Form).
 1048
 1049/*********************************************************/
 1050
 1051disjoin2([F|[]], F):-!.
 1052disjoin2([F | Rest], F or NewForm) :- disjoin2(Rest, NewForm).
 1053
 1054/*********************************************************/
 1055/* conjoin(List, Conjunction)                            */
 1056/*                                                       */ 
 1057/* Takes a list of nodes (List) eg [a,b,c] and returns   */
 1058/* them separated by "and" eg a and b and c in           */
 1059/* Conjunction.                                          */
 1060/*********************************************************/
 1061
 1062conjoin([], true):-!.
 1063conjoin(List, Form) :- conjoin2(List, Form).
 1064
 1065/********************************************************/
 1066
 1067conjoin2([F|[]],F):-!.
 1068conjoin2([F | Rest], F and NewForm) :- conjoin2(Rest, NewForm).
 1069
 1070/*****************************************************************************/
 1071/* is_superset_of__member_of_list(Node, List)                                */ 
 1072/*                                                                           */
 1073/* Returns true if one of List is a subset of Node. Usful for detecting      */
 1074/* conjunctions on the rhs of a rule given we are trying to generate a       */
 1075/* node.                                                                     */
 1076/*                                                                           */
 1077/*****************************************************************************/
 1078
 1079is_superset_of_member_of_list(Node, [H|_]):-
 1080   subset(H, Node).
 1081
 1082is_superset_of_member_of_list(Node, [_|List]):-
 1083   is_superset_of_member_of_list(Node, List).
 1084
 1085/*****************************************************************************/
 1086/* node_is_member_of(NewNode, ListofNodes)                                   */ 
 1087/*                                                                           */
 1088/* Similar to node_is_superset_of_list but returns true if the new node and  */
 1089/* one of the nodes from list of nodes are the same (set wise) ie the        */
 1090/* predicate would return true if new node was [a,b] and either [a, b] or    */
 1091/* [b,a] were found in ListOfNodes.                                          */
 1092/*                                                                           */
 1093/*****************************************************************************/
 1094
 1095node_is_member_of(NewNode, [Node|_]):-
 1096   same(NewNode, Node), !.
 1097
 1098node_is_member_of(NewNode, [_|OldNodes]):-
 1099   node_is_member_of(NewNode, OldNodes).
 1100
 1101/*****************************************************************************/
 1102/* same(NodeX,NodeY)                                                         */
 1103/*                                                                           */
 1104/* Takes two nodes and returns true if they are equivalent ie [a] and [a]    */
 1105/* would return true, also [a,b] and [b,a], but [a,b,c] and [b,c] would not. */
 1106/*                                                                           */
 1107/*****************************************************************************/
 1108
 1109same(X,X) :- !.
 1110
 1111same(X,Y):-
 1112  subset(X,Y),!,
 1113  subset(Y,X).
 1114
 1115/*****************************************************************************/
 1116/* remove_duplicate_nodes(NodeList, NewNodes).                               */
 1117/*                                                                           */
 1118/* Takes a list of nodes (NodeList) and removes any duplicate nodes which    */
 1119/* may exist, ie it returns the set of nodes obtained from the list of nodes.*/
 1120/*                                                                           */
 1121/*****************************************************************************/
 1122
 1123remove_duplicate_nodes([],[]):-!.
 1124
 1125remove_duplicate_nodes([Node|NodeList], NewNodes):-
 1126   node_is_member_of(Node, NodeList), !,
 1127   remove_duplicate_nodes(NodeList, NewNodes).
 1128
 1129remove_duplicate_nodes([Node|NodeList], [Node|NewNodes]):-
 1130   remove_duplicate_nodes(NodeList, NewNodes).
 1131
 1132/***************************************************************************/
 1133
 1134remove_member(X,[X|Rest],NewList):-
 1135   remove_member(X,Rest,NewList).
 1136
 1137remove_member(X,[Y|Rest],[Y|NewList]):-
 1138   remove_member(X,Rest,NewList).
 1139
 1140remove_member(_,[],[]).
 1141
 1142/*********************************************************************************************/
 1143/*  rewrite_and_or(List,Disjunction)                                                         */
 1144/*                                                                                           */
 1145/* Takes a list in the form [[...],[..],[...],[....]] and conjoins all the [..] bits ie      */
 1146/* sticks and between the literals and replaces the , in the original lis by or.             */
 1147/*********************************************************************************************/
 1148
 1149rewrite_and_or([H], NewH):-
 1150   conjoin(H,NewH).
 1151 
 1152rewrite_and_or([H|Tail], NewH or NewTail):-
 1153  conjoin(H, NewH),
 1154  rewrite_and_or(Tail, NewTail).
 1155
 1156/******************************************************************************************/
 1157
 1158negate_modal_lit(~ k ~ X, k ~ X).
 1159
 1160negate_modal_lit(k ~ X, ~ k ~ X).
 1161
 1162negate_modal_lit(~ k X, k X).
 1163
 1164negate_modal_lit(k X, ~ k X).
 1165
 1166negate_modal_lit(~ X, X).
 1167
 1168negate_modal_lit(X, ~ X).
 1169
 1170
 1171/* snff(Initial, Final) :- The Initial set of rules, is transformed to the
 1172                           Final set, which are in DSNF_K form. */
 1173
 1174/********************************************/
 1175/* The Final set of rules is in DSNF_K form */
 1176/********************************************/
 1177
 1178snff([],[]).
 1179
 1180snff(Final, Final) :-
 1181        snff_in_form_list(Final).    
 1182
 1183snff(Initial, Final) :-
 1184        snff_anchor_to_start(Initial,Anchored),
 1185        snff_rewrite_list(Anchored,Final).
 1186
 1187/****************************************************************/
 1188/* Anchor formulae to start if it is not already in DSNF_K form */
 1189/****************************************************************/
 1190
 1191snff_anchor_to_start([],[]):-!.
 1192
 1193snff_anchor_to_start([H|Tail], [H|NewRest]):-
 1194        in_form(H),
 1195        snff_anchor_to_start(Tail,NewRest).

 1199snff_anchor_to_start([H|Tail], [start => V, V => (H)|NewRest]):-
 1200        new_temp_prop(V),
 1201        snff_anchor_to_start(Tail, NewRest).
 1202
 1203/*************************************************/
 1204/* Rewrite rules, so they are in the DSNF_K form */
 1205/*************************************************/
 1206
 1207snff_rewrite_list([],[]):-!.
 1208snff_rewrite_list([Rule|Rest],[Rule|NewRest]):-
 1209         in_form(Rule),
 1210         snff_rewrite_list(Rest,NewRest).
 1211
 1212snff_rewrite_list([Rule|Rest],Other):-
 1213         snff_rewrites(Rule,NewRule, NewInform),
 1214         snff_rewrite_list(NewRule,NewerRule),
 1215         append(NewInform,NewerRule,FinalRule),
 1216         snff_rewrite_list(Rest,NewRest),
 1217         append(FinalRule,NewRest,Other).
 1218
 1219/*************************************************/
 1220/* Rewrite a given clause                        */
 1221/*************************************************/
 1222
 1223snff_rewrites(X => (A and B),[X => A, X => B],[]).
 1224
 1225snff_rewrites(X => ~(A and B),[X => ~ A or ~ B],[]).
 1226
 1227snff_rewrites(X => (A => B),[X => ~ A or B],[]).
 1228
 1229snff_rewrites(X => ~ (A => B),[X => A, X => ~ B],[]).
 1230
 1231snff_rewrites(X => ~ ~ A ,[X => A],[]).
 1232
 1233snff_rewrites(X => k A,[X => ~ V],[V => k A, ~ V => k A]):-
 1234        is_literal(A),
 1235        simplify_and(~ A,NewA),
 1236        new_dontknow_prop(V,NewA).
 1237
 1238snff_rewrites(X => k A ,[V => A],[X => k V]):-
 1239        is_not_literal(A),
 1240        new_temp_prop(V).
 1241
 1242snff_rewrites(X => ~ k A ,[X => V],[V => ~ k A, ~ V => k A]):-
 1243        is_literal(A),
 1244        simplify_and(~ A, NewA),
 1245        new_dontknow_prop(V,NewA).
 1246
 1247snff_rewrites(X => ~ k A ,[X => ~ k ~ V, V => ~ A],[]):-
 1248        is_not_literal(A),
 1249        new_temp_prop(V).
 1250
 1251snff_rewrites(X => A or B, Rest,[NegX or NewA or NewB]):-
 1252        snff_negate(X,NegX),
 1253        check_dnf(A, NewA, ARest),
 1254        check_dnf(B, NewB, BRest),
 1255        append(ARest,BRest,Rest).
 1256
 1257snff_rewrites(X => next A ,[V => A],[X => next V]):-
 1258%        is_not_literal(A),
 1259        new_temp_prop(V).
 1260
 1261snff_rewrites(X => ~ next A,[X => next ~ A],[]).
 1262
 1263snff_rewrites(X => (A until B),[X => V until B, V => A],[]):-
 1264        is_not_literal(A),
 1265        new_temp_prop(V).
 1266
 1267snff_rewrites(X => (A until B),[X => A until V, V => B],[]):-
 1268        is_not_literal(B),
 1269        new_temp_prop(V).
 1270
 1271snff_rewrites(X => (A until B),[],[~ X or B or A, ~ X or B or V, V => next (B or A), V => next (B or V), X => sometimes B]):-
 1272        is_literal(A),
 1273        is_literal(B),
 1274        new_temp_prop(V).
 1275
 1276snff_rewrites(X => ~ (A until B),[X => ((~ B) unless (~ A and ~ B))],[]).
 1277
 1278snff_rewrites(X => (A unless B),[X => V unless B, V => A],[]):-
 1279        is_not_literal(A),
 1280        new_temp_prop(V).
 1281
 1282snff_rewrites(X => (A unless B) ,[X => A unless V, V => B],[]):-
 1283        is_not_literal(B),
 1284        new_temp_prop(V).
 1285
 1286snff_rewrites(X => (A unless B) ,[],[~ X or B or A, ~ X or B or V, V => next (B or A), V => next (B or V)]):-
 1287        is_literal(A),
 1288        is_literal(B),
 1289        new_temp_prop(V).
 1290
 1291snff_rewrites(X => ~ (A unless B) ,[X => ((~ B) until (~ A and ~ B))],[]).
 1292
 1293snff_rewrites(X => (sometimes A) ,[V => A],[X => sometimes V]):-
 1294        is_not_literal(A),
 1295        new_temp_prop(V).
 1296
 1297snff_rewrites(X => (~ sometimes A) ,[X => always ~ A],[]).
 1298
 1299snff_rewrites(X => (always A) ,[X => always V , V => A],[]):-
 1300        is_not_literal(A),
 1301        new_temp_prop(V).
 1302
 1303snff_rewrites(X => (always A) ,[],[~ X or A, V => next A, ~ X or V, V => next V]):-
 1304        is_literal(A),
 1305        new_temp_prop(V).
 1306
 1307snff_rewrites(X => (~ always A) ,[X => sometimes ~ A ],[]).
 1308
 1309snff_rewrites(X => (Y),[],[~ X or Y]):-
 1310      conjunction_of_literals(X),
 1311      disjunction_of_modal_literals(Y).
 1312
 1313/***********************************/
 1314/* check if rule is in DSNF_K form */
 1315/***********************************/
 1316
 1317snff_in_form_list([]):-!.
 1318
 1319snff_in_form_list([H|Tail]):-
 1320      in_form(H),
 1321      snff_in_form_list(Tail).        
 1322
 1323/**********************************/
 1324/* Normal Form                    */
 1325/**********************************/
 1326
 1327in_form(start => X):-
 1328      disjunction_of_literals(X).
 1329
 1330in_form(X):-
 1331      disjunction_of_literals(X).
 1332
 1333in_form(X => k A):-
 1334      is_literal(X),
 1335      is_literal(A).
 1336
 1337in_form(X => ~ k A):-
 1338      is_literal(X),
 1339      is_literal(A).
 1340
 1341in_form(X => sometimes Y):-
 1342       conjunction_of_literals(X),
 1343       is_literal(Y).
 1344
 1345in_form(X => next(Y)):-
 1346      conjunction_of_literals(X),
 1347      disjunction_of_literals(Y).
 1348
 1349/************************************/
 1350/* Disjunction of literals          */
 1351/************************************/
 1352
 1353disjunction_of_literals(X):-
 1354       strip_or(X,StrippedX),
 1355       is_literal_list(StrippedX).
 1356
 1357/**********************************/
 1358/* Disjucntion of modal literals  */
 1359/**********************************/
 1360
 1361disjunction_of_modal_literals(X):-
 1362       strip_or(X,StrippedX),
 1363       is_modal_literal_list(StrippedX).
 1364
 1365/***********************************/
 1366/* Conjunction of literals         */
 1367/***********************************/
 1368
 1369conjunction_of_literals(X):-
 1370       strip_and(X,StrippedX),
 1371       is_literal_list(StrippedX).
 1372
 1373/**************************************************/
 1374/* Verifies if a given list is a list of literals */
 1375/**************************************************/
 1376
 1377is_literal_list([[H]|Tail]):-
 1378      is_literal(H),
 1379      is_literal_list(Tail).
 1380      
 1381is_literal_list([]).       
 1382
 1383/********************************************************/
 1384/* Verifies if a given list is a list of modal literals */
 1385/********************************************************/
 1386
 1387is_modal_literal_list([]).
 1388
 1389is_modal_literal_list([[k H]|Tail]):-
 1390      is_literal(H),
 1391      is_modal_literal_list(Tail).
 1392
 1393is_modal_literal_list([[~ k H]|Tail]):-
 1394      is_literal(H),
 1395      is_modal_literal_list(Tail).
 1396
 1397is_modal_literal_list([[H]|Tail]):-
 1398      is_literal(H),
 1399      is_modal_literal_list(Tail).
 1400
 1401/******************** **************/
 1402/* Check if subformulae are in DNF */
 1403/***********************************/           
 1404
 1405check_dnf(A or B, NewA or NewB, Rest):-
 1406        check_dnf(A, NewA, ARest),
 1407        check_dnf(B, NewB, BRest),
 1408        append(ARest,BRest,Rest).
 1409
 1410check_dnf(A => B, NewAll, Rest):-
 1411        check_dnf(~ A or B, NewAll, Rest).
 1412
 1413check_dnf(A, A, []):-
 1414       is_literal(A).
 1415
 1416check_dnf(k A, ~ V, [V => ~ k A, ~ V => k A]):-
 1417        is_literal(A),
 1418        snff_negate(A,NegA),
 1419        new_dontknow_prop(V,NegA).
 1420
 1421check_dnf(~ k A, V, [V => ~ k A, ~ V => k A]):-
 1422        is_literal(A),
 1423        snff_negate(A,NegA),
 1424        new_dontknow_prop(V,NegA).
 1425
 1426check_dnf(A, V, [V => A]):-
 1427        new_temp_prop(V). 

 1429/*******************************/
 1430/* Form to NNF_Form            */
 1431/*******************************/
 1432
 1433snff_negate(~ X, X):- !.
 1434
 1435snff_negate(X and Y, NotX or NotY):- 
 1436        !, 
 1437        snff_negate(X, NotX),
 1438        snff_negate(Y, NotY).
 1439
 1440snff_negate(X or Y, NotX and NotY):- 
 1441        !, 
 1442        snff_negate(X, NotX), 
 1443	snff_negate(Y, NotY).
 1444
 1445snff_negate(true, false).
 1446
 1447snff_negate(false, true).
 1448
 1449snff_negate(X, ~ X):- 
 1450       is_proposition(X).
 1451
 1452
 1453/**************************************************************************/
 1454/*
 1455   This program is an implementation of nontemporal resolution. 
 1456The predicates related to substitution have been written by Michael, 
 1457non temporal resolution predicates are based on those written by Michael, 
 1458and subsumtion predicates are written by Clare.
 1459
 1460The following procedures are necessary :-
 1461
 1462        1. Check for false
 1463        2. Simplification ie x => next false converted to
 1464                             true => ~x  
 1465        3. Subsumption
 1466        4. Non temporal resolution
 1467        5. Provides new real resolvents
 1468        6. Repeat 1 to 5 until false found or no new resolvents
 1469
 1470Note :-
 1471======
 1472The predicate
 1473                fullmres(OldRules,NewRules)
 1474
 1475sets the non temporal resolution in progress and expects a set of clauses derived 
 1476from translation to SNF (OldRules),which have been numbered and rewritten to the form
 1477
 1478                r(Number,FromList,Text)
 1479
 1480where Number is the number of the clause, FromList, will originally be empty, and Text 
 1481is the actual clause itself. It returns NewRules ie what has been derived from non 
 1482temporal resolution. This predicate is called from fullres.pl as part of the main cycle.
 1483
 1484     A predicate cyclemres is called which recurs on itself until no new resolvents have 
 1485been derived or false has been derived. This predicate and the predicates it calls maintains 
 1486a distinction round each cycle of the Old ruleset and those newly derived from resolution, 
 1487so simpilfication may just be done on the new ruleset, subsumption may be done between the 
 1488new ruleset and the old ruleset, and then non temporal resolution may be done between the 
 1489new ruleset and the old ruleset,before combining the two and starting again around the cycle.
 1490
 1491********************************************************************************/
 1492
 1493/*******************************************************************************/
 1494/*  mres(LiteralRules,
 1495         ModalRules,
 1496         InitialRules,
 1497         NewLRules,
 1498         NewMRules)                                                            */
 1499
 1500
 1501/* This sets the nontemporal resolution off, the first three arguments,        */
 1502/* containing literal, modal and initial clauses,                              */
 1503/* derived from SNF which have been rewriten into the form                     */
 1504/* r(Number,FromList,Text), where currently FromList will be empty.            */
 1505/* NewLRules and NewMRules will contain the new ruleset after no more          */
 1506/* non temporal resolution can take place, or false if false has been derived. */
 1507/*******************************************************************************/
 1508
 1509mres(LiteralRules,ModalRules,Initial,NewLRules,NewMRules):-
 1510     cyclemres(1,[],[],LiteralRules,ModalRules,Initial,NewLRules,NewMRules).    
 1511
 1512% Leave 2nd and 3rd arguments empty so as to treat the original ruleset as "new" resolvents.
 1513
 1514/*****************************************************************************/
 1515/*                                                                           */
 1516/* This predicate is called from fullres.pl during the full resolution       */
 1517/* process. OldRules are in the form r(Number,FromList,Text), where          */
 1518/* Number is the ruless number, FromList contains the numbers of the rules   */
 1519/* which were the parents of this resolvent, and Text is the rule itself     */
 1520/* (in SNF). NewishRules contain the new resolvents obtained from the        */
 1521/* last temporal resolution step. SRules contains a rules which have been    */
 1522/* subsumed on previous cycles round the non-temporal resolution process.    */
 1523/* NewRules will contain the new ruleset                                     */
 1524/* after no more non temporal resolution can take place, or false if a       */
 1525/* contradiction has been derived. NewSRules contains SRules plus any new    */
 1526/* rules which ahve been subsumed.                                           */
 1527/*****************************************************************************/
 1528
 1529mres(OldLiteral,OldModal,NewishLiteral,NewishModal,Initial,NewLiteral,NewModal):-
 1530   cyclemres(1,OldLiteral,OldModal,NewishLiteral,NewishModal,Initial,NewLiteral,NewModal).
 1531
 1532/*****************************************************************************/
 1533/*  cyclemres(Count,
 1534              OldLiteral,
 1535              OldModal,
 1536              NewishLiteral,
 1537              NewishModal,
 1538              Initial,
 1539              NewLiteral,
 1540              NewModal
 1541              )                                                              */
 1542/*                                                                           */
 1543/*  Cycles around the non temporal resolution cycle, checking for false and  */
 1544/*  if found returning false, otherwise performing simplification,           */
 1545/*  subsumption, nontemporal resolution and then recurring on itself until   */
 1546/*  false or an empty set of resolvents is detected. Count is the current    */
 1547/*  cycle we are on, OldRules are rules from previous cyles rounds the       */
 1548/*  non-temporal resolution processes. NewishResolvents are the new          */
 1549/*  resolvents generated during the last cycle of non-temporal resolution    */
 1550/*  and SRules are the store of rules which have been subsumed which may need*/
 1551/*  to be kept to generate a proof if false is derived. NewRules is the      */
 1552/*  final ruleset after no more non-temporal resolution can be done and      */
 1553/*  NewSRules is the new set of subsumed rules.                              */
 1554/*****************************************************************************/
 1555
 1556cyclemres(_,[],[],[],[],_,[],[]).
 1557%:-my_write('\ncyclemres ==> (1)\n').                     % No new resolvents.
 1558
 1559cyclemres(_,LRules,MRules,[],[],_,LRules,MRules):-
 1560%    my_write('\ncyclemres ==> (2)\n'),
 1561    my_write('Have generated no new resolvents,current literal/modal clauses are :-\n'),
 1562    write_ruleset(LRules),                   % Terminate non temporal resolution
 1563    write_ruleset(MRules).                   % as no new Rules have been derived.
 1564
 1565cyclemres(_,_,_,NewLRules,_,[r(_,_,X)],[r(0,[],false)],_):-
 1566%    my_write('\ncyclemres ==> (2.5)\n'),
 1567    snff_negate(X,NegX),
 1568    test_member(NegX,NewLRules),
 1569    simplify(NewLRules,SNewLRules),
 1570    self_subsumption(SNewLRules,SubNewLRules),
 1571    flatten(SubNewLRules,FSubNewLRules),
 1572    my_write('\nNew literal clauses include (~ start).\n'),
 1573    write_ruleset(FSubNewLRules),      % Terminate non temporal resolution as false
 1574    write('\nHave generated false in initial clauses.\n').
 1575
 1576cyclemres(_,_OldLRules,OldMRules,NewLRules,_,_,[r(0,[],false)],OldMRules):-
 1577%    my_write('\ncyclemres ==> (3)\n'),
 1578    test_member(false,NewLRules),
 1579    my_write('\nNew literal clauses include false.\n'),
 1580    write_ruleset(NewLRules),      % Terminate non temporal resolution as false
 1581    write('\nHave generated false in literal clauses.\n').
 1582
 1583cyclemres(_,_OldLRules,_OldMRules,_,NewMRules,_,[r(0,[],false)],[r(0,[],false)]):-
 1584%    my_write('\ncyclemres ==> (4)\n'),
 1585    test_member(false,NewMRules),
 1586    my_write('\nNewModal clauses include false.\n'),
 1587    write_ruleset(NewMRules),   % Terminate non temporal resolution as false
 1588    write('\nHave generated false in modal clauses.\n').
 1589
 1590% Occasionally ran out of space during non-temporal resolution so have hadded a specific garbage collect.
 1591
 1592cyclemres(Count,OldLRules,OldMRules,NewLRules,NewMRules,Initial,NewerLRules,NewerMRules):-
 1593%   my_write('\ncyclemres ==> (5)\n'),
 1594%   garbage_collect,
 1595   writef('\nCycle Number%t.',[Count]),
 1596   my_k_to_literal(NewMRules,KRules),
 1597   append(KRules,NewLRules,AddedNewLRules),
 1598   simplify(AddedNewLRules,SimplifiedLRules),
 1599   simplify(NewMRules,SimplifiedMRules),
 1600   garbage_collect,
 1601   subsumption(OldLRules,SimplifiedLRules,SubOldLRules,SubNewLRules1),
 1602   trim_stacks,
 1603   subsumption(OldMRules,SubNewLRules1,SubOldMRules1,SubNewLRules2),
 1604   trim_stacks,
 1605   subsumption(SimplifiedMRules,SubNewLRules2,SubNewMRules1,SubNewLRules),
 1606   trim_stacks,
 1607   subsumption(SubOldMRules1,SubNewMRules1,SubOldMRules,SubNewMRules),
 1608   trim_stacks,
 1609   my_write('\nOld Literal Clauses\n'),
 1610   write_ruleset(SubOldLRules),
 1611   my_write('\nOld Modal Clauses\n'),
 1612   write_ruleset(SubOldMRules),
 1613   my_write('\nNew Literal Clauses\n'),
 1614   write_ruleset(SubNewLRules),
 1615   my_write('\nNew Modal Clauses\n'),
 1616   write_ruleset(SubNewMRules),
 1617   do_mres(SubOldLRules,SubOldMRules,SubNewLRules,SubNewMRules,ResLRules,ResMRules,NewOldLRules,NewOldMRules),
 1618   NewCount is Count + 1,!,garbage_collect,
 1619   cyclemres(NewCount,NewOldLRules,NewOldMRules,ResLRules,ResMRules,Initial,NewerLRules,NewerMRules).
 1620
 1621/* ************************ */
 1622/* SUBSUMPTION              */
 1623/* ************************ */
 1624
 1625/**********************************************************************************/
 1626/*  subsumption(Old_Rules,New_Rules,SRules,New_Old_Rules,New_New_Rules,NewSRules) */
 1627/*                                                                                */
 1628/*   This predicate takes every rule in New_Rules and attempts subsumption        */
 1629/*   between every rule and every other in this list. Then subsumption is         */
 1630/*   performed between everything in the subsumed version of New_Rules and        */
 1631/*   Old_Rules. New_Old_Rules is then the subsumed version of Old_Rules and       */
 1632/*   New_New_Rules is the subsumed version of New_Rules. SRules contains rules    */
 1633/*   which have been subsumed on previous cycles and NewSRules contain            */
 1634/*   SRules plus any rules subsumed on this cycle.                                */
 1635/**********************************************************************************/
 1636
 1637subsumption(Old_Rules,New_Rules,New_Old_Rules,FNew_New_Rules) :-
 1638  self_subsumption(New_Rules,Newish_Rules),
 1639  flatten(Newish_Rules,FNewish_Rules),!,
 1640  subsumption2(Old_Rules,FNewish_Rules,New_Old_Rules,New_New_Rules),
 1641  flatten(New_New_Rules,FNew_New_Rules),!.
 1642
 1643/******************************************************************************/
 1644/*  self_subsumption([R | Rest],SRules,New_Rules,NewSRules)                   */
 1645/*                                                                            */
 1646/*  Attempts subsumption between R and Rest, recurrs on Rest and outputs      */
 1647/*  subsumed list in New_Rules. SRules are the rules which have been subsumed */
 1648/*  on previous cycles and any new ones subsumed are added to NewSRules.      */
 1649/******************************************************************************/
 1650
 1651self_subsumption([],[]):-!.
 1652
 1653self_subsumption([R|Rest],[NewR|NewRules]):-
 1654  subsume_rule(Rest,R,Remain_Rest,NewR),!,
 1655  self_subsumption(Remain_Rest,NewRules).
 1656
 1657
 1658/***********************************************************************************/
 1659/*  subsumption2(OldRules,[R | Rest],SRules,New_Old_Rules,New_New_Rules,NewSRules) */
 1660/*                                                                                 */
 1661/*  Attempts subsumption between R and OldRules, recurrs on Rest and outputs       */
 1662/*  lists after subsumption in New_Old_Rules and New_New_Rules. SRules are the     */
 1663/*  rules which have been subsumed on previous cycles and any new ones             */
 1664/*  subsumed are added to NewSRules.                                               */
 1665/***********************************************************************************/
 1666
 1667subsumption2(Old_Rules,[],Old_Rules,[]):-!.
 1668
 1669subsumption2([],NewRules,[],NewRules):-!.
 1670
 1671subsumption2(Old_Rules,[R|Rest],New_Old_Rules,[NewR|New_Rules]):-
 1672   subsume_rule(Old_Rules,R,Newish_Old_Rules,NewR),!,
 1673   subsumption2(Newish_Old_Rules,Rest,New_Old_Rules,New_Rules).
 1674
 1675/*******************************************************************************/
 1676/* subsume_rule(Old_Rules,ThisRule,SRules,New_Old_Rules,New_ThisRule,NewSRules)*/
 1677/*                                                                             */
 1678/*   This predicate compares ThisRule with every rule in Old_Rules. Rules are  */
 1679/*   in the format r(Number,FromList,Text). If ThisRule is subsumed by a       */
 1680/*   rule in Old_Rules then Old_rules are returned and New_ThisRule will be    */
 1681/*   and empty list but if ThisRule subsumes a Rule in Old_Rules, the rule     */
 1682/*   that has been subsumed is removed from Old_Rules and the predicate the    */
 1683/*   attempts subsumption between ThisRule and the rest of Old_Rules.          */
 1684/*   It is important that the predicates are in the order they appear in, as   */
 1685/*   if there are duplicate rules ie Rule1 subsumes Rule2 and vice versa we    */
 1686/*   want to remove ThisRule and return an empty list as New_ThisRule          */
 1687/*   rather than the other way around for we are depending upon no new         */
 1688/*   resolvents to be derived for our non-temporal resolution process to       */
 1689/*   terminate. SRules contains any rules which have been subsumed previously  */
 1690/*   NewSRules will also contain rules subsumed on this cycle.                 */
 1691/*******************************************************************************/
 1692
 1693% Firstly looking at cases of strong last implies something
 1694
 1695subsume_rule([],r(N1,N2,G),[],[r(N1,N2,G)]):-!.
 1696subsume_rule([],R,[],[R]):-!.
 1697
 1698subsume_rule([r(N1,N2,F) | Rules],r(_,_,G),[r(N1,N2,F) | Rules],[]) :-
 1699             dis_implies(F,G),!.                                % P => F
 1700
 1701subsume_rule([r(_,_,F) | Rules],r(N1,N2,G),New_Old_Rules,New_New_Rules) :-
 1702            dis_implies(G ,F),!,                        % Q => G subsumes P => F
 1703	    subsume_rule(Rules,r(N1,N2,G),New_Old_Rules,New_New_Rules).
 1704
 1705% default behaviour: ie no subsumption takes place
 1706
 1707subsume_rule([ R | Rules],r(N1,N2,G),[ R | New_Rules],New_New_Rules) :-
 1708	subsume_rule(Rules,r(N1,N2,G),New_Rules,New_New_Rules).
 1709
 1710% default behaviour to catch any of the cases not mentioned above
 1711
 1712subsume_rule([ R1 | Rules],R2,[ R1 | New_Old_Rules],New_New_Rules) :-
 1713   subsume_rule(Rules,R2,New_Old_Rules,New_New_Rules).
 1714
 1715
 1716/* ************************* */
 1717/* NON-TEMPORAL RESOLUTION * */
 1718/* ************************* */
 1719
 1720/*********************************************************************************/
 1721/* mres(OrigRules,[Rule|Rest],NewRules,Final)                                    */
 1722/*                                                                               */
 1723/*   Michaels code changed slightly to do non temporal resolution between        */
 1724/*   two lists OrigRules and [Rule|Rest] (new rules derived from resolution last */
 1725/*   time round the loop). After resolving Rule with every rule in OrigRules it  */
 1726/*   is added to OrigRules, and the first rule from Rest is resolved with all    */
 1727/*   rules in OrigRules + Rule, and so on. When Rest is empty, OrigRules which   */
 1728/*   now has all of [Rule|Rest] attached is copied to NewOrig and resolvents     */
 1729/*   found built up in Final. The first time round the loop ie after             */
 1730/*   initial conversion to SNF OrigRules will be empty, so gradually [Rule|Rest] */
 1731/*   will be copied into it and effectively resolved on itself. Rules are in the */
 1732/*   form r(Number,FromList,Text) . When resolution takes place a new            */
 1733/*   number for the rule is placed in Number and FromList will have the two rule */
 1734/*   numbers of the parents of the new rule.                                     */
 1735/*********************************************************************************/
 1736
 1737
 1738do_mres(LNewOrig,MOrigRules,LNew,RNew,FinalL,FinalM,NewOrigL2,NewOrigM2):-
 1739%    my_write('\ndo_mres ==> (2)\n'),
 1740    do_mres(LNewOrig,MOrigRules,LNew,FinalL1,FinalM1,NewOrigL1,NewOrigM1),
 1741    do_mres(NewOrigL1,NewOrigM1,RNew,FinalL2,FinalM2,NewOrigL2,NewOrigM2),
 1742    append(FinalL1,FinalL2,FinalL),
 1743    append(FinalM1,FinalM2,FinalM).
 1744
 1745do_mres(LNewOrig,MNewOrig,[],[],[],LNewOrig,MNewOrig).
 1746%:-my_write('\ndo_mres ==> (1).\n').
 1747
 1748do_mres(LOrigRules,MOrigRules,[Rule|Rest],FinalL,FinalM,NewOrigL,NewOrigM) :-
 1749%        my_write('\ndo_mres ==> (3).\n'),
 1750	mresolve(Rule,LOrigRules,MOrigRules,RulesL1,RulesM1),
 1751        add_to_set(LOrigRules,MOrigRules,Rule,Rest,RulesL1,RulesM1,FinalL,FinalM,NewOrigL,NewOrigM).
 1752
 1753/*************************************************************************************************/
 1754
 1755add_to_set(LOrigRules,MOrigRules,Rule,Rest,RulesL1,RulesM1,FinalL,FinalM,NewOrigL,NewOrigM) :-
 1756%        my_write('\nadd_to_set ==> (1)\n'),
 1757        is_modal_rule(Rule),!,
 1758	do_mres(LOrigRules,[Rule|MOrigRules],Rest,NewRulesL,NewRulesM,NewOrigL,NewOrigM),
 1759	append(RulesL1,NewRulesL,FinalL),
 1760	append(RulesM1,NewRulesM,FinalM).
 1761
 1762add_to_set(LOrigRules,MOrigRules,Rule,Rest,RulesL1,RulesM1,FinalL,FinalM,NewOrigL,NewOrigM) :-
 1763%        my_write('\nadd_to_set ==> (2)\n'),
 1764	do_mres([Rule|LOrigRules],MOrigRules,Rest,NewRulesL,NewRulesM,NewOrigL,NewOrigM),
 1765	append(RulesL1,NewRulesL,FinalL),
 1766	append(RulesM1,NewRulesM,FinalM).
 1767
 1768/*********************************************************************************/
 1769/*  mresolve(Rule,OrigRules,NewRules)                                            */
 1770/*                                                                               */
 1771/*  Takes a rule of the form r(Number,FromList,Text) and tries resolution        */
 1772/*  between the Text of this rule and the Text of all the other rules in         */
 1773/*  OrigRules. Any new resolvents derived are put into new rules where the       */
 1774/*  Number of the new resolvent is the next new rule number, and FromList is     */
 1775/*  filled with the rule numbers of the parents of the resolvent.                */
 1776/*********************************************************************************/
 1777
 1778/* First,the cases where resolution cannot take place */
 1779
 1780mresolve(_,[],[],[],[]).
 1781% :-my_write('\nmresolve ==> (1)\n').
 1782
 1783/* Next,resolution of initial rules: */
 1784
 1785mresolve(r(N1,N2,F),[r(N3,_,G) | Rest],Other,LFinal,MFinal) :-
 1786%        my_write('\nmresolve ==> (2)\n'),
 1787        basic_nt_resolve(F,G,Resolvent,[],[]),
 1788	mresolve(r(N1,N2,F),Rest,Other,NewLRules,NewMRules),
 1789	generate_new_resolvent([N1,N3],Resolvent,NewLRules,NewMRules,LFinal,MFinal).
 1790
 1791mresolve(Rule,[_ | Rest],Other,NewLRules,NewMRules) :-
 1792%        my_write('\nmresolve ==> (3)\n'),
 1793	mresolve(Rule,Rest,Other,NewLRules,NewMRules).
 1794
 1795mresolve(r(N1,N2,F),[],[r(N3,_,G) | Rest],LFinal,MFinal) :-
 1796%        my_write('\nmresolve ==> (4)\n'),
 1797        basic_nt_resolve(F,G,Resolvent,[],[]),
 1798	mresolve(r(N1,N2,F),[],Rest,NewLRules,NewMRules),
 1799	generate_new_resolvent([N1,N3],Resolvent,NewLRules,NewMRules,LFinal,MFinal).
 1800
 1801mresolve(Rule,[],[_ | Rest],NewLRules,NewMRules) :-
 1802%        my_write('\nmresolve ==> (5)\n'),
 1803	mresolve(Rule,[],Rest,NewLRules,NewMRules).
 1804
 1805/*****************************************************************************/
 1806/*  generate_new_resolvent(FromList,ResolventList,Rules,NewRules             */
 1807/*                                                                           */
 1808/* If Resolvent is empty this just returns Rules as they are, otherwise a    */
 1809/* new rule is created and added to the front of Rules.                      */
 1810/*****************************************************************************/
 1811
 1812generate_new_resolvent(_,[],LR,MR,LR,MR).
 1813
 1814generate_new_resolvent(FromList,[Resolvent],LRules,MRules,FinalLRules,FinalMRules):-
 1815      is_modal_disjunct(Resolvent),!,
 1816      simplify_rule(r(_,FromList,Resolvent),[r(_,FromList,SimpRule)]),
 1817      change_form(SimpRule,RulesList),
 1818      number_rules(RulesList,FromList,NumberedRules),
 1819      simplify(NumberedRules,SimpRules),
 1820      separate_rules(SimpRules,_ERules,_Initial,NewLRules,NewMRules,_Temporal),
 1821      append(LRules,NewLRules,FinalLRules),
 1822      append(MRules,NewMRules,FinalMRules).
 1823
 1824generate_new_resolvent(FromList,[Resolvent],LRules,MRules,[SimpRule | LRules],MRules):-
 1825      newrulecount(N),
 1826      simplify_rule(r(N,FromList,Resolvent),[SimpRule]).
 1827
 1828/******************************************************************************/
 1829/*  basic_nt_resolve(Disj1,Disj2,Resolvent,S1,S2) :-                          */
 1830/*                                                                            */
 1831/*      Tries to resolve the clauses Disj1 and Disj2 together.                */
 1832/*      If it fails, Resolvent is [], if it succeeds,                         */
 1833/*	resolvent is [resolvent]. S1 is a list recording what is left          */
 1834/*	of Disj1, while S2 is what is left of Disj2.                           */
 1835/******************************************************************************/ 
 1836
 1837basic_nt_resolve(A => B,Disj2,Resolvent,S1,S2):- 
 1838        snff_negate(A,NegA),!,
 1839        basic_nt_resolve(NegA or B,Disj2,Resolvent,S1,S2).        
 1840
 1841basic_nt_resolve(Disj1,A => B,Resolvent,S1,S2):-
 1842        snff_negate(A,NegA),!,
 1843        basic_nt_resolve(Disj1,NegA or B,Resolvent,S1,S2).
 1844
 1845basic_nt_resolve(A or B,Disj2,Resolvent,S1,S2) :-
 1846	basic_nt_resolve(A,Disj2,Resolvent,[B|S1],S2).
 1847
 1848basic_nt_resolve(A or B,Disj2,Resolvent,S1,S2) :-
 1849	basic_nt_resolve(B,Disj2,Resolvent,[A|S1],S2).
 1850
 1851basic_nt_resolve(_ or _, _,_,_,_) :- fail.
 1852
 1853basic_nt_resolve(A,Disj2,Resolvent,S1,S2) :-
 1854	internal_nt_resolve(A,Disj2,Resolvent,S1,S2).
 1855
 1856/*****************************************************************************/
 1857/*  internal_nt_resolve(L,Disj, Resolvent,S1,S2)                             */
 1858/*                                                                           */
 1859/*  Attempts to resolve L which is now a proposition or negated proposition  */
 1860/*  with Disj. S1 and S2 have what remains of the original two disjuncts     */
 1861/*  we were trying to resolve. The resolvent created is returned in          */
 1862/*  Resolvent                                                                */
 1863/*****************************************************************************/
 1864
 1865internal_nt_resolve(L,A or B, Resolvent,S1,S2) :-
 1866	internal_nt_resolve(L,A,Resolvent,S1,[B|S2]).
 1867
 1868internal_nt_resolve(L,A or B,Resolvent,S1,S2) :- 
 1869	internal_nt_resolve(L,B,Resolvent,S1,[A|S2]).
 1870
 1871internal_nt_resolve(_,_ or _,_,_,_) :- fail.
 1872
 1873internal_nt_resolve(L,M,[Resolvent],S1,S2) :-
 1874        resolveable(L,M,S1,S2,NewS1,NewS2),
 1875	append(NewS1,NewS2,NewLst),
 1876	disjoin(NewLst,Resolvent).
 1877
 1878/*********************/
 1879/* Basic Resolution  */
 1880/*********************/
 1881
 1882resolveable(L,M,S1,S2,S1,S2):-
 1883  comp_lits(L,M).
 1884
 1885/********************/
 1886/* Modal Resolution */
 1887/********************/
 1888
 1889resolveable(L,M,S1,S2,NewS1,NewS2):-
 1890  sometime_rule(L,M,S1,S2,NewS1,NewS2). 
 1891
 1892resolveable(L,M,S1,S2,NewS1,NewS2):- 
 1893  always_rule(L,M,S1,S2,NewS1,NewS2). 
 1894
 1895/**********/ 
 1896/* MRES 2 */ 
 1897/**********/ 
 1898
 1899sometime_rule(k L,k M,S1,S2,S1,S2):-
 1900  comp_lits(L,M). 
 1901
 1902/**********/ 
 1903/* MRES 3 */ 
 1904/**********/ 
 1905
 1906sometime_rule(k L,M,S1,S2,S1,S2):-
 1907  comp_lits(L,M).
 1908
 1909sometime_rule(L,k M,S1,S2,S1,S2):-
 1910  comp_lits(L,M).
 1911
 1912/**********/ 
 1913/* MRES 4 */ 
 1914/**********/ 
 1915
 1916always_rule(~ k L,L,S1,S2,S1,NewS2):-
 1917  change_resolvent(S2,NewS2).
 1918
 1919always_rule(L,~ k L,S1,S2,NewS1,S2):-
 1920  change_resolvent(S1,NewS1).
 1921
 1922always_rule(~ k ~ L,M,S1,S2,S1,NewS2):-
 1923  comp_lits(L,M), 
 1924  change_resolvent(S2,NewS2). 
 1925
 1926always_rule(L,~ k ~ M,S1,S2,NewS1,S2):- 
 1927  comp_lits(L,M), 
 1928  change_resolvent(S1,NewS1). 
 1929
 1930/****************/ 
 1931/* MOD FUNCTION */ 
 1932/****************/ 
 1933
 1934change_resolvent([A or B|Rest], NewAll):-
 1935  change_resolvent(A or B,NewAB),
 1936  change_resolvent(Rest, NewRest), 
 1937  append(NewAB,NewRest, NewAll).
 1938
 1939change_resolvent(A or B, NewAB):-
 1940  change_resolvent(A, NewA),
 1941  change_resolvent(B, NewB),
 1942  append(NewA, NewB, NewAB).
 1943
 1944change_resolvent([A|Rest],NewAll):-
 1945  change_resolvent(A,NewA),
 1946  change_resolvent(Rest,NewRest),
 1947  append(NewA,NewRest,NewAll).
 1948
 1949change_resolvent([],[]).
 1950
 1951change_resolvent(X,[X]):-is_snl_literal(X).
 1952
 1953change_resolvent(~ k L,[~ k L]):-is_literal(L).
 1954
 1955change_resolvent(k L,[k L]):-is_literal(L).
 1956
 1957change_resolvent(k ~ L,[k ~ L]):-is_literal(L).        % Clare is this right?
 1958
 1959change_resolvent(~ k ~ L,[~ k ~ L]):-is_literal(L).
 1960
 1961change_resolvent(~ L,[~ k L]):-is_literal(L).
 1962
 1963change_resolvent(L,[~ k ~ L]):-is_literal(L). 
 1964
 1965/**********************************/ 
 1966
 1967is_modal_rule(r(_,_,Y => X)):- 
 1968   is_modal_rule(Y => X). 
 1969
 1970is_modal_rule(_Y => X):- 
 1971  is_modal_disjunct(X). 
 1972
 1973/**********************************/ 
 1974
 1975is_modal_disjunct(k _). 
 1976
 1977is_modal_disjunct(~ k _). 
 1978
 1979is_modal_disjunct(A or _):- 
 1980  is_modal_disjunct(A). 
 1981
 1982is_modal_disjunct(_ or B):- 
 1983  is_modal_disjunct(B). 
 1984
 1985/***************************************/
 1986
 1987is_list_of_only_modals(A or B):-
 1988  is_modal(A), 
 1989  is_list_of_only_modals(B).
 1990
 1991is_list_of_only_modals(A):-
 1992  is_modal(A).
 1993
 1994is_list_of_only_literals(A or B):-
 1995  is_literal(A), 
 1996  is_list_of_only_literals(B).
 1997
 1998is_list_of_only_literals(A):-
 1999   is_literal(A). 
 2000
 2001/*****************************************************************/
 2002/* The following returns a modal clause in the new normal form   */
 2003/*****************************************************************/ 
 2004
 2005change_form(true,[true]).
 2006
 2007change_form(Disjunction,[true => Disjunction]):-
 2008  is_modal(Disjunction).
 2009
 2010change_form(~ k X or Disj1, [Disj2 => ~ k X]):-
 2011  is_literal(Disj1),!,
 2012  snff_negate(Disj1,Disj2).
 2013
 2014change_form(k X or Disj1, [Disj2 => k X]):-
 2015  is_literal(Disj1),!,
 2016  snff_negate(Disj1,Disj2).
 2017
 2018change_form(Disj1 or ~ k X, [Disj2 => ~ k X] ):-
 2019  is_literal(Disj1),!,
 2020  snff_negate(Disj1,Disj2).
 2021
 2022change_form(Disj1 or k X, [Disj2 => k X]):-
 2023  is_literal(Disj1),!,
 2024  snff_negate(Disj1,Disj2).
 2025
 2026change_form(Disjunction,[Disjunction]):-
 2027   is_list_of_only_literals(Disjunction).
 2028
 2029change_form(Disjunction,List):- 
 2030  is_list_of_only_modals(Disjunction), 
 2031  snl_form(Disjunction,Literals,Modals),
 2032  append([Literals],Modals,List). 
 2033
 2034change_form(Disj1 or Disj2,Rest):-
 2035  is_literal(Disj1), 
 2036  snff_rewrite_list([~ Disj1 => (Disj2)],Rest).
 2037
 2038change_form(Disj1 or Disj2,Rest):- 
 2039  is_not_literal(Disj1),!, 
 2040  change_order(Disj1 or Disj2, NewDisj),
 2041  change_form(NewDisj,Rest). 
 2042
 2043/************************************************/ 
 2044
 2045change_order(A or B,NewOrder):- 
 2046  strip_or(A,NewA), 
 2047  strip_or(B,NewB), 
 2048  flatten(NewA,FlatA), 
 2049  flatten(NewB,FlatB), 
 2050  append(FlatB,FlatA,New), 
 2051  disjoin(New,NewOrder). 
 2052
 2053
 2054/*********************************************************************/
 2055/* The following returns the SNL literals and definition clauses     */
 2056/* from a given formula                                              */
 2057/*                                                                   */
 2058/* (1) the SNL literal itself                                        */
 2059/* (2) the disjunction of SNL literals                               */
 2060/* (3) the SNL(NEW), in case of a conjunction                        */
 2061/* (4) SNL(literal), in case of a non SNL literal                    */
 2062/*                                                                   */
 2063/*********************************************************************/
 2064
 2065snl(Formula,Formula,_,[],[]):- 
 2066   is_snl_literal(Formula). 
 2067
 2068snl(NewLiteralA or NewLiteralB,A or B,N,Literals,Modals):- 
 2069   snl(NewLiteralA,A,N,Literals1,Modals1), 
 2070   snl(NewLiteralB,B,N,Literals2,Modals2), 
 2071   append(Literals1,Literals2,Literals), 
 2072   append(Modals1,Modals2,Modals). 
 2073
 2074snl(NewLiteral,A and B,N,Literals,Modals):- 
 2075  snl_conjunction(NewLiteral,A and B,N,Literals,Modals). 
 2076
 2077snl(NewLiteral,Formula,N,[],[Rule1,Rule2]):- 
 2078   is_literal(Formula),!, 
 2079   new_dontknow_prop(NewLiteral,Formula), 
 2080   snff_negate(Formula, NegF), 
 2081   snff_negate(NewLiteral, NegNewLiteral), 
 2082   number_rule(NewLiteral => ~ k NegF,N,Rule1), 
 2083   number_rule(NegNewLiteral => k NegF,N,Rule2). 
 2084
 2085/****************************************************************/ 
 2086/* The following takes a formula and returns the corresponding  */
 2087/* SNL definition clauses.                                      */
 2088/****************************************************************/ 
 2089
 2090
 2091snl_form(k L,[NegNewProp],[NewProp => ~ k L, NegNewProp => k L]):- 
 2092   snff_negate(L,NegL), 
 2093   new_dontknow_prop(NewProp, NegL), 
 2094   snff_negate(NewProp,NegNewProp). 
 2095
 2096snl_form(~ k L,[NewProp],[NewProp => ~ k L, NegNewProp => k L]):- 
 2097   snff_negate(L,NegL), 
 2098   new_dontknow_prop(NewProp, NegL), 
 2099   snff_negate(NewProp,NegNewProp). 
 2100
 2101snl_form(A or B,Literals,Modals):- 
 2102   snl_form(A,Literals1,Modals1), 
 2103   snl_form(B,Literals2,Modals2), 
 2104   append(Literals1,Literals2,LiteralList), 
 2105   disjoin(LiteralList,Literals), 
 2106   append(Modals1,Modals2,Modals). 
 2107
 2108/************************************************************/ 
 2109/* The following deals with conjunctions of literals        */
 2110/* and returns the new proposition renaming the conjunction */
 2111/* as well as its corresponding definition clauses          */
 2112/************************************************************/