1%
    2%  fluent.pl:  predicates for manipulating fluent terms
    3%
    4%  Copyright 2008, Ryan Kelly
    5%
    6%  This file supplies the basic predicates for manipulating and reasoning
    7%  about fluent terms.  It shells out to a third-party prover for the
    8%  hard work.
    9%
   10%  Variables are expected to be actual prolog variables, as this vastly
   11%  increases the simplicity and efficiency of certain operations.  It also
   12%  means we need to take extra care in some other areas.  In particular,
   13%  we assume that the formula contains the *only* references to those
   14%  variables, so we are free to bind them in simplification and reasoning.
   15%
   16%  The following predicate is expected to be provided as a 'black box'
   17%  reasoning engine:
   18%
   19%    entails(Axioms,Conc):  Succeeds when Conc is logically entailed by Axioms
   20%
   21%  Axioms is a list of formulae, and Conc is a formula.  The predicate must
   22%  not bind any variables in Conc.
   23%
   24
   25
   26%
   27%  Our logical operators are:
   28% 
   29%     P & Q       -   logical and
   30%     P | Q       -   logical or
   31%     P => Q      -   implication
   32%     P <=> Q     -   equivalence
   33%     ~P          -   negation
   34%     !([X:T]:P)  -   universal quantification with typed variables
   35%     ?([X:T]:P)  -   existential quantification with types variables
   36%     A = B       -   object equality
   37%     A \= B      -   object inequality
   38%     knows(A,P)  -   individual-level knowledge modality
   39%     pknows(E,P) -   complex epistemic modality
   40%
   41%  Epistemic path operators are:
   42%
   43%     P ; Q       -   sequence
   44%     P | Q       -   choice
   45%     ?(P)        -   test
   46%     !(X:T)      -   nondet. rebind of a typed variable
   47%     -([X:V])    -   set vars to specific values
   48%     P*          -   iteration
   49%     
   50%  Most of these are native prolog operators so we dont have
   51%  to declare them ourselves.  Note that ! and ?
   52%  take a list variables as their first argument - this
   53%  allows more compact quantification over multiple variables.
   54%
   55%  Also note that variables are always paired with their type in the
   56%  quantifier - while we could probably deduce the type from its use
   57%  in the enclosed formula, having it explicit is oh so much easier.
   58%
   59
   60:- op(200,fx,~).   61:- op(500, xfy, <=>).   62:- op(500, xfy, =>).   63:- op(520, xfy, &).   64:- op(1200, xfx, :).   65:- op(550, fx, !).   66:- op(550, fx, ?).   67:- op(400, xf, *).   68
   69
   70%
   71%  normalize(F,N) - perform some basic normalisations on a formula
   72%
   73%  This is designed to make formulae easier to reason about.  It
   74%  re-arranges orderless terms into a standard order, for example
   75%  the arguments to '=' and the list of variables in a quantification.
   76%  It also simplifies away some trivial tautologies.
   77% 
   78normalize((A=B),(A=B)) :-
   79    A @< B, !.
   80normalize((A=B),(B=A)) :-
   81    B @< A, !.
   82normalize((A=B),true) :-
   83    A == B, !.
   84normalize((A\=B),(A\=B)) :-
   85    A @< B, !.
   86normalize((A\=B),(B\=A)) :-
   87    B @< A, !.
   88normalize((A\=B),false) :-
   89    A == B, !.
   90normalize(?(X:P),?(Y:Q)) :-
   91    sort(X,Y),
   92    normalize(P,Q), !.
   93normalize(!(X:P),!(Y:Q)) :-
   94    sort(X,Y),
   95    normalize(P,Q), !.
   96normalize(~P,~Q) :-
   97    normalize(P,Q), !.
   98normalize((P1 & Q1),(P2 & Q2)) :-
   99    normalize(P1,P2),
  100    normalize(Q1,Q2), !.
  101normalize((P1 | Q1),(P2 | Q2)) :-
  102    normalize(P1,P2),
  103    normalize(Q1,Q2), !.
  104normalize((P1 => Q1),(P2 => Q2)) :-
  105    normalize(P1,P2),
  106    normalize(Q1,Q2), !.
  107normalize((P1 <=> Q1),(P2 <=> Q2)) :-
  108    normalize(P1,P2),
  109    normalize(Q1,Q2), !.
  110normalize(knows(A,P),knows(A,Q)) :-
  111    normalize(P,Q), !.
  112normalize(pknows(E,P),pknows(E,Q)) :-
  113    normalize(P,Q), !.
  114normalize(pknows0(E,P),pknows0(E,Q)) :-
  115    normalize(P,Q), !.
  116normalize(P,P). 
  117
  118
  119%
  120%  struct_equiv(P,Q)  -  two formulae are structurally equivalent,
  121%                        basically meaning they are identical up
  122%                        to renaming of variables.
  123%
  124%  struct_oppos(P,Q)  -  two formulae are structurally opposed,
  125%                        making their conjunction a trivial falsehood.
  126%
  127
  128struct_equiv(P,Q) :-
  129    is_atom(P), is_atom(Q), P==Q.
  130struct_equiv(P1 & P2,Q1 & Q2) :-
  131    struct_equiv(P1,Q1),
  132    struct_equiv(P2,Q2).
  133struct_equiv(P1 | P2,Q1 | Q2) :-
  134    struct_equiv(P1,Q1),
  135    struct_equiv(P2,Q2).
  136struct_equiv(P1 => P2,Q1 => Q2) :-
  137    struct_equiv(P1,Q1),
  138    struct_equiv(P2,Q2).
  139struct_equiv(P1 <=> P2,Q1 <=> Q2) :-
  140    struct_equiv(P1,Q1),
  141    struct_equiv(P2,Q2).
  142struct_equiv(~P,~Q) :-
  143    struct_equiv(P,Q).
  144struct_equiv(?([] : P),?([] : Q)) :-
  145    struct_equiv(P,Q).
  146struct_equiv(?([V1:T|Vs1] : P),?([V2:T|Vs2] : Q)) :-
  147    subs(V1,V2,P,P1),
  148    struct_equiv(?(Vs1 : P1),?(Vs2 : Q)).
  149struct_equiv(!([] : P),!([] : Q)) :-
  150    struct_equiv(P,Q).
  151struct_equiv(!([V1:T|Vs1] : P),!([V2:T|Vs2] : Q)) :-
  152    subs(V1,V2,P,P1),
  153    struct_equiv(!(Vs1 : P1),!(Vs2 : Q)).
  154struct_equiv(knows(A,P),knows(A,Q)) :-
  155    struct_equiv(P,Q).
  156struct_equiv(pknows(E,P),pknows(E,Q)) :-
  157    struct_equiv(P,Q).
  158struct_equiv(pknows0(E,P),pknows0(E,Q)) :-
  159    struct_equiv(P,Q).
  160
  161struct_oppos(P,Q) :-
  162    P = ~P1, struct_equiv(P1,Q) -> true
  163    ;
  164    Q = ~Q1, struct_equiv(P,Q1) -> true
  165    ;
  166    P=true, Q=false -> true
  167    ;
  168    P=false, Q=true.
  169
  170
  171%
  172%  contradictory(F1,F2)  -  F1 and F2 are trivially contradictory,
  173%                           meaning F1 -> ~F2 and F2 -> ~F1
  174%
  175
  176contradictory(F1,F2) :-
  177    struct_oppos(F1,F2) -> true
  178    ;
  179    free_vars(F1,Vars1), member(V1,Vars1),
  180    free_vars(F2,Vars2), member(V2,Vars2),
  181    V1 == V2,
  182    really_var_given_value(V1,F1,B), 
  183    really_var_given_value(V2,F2,C),
  184    (\+ unifiable(B,C,_)) -> true
  185    ;
  186    fail.
  187
  188really_var_given_value(A,B,C):- call(call,var_given_value(A,B,C)).
  189%
  190%  fml_compare  -  provide a standard order over formula terms
  191%
  192%  This allows them to be sorted, have duplicates removed, etc.
  193%  Formula should be normalised before this is applied.
  194%
  195fml_compare('=',F1,F2) :-
  196    struct_equiv(F1,F2), !.
  197fml_compare(Ord,F1,F2) :-
  198    ( F1 @< F2 ->
  199        Ord = '<'
  200    ;
  201        Ord = '>'
  202    ).
  203
  204
  205%
  206%  contains_var(A,V)  -  formula A contains variable V
  207%
  208%  ncontains_var(A,V)  -  formula A does not contain variable V
  209%
  210%
  211%  Since we know that V is a variable, we do this test by making a copy,
  212%  grounding the copied variable, then checking for structural equivalence
  213%  with the original term.
  214%
  215contains_var(A,V:_) :-
  216    copy_term(A:V,A2:V2),
  217    V2=groundme,
  218    A \=@= A2.
  219
  220ncontains_var(A,V:_) :-
  221    copy_term(A:V,A2:V2),
  222    V2=groundme,
  223    A =@= A2.
  224    
  225
  226%
  227%  flatten_op(Op,Terms,Result) - flatten repeated ops into a list
  228%
  229%  This precicate succeeds when Result is a list of terms from Terms,
  230%  which were joined by the operator Op.  Basically allows a tree of
  231%  similar operators such as ((A & B) & (C & (D & E))) to be flattened
  232%  into a list (A,B,C,D,E).
  233%
  234
  235% :- index(flatten_op(0,1,0)).
  236
  237flatten_op(_,[],[]).
  238flatten_op(O,[T|Ts],Res) :-
  239    %( var(T) ->
  240    %    Res = [T|Res2],
  241    %    flatten_op(O,Ts,Res2)
  242    ( T =.. [O|Args] ->
  243        append(Args,Ts,Ts2),
  244        flatten_op(O,Ts2,Res)
  245    ;
  246        Res = [T|Res2],
  247        flatten_op(O,Ts,Res2)
  248    ).
  249
  250%
  251%  flatten_quant(Q,Ts,VarsIn,VarsOut,Body) - flatten nested quantifiers
  252%
  253flatten_quant(Q,T,Vars,Vars,T) :-
  254    \+ functor(T,Q,1), !.
  255flatten_quant(Q,T,Acc,Vars,Body) :-
  256    T =.. [Q,(V : T2)],
  257    append(V,Acc,Acc2),
  258    flatten_quant(Q,T2,Acc2,Vars,Body).
  259
  260%
  261%  flatten_quant_and_simp(Q,BodyIn,VarsIn,VarsOut,BodyOut)
  262%       - flatten nested quantifiers, and apply simplification
  263%
  264%  Just like flatten_quant/5 above, but applies simplify/2 to the body
  265%  when it does not match the quantifier, in case its simplification
  266%  does match.
  267%
  268flatten_quant_and_simp(Q,T,VarsIn,VarsOut,Body) :-
  269    ( T =.. [Q,(V : T2)] ->
  270      append(V,VarsIn,Vars2),
  271      flatten_quant_and_simp(Q,T2,Vars2,VarsOut,Body)
  272    ;
  273      simplify1(T,Tsimp),
  274      ( Tsimp =.. [Q,(V : T2)] ->
  275          append(V,VarsIn,Vars2),
  276          flatten_quant_and_simp(Q,T2,Vars2,VarsOut,Body)
  277      ;
  278          Body = Tsimp, VarsIn = VarsOut
  279      )
  280    ).
  281
  282
  283%
  284%  ismember(Elem,List)  -  like member/2, but does not bind variables or
  285%                          allow backtracking.
  286%
  287ismember(_,[]) :- fail.
  288ismember(E,[H|T]) :-
  289    ( E == H ->
  290        true
  291    ;
  292        ismember(E,T)
  293    ).
  294
  295%
  296%  vdelete(List,Elem,Result) - like delete/3 but using equivalence rather
  297%                              than unification, so it can be used on lists
  298%                              of variables
  299%
  300vdelete([],_,[]).
  301vdelete([H|T],E,Res) :-
  302    ( E == H ->
  303        vdelete(T,E,Res)
  304    ;
  305        Res = [H|T2],
  306        vdelete(T,E,T2)
  307    ).
  308
  309% :- index(vdelete_list(0,1,0)).
  310
  311vdelete_list(L,[],L).
  312vdelete_list(L,[H|T],L2) :-
  313    vdelete(L,H,L1),
  314    vdelete_list(L1,T,L2).
  315
  316
  317%
  318%  indep_of_vars(Vars,P)  -  P contains none of the vars in the list Vars,
  319%                            i.e. it is independent of the vars.
  320%
  321indep_of_vars(Vars,P) :-
  322    \+ ( member(X,Vars), contains_var(P,X) ).
  323
  324
  325%
  326%  var_in_list(Var,VarL)  -  variable V is in the list VarL
  327%
  328var_in_list([],_) :- fail.
  329var_in_list([H|T],V) :-
  330    ( V == H ->
  331        true
  332    ;
  333        var_in_list(T,V)
  334    ).
  335
  336%
  337%  pairfrom(L,E1,E2,Rest)  -  E1 and E2 are a pair of (different) elements
  338%                             from L, wile Rest is the rest of the list
  339%
  340%  Like doing (member(E1,L), member(E2,L))  but more efficient, doesnt match
  341%  E1 and E2 to the same element, and doesnt generate equivalent permutations.
  342%
  343pairfrom(L,E1,E2,Rest) :-
  344    pairfrom_rec(L,[],E1,E2,Rest).
  345
  346pairfrom_rec([H|T],Rest1,E1,E2,Rest) :-
  347    E1 = H, select(E2,T,Rest2), append(Rest1,Rest2,Rest)
  348    ;
  349    pairfrom_rec(T,[H|Rest1],E1,E2,Rest).
  350
  351
  352%
  353%  simplify(+F1,-F2) - simplify a formula
  354%  
  355%  This predicate applies some basic simplification rules to a formula
  356%  to eliminate redundancy and (hopefully) speed up future reasoning.
  357%  
  358
  359simplify(P,S) :-
  360    normalize(P,Nml),
  361    simplify1(Nml,S1),
  362    fml2nnf(S1,Nnf),
  363    simplify1(Nnf,S).
  364
  365simplify1(P,P) :-
  366    is_atom(P), P \= (_ = _), P \= (_ \= _).
  367simplify1(P & Q,S) :-
  368    flatten_op('&',[P,Q],TermsT),
  369    simplify1_conjunction(TermsT,TermsS),
  370    ( TermsS = [] ->
  371        S = true
  372    ;
  373        % This will remove duplicates, which includes struct_equiv formulae
  374        predsort(fml_compare,TermsS,Terms),
  375        joinlist('&',Terms,S)
  376    ).
  377simplify1(P | Q,S) :-
  378    flatten_op('|',[P,Q],TermsT),
  379    simplify1_disjunction(TermsT,TermsS),
  380    ( TermsS = [] ->
  381        S = false
  382    ;
  383        % This will remove duplicates, which includes struct_equiv formulae
  384        predsort(fml_compare,TermsS,Terms),
  385        joinlist('|',Terms,S)
  386    ).
  387simplify1(P => Q,S) :-
  388    simplify1(P,Sp),
  389    simplify1(Q,Sq),
  390    (
  391        Sp=false -> S=true
  392    ;
  393        Sp=true -> S=Sq
  394    ;
  395        Sq=true -> S=true
  396    ;
  397        Sq=false -> S=(~Sp)
  398    ;
  399        S = (Sp => Sq)
  400    ).
  401simplify1(P <=> Q,S) :-
  402    simplify1(P,Sp),
  403    simplify1(Q,Sq),
  404    (
  405        struct_equiv(P,Q) -> S=true
  406    ;
  407        struct_oppos(P,Q) -> S=false
  408    ;
  409        Sp=false -> S=(~Sq)
  410    ;
  411        Sq=true -> S=Sq
  412    ;
  413        Sq=false -> S=(~Sp)
  414    ;
  415        Sq=true -> S=Sp
  416    ;
  417        S = (Sp <=> Sq)
  418    ).
  419simplify1(~P,S) :-
  420    simplify1(P,SP),
  421    (
  422        SP=false -> S=true
  423    ;
  424        SP=true -> S=false
  425    ;
  426        SP = ~P2 -> S=P2
  427    ;
  428        SP = (A\=B) -> S=(A=B)
  429    ;
  430        S = ~SP
  431    ).
  432simplify1(!(Xs:P),S) :-
  433    ( Xs = [] -> simplify1(P,S)
  434    ;
  435    flatten_quant_and_simp('!',P,Xs,VarsT,Body),
  436    sort(VarsT,Vars),
  437    (
  438        Body=false -> S=false
  439    ;
  440        Body=true -> S=true
  441    ;
  442        % Remove any useless variables
  443        partition(ncontains_var(Body),Vars,_,Vars2),
  444        ( Vars2 = [] ->
  445            S2 = Body
  446        ;
  447          % Pull independent components outside the quantifier.
  448          % Both conjuncts and disjuncts can be handled in this manner.
  449          (flatten_op('|',[Body],BTerms), BTerms = [_,_|_] -> 
  450            partition(indep_of_vars(Vars),BTerms,Indep,BT2),
  451            % Because we have removed useless vars, BT2 cannot be empty
  452            joinlist('|',BT2,Body2),
  453            ( Indep = [] ->
  454              S2=!(Vars2:Body2)
  455            ;
  456              joinlist('|',Indep,IndepB),
  457              S2=(!(Vars2:Body2) | IndepB)
  458            )
  459          
  460          ; flatten_op('&',[Body],BTerms), BTerms = [_,_|_] ->
  461            partition(indep_of_vars(Vars),BTerms,Indep,BT2),
  462            joinlist('&',BT2,Body2),
  463            ( Indep = [] ->
  464              S2=!(Vars2:Body2)
  465            ;
  466              joinlist('&',Indep,IndepB),
  467              S2=(!(Vars2:Body2) & IndepB)
  468            )
  469          ;
  470            S2=!(Vars2:Body)
  471          )
  472        ),
  473        S = S2
  474    )).
  475simplify1(?(Xs:P),S) :-
  476   ( Xs = [] -> simplify1(P,S)
  477   ;
  478   flatten_quant_and_simp('?',P,Xs,VarsT,Body),
  479   sort(VarsT,Vars),
  480   (
  481       Body=false -> S=false
  482   ;
  483       Body=true -> S=true
  484   ;
  485       % Remove vars that are assigned a specific value, simply replacing
  486       % them with their value in the Body formula
  487       member(V1:T1,Vars), var_valuated(V1,Body,Body2) ->
  488           vdelete(Vars,V1:T1,Vars2), simplify1(?(Vars2:Body2),S)
  489   ;
  490       % Remove any useless variables
  491       partition(ncontains_var(Body),Vars,_,Vars2),
  492       ( Vars2 = [] ->
  493           S = Body
  494       ;
  495         % Pull independent components outside the quantifier,
  496         % Both conjuncts and disjuncts can be handled in this manner.
  497         (flatten_op('|',[Body],BTerms), BTerms = [_,_|_] -> 
  498           partition(indep_of_vars(Vars),BTerms,Indep,BT2),
  499           joinlist('|',BT2,Body2),
  500           ( Indep = [] ->
  501             S = ?(Vars2:Body2)
  502           ;
  503             joinlist('|',Indep,IndepB),
  504             S = (?(Vars2:Body2) | IndepB)
  505           )
  506         ; flatten_op('&',[Body],BTerms), BTerms = [_,_|_] ->
  507           partition(indep_of_vars(Vars),BTerms,Indep,BT2),
  508           joinlist('&',BT2,Body2),
  509           ( Indep = [] ->
  510             S = ?(Vars2:Body2)
  511           ;
  512             joinlist('&',Indep,IndepB),
  513             S = (?(Vars2:Body2) & IndepB)
  514           )
  515         ;
  516           S = ?(Vars2:Body)
  517         )
  518       )
  519   )).
  520simplify1((A=B),S) :-
  521   (
  522       A == B -> S=true
  523   ;
  524       % Utilising the unique names assumption, we can rewrite it to
  525       % a conjunction of simpler equalities by striping functors, or
  526       % to false if the terms will never unify
  527       ( unifiable(A,B,Eqs) ->
  528           joinlist('&',Eqs,S1),
  529           normalize(S1,S)
  530       ;
  531           S=false
  532       )
  533   ).
  534simplify1((A\=B),S) :-
  535   (
  536       A == B -> S=false
  537   ;
  538       % Utilising the unique names assumption, we can rewrite it to
  539       % a disjunction of simpler inequalities by striping functors, or
  540       % to true if the terms will never unify
  541       ( unifiable(A,B,Eqs) ->
  542           joinlist('&',Eqs,S1),
  543           normalize(S1,S2),
  544           S = ~S2
  545       ;
  546           S = true
  547       )
  548   ).
  549simplify1(knows(A,P),S) :-
  550   simplify1(P,Ps),
  551   ( Ps=true -> S=true
  552   ; Ps=false -> S=false
  553   ; S = knows(A,Ps)
  554   ).
  555simplify1(pknows(E,P),S) :-
  556   simplify_epath(E,Es),
  557   simplify1(P,Ps),
  558   ( Ps=true -> S=true
  559   ; Ps=false -> S=false
  560   ; Es=(?false) -> S=true
  561   ; Es=(?true) -> S=Ps
  562   ; S = pknows(Es,Ps)
  563   ).
  564simplify1(pknows0(E,P),S) :-
  565   simplify_epath(E,Es),
  566   simplify1(P,Ps),
  567   ( Ps=true -> S=true
  568   %; Ps=false -> S=false  % this may be OK if Es=(?false) but we can't
  569                           % always detect such a case
  570   ; Es=(?false) -> S=true
  571   ; Es=(?true) -> S=Ps
  572   ; S = pknows0(Es,Ps)
  573   ).
  574
  575
  576%
  577%  simplify1_conjunction(In,Out)  -  simplify the conjunction of list of fmls
  578%  simplify1_disjunction(In,Out)  -  simplify the disjunction of list of fmls
  579%
  580
  581simplify1_conjunction(FmlsIn,FmlsOut) :-
  582    maplist(simplify1,FmlsIn,FmlsI1),
  583    simplify1_conjunction_rules(FmlsI1,FmlsI2),
  584    simplify1_conjunction_acc(FmlsI2,[],FmlsOut).
  585
  586simplify1_conjunction_rules(ConjsI,ConjsO) :-
  587    (pairfrom(ConjsI,C1,C2,Rest), (simplify1_conjunction_rule(C1,C2,C1o,C2o) ; simplify1_conjunction_rule(C2,C1,C2o,C1o)) ->
  588      simplify1_conjunction_rules([C1o,C2o|Rest],ConjsO)
  589    ;
  590      ConjsO = ConjsI
  591    ).
  592 
  593simplify1_conjunction_rule(C1,C2,C1,C2o) :-
  594    C2 = (C2a | C2b),
  595    ( struct_oppos(C1,C2a), C2o=C2b
  596    ; struct_oppos(C1,C2b), C2o=C2a
  597    ).
  598simplify1_conjunction_rule(C1,C2,C1,true) :-
  599    C2 = (C2a | C2b),
  600    ( struct_equiv(C1,C2a)
  601    ; struct_equiv(C1,C2b)
  602    ).
  603    
  604
  605
  606simplify1_conjunction_acc([],FmlsAcc,FmlsAcc).
  607simplify1_conjunction_acc([F|FmlsIn],FmlsAcc,FmlsOut) :-
  608    ( member(Eq,FmlsAcc), struct_equiv(F,Eq) ->
  609        F2 = true
  610    ; member(Opp,FmlsAcc), struct_oppos(F,Opp) ->
  611        F2 = false
  612    ;
  613        F2 = F
  614    ),
  615    ( F2=true ->
  616        simplify1_conjunction_acc(FmlsIn,FmlsAcc,FmlsOut)
  617    ; F2=false ->
  618        FmlsOut=[false]
  619    ;
  620        simplify1_conjunction_acc(FmlsIn,[F2|FmlsAcc],FmlsOut)
  621    ).
  622    
  623
  624simplify1_disjunction(FmlsIn,FmlsOut) :-
  625    maplist(simplify1,FmlsIn,FmlsI1),
  626    simplify1_disjunction_rules(FmlsI1,FmlsI2),
  627    simplify1_disjunction_acc(FmlsI2,[],FmlsOut).
  628
  629simplify1_disjunction_rules(DisjI,DisjO) :-
  630    (pairfrom(DisjI,D1,D2,Rest), (simplify1_disjunction_rule(D1,D2,D1o,D2o) ; simplify1_disjunction_rule(D2,D1,D2o,D1o)) ->
  631      simplify1_disjunction_rules([D1o,D2o|Rest],DisjO)
  632    ;
  633      DisjO = DisjI
  634    ).
  635 
  636simplify1_disjunction_rule(D1,D2,D1,D2o) :-
  637    D2 = (D2a & D2b),
  638    ( struct_oppos(D1,D2a), D2o=D2b
  639    ; struct_oppos(D1,D2b), D2o=D2a
  640    ).
  641simplify1_disjunction_rule(D1,D2,D1,false) :-
  642    D2 = (D2a & D2b),
  643    ( struct_equiv(D1,D2a)
  644    ; struct_equiv(D1,D2b)
  645    ).
  646
  647simplify1_disjunction_acc([],FmlsAcc,FmlsAcc).
  648simplify1_disjunction_acc([F|FmlsIn],FmlsAcc,FmlsOut) :-
  649    ( member(Eq,FmlsAcc), struct_equiv(F,Eq) ->
  650        F2 = false
  651    ; member(Opp,FmlsAcc), struct_oppos(F,Opp) ->
  652        F2 = true
  653    ;
  654        F2 = F
  655    ),
  656    ( F2=false ->
  657        simplify1_disjunction_acc(FmlsIn,FmlsAcc,FmlsOut)
  658    ; F2=true ->
  659        FmlsOut=[true]
  660    ;
  661        simplify1_disjunction_acc(FmlsIn,[F2|FmlsAcc],FmlsOut)
  662    ).
  663
  664
  665%
  666%  var_given_value(X,P,V,Q)  -  variable X is uniformly given the value V
  667%                               within the formula P.  Q is a formula equiv
  668%                               to P, with variable X set to V.
  669%
  670%  var_given_value_list(X,Ps,V,Qs)  -  variable X is uniformly given the value
  671%                                      V in all formulae in list Ps.
  672% 
  673%  Determining Q from P is not a simple substitution - if the value V
  674%  contains vars that are introduced by a quantifier in P, this quantifier
  675%  must be lifted to outermost scope.
  676%
  677
  678/*
  679% :- index(var_given_value(0,1,0,0)).
  680% :- index(var_given_value_list(0,1,0,0)).
  681*/
  682
  683var_given_value(X,A=B,V,true) :-
  684    ( X == A ->
  685        V = B
  686    ;
  687        X == B, V = A
  688    ).
  689var_given_value(X,P1 & P2,V,Q) :-
  690    flatten_op('&',[P1,P2],Cjs),
  691    select(Cj,Cjs,Rest), var_given_value(X,Cj,V,Qj),
  692    partition(vgv_partition(X),Rest,Deps,Indeps),
  693    (Indeps = [] -> IndepFml=true ; joinlist('&',Indeps,IndepFml)),
  694    (Deps = [] -> DepFml1=true ; joinlist('&',Deps,DepFml1)),
  695    subs(X,V,DepFml1,DepFml),
  696    % We may have lifted a variable outside the scope of its
  697    % quantifier.  We must push QRest back down through the quantifiers
  698    % to rectify this.  By invariants of the operation, we know all 
  699    % relevant quantifiers are at outermost scope in Qj.
  700    (DepFml \= true ->
  701      term_variables(V,Vars),
  702      vgv_push_into_quantifiers(Vars,Qj,DepFml,QFml)
  703    ;
  704      QFml = Qj
  705    ),
  706    Q = (IndepFml & QFml), !.
  707var_given_value(X,P1 | P2,V,Q) :-
  708    flatten_op('|',[P1,P2],Djs),
  709    var_given_value_list(X,Djs,V,Qs),
  710    joinlist('|',Qs,Q).
  711var_given_value(X,!(Vars:P),V,!(VarsQ:Q)) :-
  712    var_given_value(X,P,V,Q2),
  713    flatten_quant('!',Q2,Vars,VarsQ,Q).
  714var_given_value(X,?(Vars:P),V,?(VarsQ:Q)) :-
  715    var_given_value(X,P,V,Q2),
  716    flatten_quant('?',Q2,Vars,VarsQ,Q).
  717var_given_value(X,knows(A,P),V,knows(A,Q)) :-
  718    var_given_value(X,P,V,Q).
  719var_given_value(X,pknows(E,P),V,pknows(E,Q)) :-
  720    var_given_value(X,P,V,Q).
  721var_given_value(X,pknows0(E,P),V,pknows0(E,Q)) :-
  722    var_given_value(X,P,V,Q).
  723% There's no clause for ~P because that can never give X a specific value
  724
  725var_given_value_list(_,[],_,[]).
  726var_given_value_list(X,[H|T],V,[Qh|Qt]) :-
  727    % Be careful not to do any unification on V.
  728    % This ruins tail-recursion, but meh...
  729    var_given_value(X,H,V,Qh),
  730    var_given_value_list(X,T,V2,Qt),
  731    V == V2.
  732
  733vgv_partition(V,F) :-
  734    contains_var(F,V:_).
  735
  736%  We can stop recursing either when Vars=[] or when we are
  737%  no longer at a quantifier, since we assume all relevant 
  738%  quantifiers have been brought to the front.
  739vgv_push_into_quantifiers(Vars,?(Qv:Qj),QDep,?(Qv:Q)) :-
  740    Vars \= [], !,
  741    vgv_subtract(Vars,Qv,Vars2),
  742    vgv_push_into_quantifiers(Vars2,Qj,QDep,Q).
  743vgv_push_into_quantifiers(Vars,!(Qv:Qj),QDep,!(Qv:Q)) :-
  744    Vars \= [], !,
  745    vgv_subtract(Vars,Qv,Vars2),
  746    vgv_push_into_quantifiers(Vars2,Qj,QDep,Q).
  747vgv_push_into_quantifiers(_,Qj,QDep,Qj & QDep).
  748
  749vgv_subtract([],_,[]).
  750vgv_subtract(Vs,[],Vs).
  751vgv_subtract(Vs,[X:_|Xs],Vs2) :-
  752    vgv_subtract_helper(Vs,X,Vs1),
  753    vgv_subtract(Vs1,Xs,Vs2).
  754
  755vgv_subtract_helper([],_,[]).
  756vgv_subtract_helper([V|Vs],X,Vs2) :-
  757    ( X == V ->
  758        vgv_subtract_helper(Vs,X,Vs2)
  759    ;
  760        Vs2 = [V|Vs22],
  761        vgv_subtract_helper(Vs,X,Vs22)
  762    ).
  763
  764%
  765%  var_valuated(X,P,P2)  -  variable X takes specific values throughout P,
  766%                           and P2 is P with the appropriate valuations
  767%                           inserted.
  768%
  769
  770% :- index(var_valuated(0,1,0)).
  771% :- index(var_valuated_list(0,1,0)).
  772% :- index(var_valuated_distribute(0,1,0,0)).
  773
  774% In the base case, X is given a single value throughout the entire formula.
  775var_valuated(X,P,Q) :-
  776   var_given_value(X,P,_,Q), !.
  777
  778% The base case for P & Q - when they both give X the same value - is
  779% already covered by the var_valuated/3 clause above.  But if one of the 
  780% conjuncts is a disjunction that valuates X, then we can distribute over
  781% it to achieve a valuation.
  782var_valuated(X,P & Q,V) :-
  783   flatten_op('&',[P,Q],Cjs),
  784   select(Cj,Cjs,RestCjs),
  785   flatten_op('|',[Cj],Djs),
  786   maplist(var_valuated_check(X),Djs), !,
  787   joinlist('&',RestCjs,RestFml),
  788   var_valuated_distribute(X,Djs,RestFml,VDjs),
  789   joinlist('|',VDjs,V), !.
  790var_valuated(X,P | Q,V) :-
  791   flatten_op('|',[P,Q],Cs),
  792   var_valuated_list(X,Cs,Vs),
  793   joinlist('|',Vs,V).
  794var_valuated(X,!(V:P),!(V:Q)) :-
  795   var_valuated(X,P,Q).
  796var_valuated(X,?(V:P),?(V:Q)) :-
  797   var_valuated(X,P,Q).
  798
  799var_valuated_list(_,[],[]).
  800var_valuated_list(X,[H|T],[Hv|Tv]) :-
  801   var_valuated(X,H,Hv),
  802   var_valuated_list(X,T,Tv).
  803
  804var_valuated_distribute(_,[],_,[]).
  805var_valuated_distribute(X,[P|Ps],Q,[Pv|T]) :-
  806   var_valuated(X,P & Q,Pv),
  807   var_valuated_distribute(X,Ps,Q,T).
  808
  809var_valuated_check(X,F) :-
  810   %var_valuated(X,F,_).
  811   var_given_value(X,F,_,_).
  812
  813
  814%
  815%  joinlist(+Op,+In,-Out) - join items in a list using given operator
  816%
  817
  818joinlist(_,[H],H) :- !.
  819joinlist(O,[H|T],J) :-
  820    T \= [],
  821    J =.. [O,H,TJ],
  822    joinlist(O,T,TJ).
  823
  824%
  825%  subs(Name,Value,Old,New):  substitue values in a term
  826%
  827%  This predicate is true when New is equal to Old with all occurances
  828%  of Name replaced by Value - basically, a symbolic substitution
  829%  routine.  For example, it is usually used to produce a result such
  830%  as:
  831%
  832%      subs(now,S,fluent(now),fluent(S)).
  833%
  834subs(X,Y,T,Tr) :-
  835    T == X, Tr = Y, !.
  836subs(X,_,T,Tr) :-
  837    T \== X, var(T), T=Tr, !.
  838subs(X,Y,T,Tr) :-
  839    T \== X, nonvar(T), T =.. [F|Ts], subs_list(X,Y,Ts,Trs), Tr =.. [F|Trs], !.
  840
  841%
  842%  subs_list(Name,Value,Old,New):  value substitution in a list
  843%
  844%  This predicate operates as subs/4, but Old and New are lists of terms
  845%  instead of single terms.  Basically, it calls subs/4 recursively on
  846%  each element of the list.
  847%
  848subs_list(_,_,[],[]).
  849subs_list(X,Y,[T|Ts],[Tr|Trs]) :-
  850    subs(X,Y,T,Tr), subs_list(X,Y,Ts,Trs).
  851
  852
  853%
  854%  fml2nnf:  convert a formula to negation normal form
  855%
  856fml2nnf(P <=> Q,N) :-
  857    fml2nnf((P => Q) & (Q => P),N), !.
  858fml2nnf(P => Q,N) :-
  859    fml2nnf((~P) | Q,N), !.
  860fml2nnf(~(P <=> Q),N) :-
  861    fml2nnf(~(P => Q) & ~(Q => P),N), !.
  862fml2nnf(~(P => Q),N) :-
  863    fml2nnf(P & ~Q,N), !.
  864fml2nnf(~(P & Q),N) :-
  865   fml2nnf((~P) | (~Q),N), !.
  866fml2nnf(~(P | Q),N) :-
  867   fml2nnf((~P) & (~Q),N), !.
  868fml2nnf(~(!(X:P)),N) :-
  869   fml2nnf( ?(X : ~P) ,N), !.
  870fml2nnf(~(?(X:P)),N) :-
  871   fml2nnf(!(X : ~P),N), !.
  872fml2nnf(~(~P),N) :-
  873    fml2nnf(P,N), !.
  874fml2nnf(P & Q,Np & Nq) :-
  875    fml2nnf(P,Np), fml2nnf(Q,Nq), !.
  876fml2nnf(P | Q,Np | Nq) :-
  877    fml2nnf(P,Np), fml2nnf(Q,Nq), !.
  878fml2nnf(!(X:P),!(X:N)) :-
  879    fml2nnf(P,N), !.
  880fml2nnf(?(X:P),?(X:N)) :-
  881    fml2nnf(P,N), !.
  882fml2nnf(knows(A,P),knows(A,N)) :-
  883    fml2nnf(P,N), !.
  884fml2nnf(pknows(E,P),pknows(E,N)) :-
  885    fml2nnf(P,N), !.
  886fml2nnf(pknows0(E,P),pknows0(E,N)) :-
  887    fml2nnf(P,N), !.
  888fml2nnf(~knows(A,P),~knows(A,N)) :-
  889    fml2nnf(P,N), !.
  890fml2nnf(~pknows(E,P),~pknows(E,N)) :-
  891    fml2nnf(P,N), !.
  892fml2nnf(~pknows0(E,P),~pknows0(E,N)) :-
  893    fml2nnf(P,N), !.
  894fml2nnf(P,P).
  895
  896%
  897%  is_atom(P)  -  the formula P is a literal atom, not a compound expression
  898%
  899%  This is used to detect the base case of many predicates that structurally
  900%  decompose formulae.
  901%
  902is_atom(P) :-
  903    P \= (~_),
  904    P \= (_ => _),
  905    P \= (_ <=> _),
  906    P \= (_ & _),
  907    P \= (_ | _),
  908    P \= ?(_:_),
  909    P \= !(_:_),
  910    P \= knows(_,_),
  911    P \= pknows(_,_),
  912    P \= pknows0(_,_).
  913
  914
  915%
  916%  copy_fml(P,Q)  -  make a copy of a formula.  The copy will have all
  917%                    bound variables renamed to new vars.  Any free variables
  918%                    will retain their original names.
  919%
  920
  921copy_fml(P,P) :-
  922    var(P), !.
  923copy_fml(P,P) :-
  924    is_atom(P).
  925copy_fml(P & Q,R & S) :-
  926    copy_fml(P,R),
  927    copy_fml(Q,S).
  928copy_fml(P | Q,R | S) :-
  929    copy_fml(P,R),
  930    copy_fml(Q,S).
  931copy_fml(P => Q,R => S) :-
  932    copy_fml(P,R),
  933    copy_fml(Q,S).
  934copy_fml(P <=> Q,R <=> S) :-
  935    copy_fml(P,R),
  936    copy_fml(Q,S).
  937copy_fml(~P,~Q) :-
  938    copy_fml(P,Q).
  939copy_fml(!(VarsP:P),!(VarsQ:Q)) :-
  940    rename_vars(VarsP,P,VarsQ,P2),
  941    copy_fml(P2,Q).
  942copy_fml(?(VarsP:P),?(VarsQ:Q)) :-
  943    rename_vars(VarsP,P,VarsQ,P2),
  944    copy_fml(P2,Q).
  945copy_fml(knows(A,P),knows(A,Q)) :-
  946    copy_fml(P,Q).
  947copy_fml(pknows(E,P),pknows(F,Q)) :-
  948    copy_epath(E,F),
  949    copy_fml(P,Q).
  950copy_fml(pknows0(E,P),pknows0(F,Q)) :-
  951    copy_epath(E,F),
  952    copy_fml(P,Q).
  953
  954%
  955%  rename_vars(Vars,F,NewVars,NewF)  -  rename the given variables to new
  956%                                       ones, producing a modified formula.
  957%
  958rename_vars(Vs,P,Vs2,P2) :-
  959    rename_vars(Vs,P,[],Vs2,P2).
  960
  961rename_vars([],P,Acc,Acc,P).
  962rename_vars([V:T|Vs],P,Acc,NewV,NewP) :-
  963    subs(V,V2,P,P2),
  964    append(Acc,[V2:T],Acc2),
  965    rename_vars(Vs,P2,Acc2,NewV,NewP).
  966
  967%
  968%  free_vars(Fml,Vars)  -  list of all free variables in the formula
  969%
  970%  "Free" is in the FOL sense of "not bound by an enclosing quantifier"
  971%
  972free_vars(Fml,Vars) :-
  973    copy_fml(Fml,Fml2),
  974    term_variables(Fml,Vars1),
  975    term_variables(Fml2,Vars2),
  976    vars_in_both(Vars1,Vars2,[],Vars).
  977
  978vars_in_both([],_,Vars,Vars).
  979vars_in_both([H|T],V2,Acc,Vars) :-
  980    ( ismember(H,V2) ->
  981        vars_in_both(T,V2,[H|Acc],Vars)
  982    ;
  983        vars_in_both(T,V2,Acc,Vars)
  984    ).
  985    
  986
  987write_eqn(P) :-
  988    write('\\begin{multline}'),nl,write_latex(P),nl,write('\\end{multline}').
  989
  990write_latex(P) :-
  991  copy_fml(P,Pc),
  992  number_vars(Pc),
  993  do_write_latex(Pc).
  994
  995do_write_latex(P) :-
  996    var(P), write(P), !.
  997do_write_latex(P <=> Q) :-
  998    do_write_latex(P), write(' \\equiv '), do_write_latex(Q).
  999do_write_latex(P => Q) :-
 1000    do_write_latex(P), write(' \\rightarrow '), do_write_latex(Q).
 1001do_write_latex(~P) :-
 1002    write(' \\neg '), do_write_latex(P).
 1003do_write_latex(P & Q) :-
 1004    flatten_op('&',[P & Q],[C|Cs]),
 1005    write(' \\left( '), do_write_latex(C), reverse(Cs,CsR),
 1006    do_write_latex_lst(CsR,' \\wedge '), write(' \\right) ').
 1007do_write_latex(P | Q) :-
 1008    flatten_op('|',['|'(P,Q)],[C|Cs]),
 1009    do_write_latex(C), reverse(Cs,CsR),
 1010    do_write_latex_lst(CsR,' \\vee ').
 1011do_write_latex(!([X|Xs]:P)) :-
 1012    write(' \\forall '),
 1013    do_write_latex(X),
 1014    do_write_latex_lst(Xs,','),
 1015    write(' : \\left[ '),
 1016    do_write_latex(P),
 1017    write(' \\right] ').
 1018do_write_latex(?([X|Xs]:P)) :-
 1019    write(' \\exists '),
 1020    do_write_latex(X),
 1021    do_write_latex_lst(Xs,','),
 1022    write(' : \\left[ '),
 1023    do_write_latex(P),
 1024    write(' \\right] ').
 1025do_write_latex(knows(A,P)) :-
 1026    write(' \\Knows( '),
 1027    do_write_latex(A),
 1028    write(','),
 1029    do_write_latex(P),
 1030    write(')').
 1031do_write_latex(pknows(E,P)) :-
 1032    write(' \\PKnows( '),
 1033    do_write_latex(E),
 1034    write(','),
 1035    do_write_latex(P),
 1036    write(')').
 1037do_write_latex(P) :-
 1038    is_atom(P), write(P).
 1039
 1040do_write_latex_lst([],_).
 1041do_write_latex_lst([T|Ts],Sep) :-
 1042    write(Sep), nl, do_write_latex(T), do_write_latex_lst(Ts,Sep).
 1043
 1044
 1045number_vars(X) :-
 1046    term_variables(X,Vs),
 1047    number_vars_rec(Vs,0).
 1048number_vars_rec([],_).
 1049number_vars_rec([V|Vs],N) :-
 1050    name(x,N1), name(N,N2), append(N1,N2,Codes),
 1051    atom_codes(V,Codes),
 1052    Ns is N + 1,
 1053    number_vars_rec(Vs,Ns).
 1054
 1055
 1056%
 1057%  pp_fml(P)  -  pretty-print the formula P
 1058%
 1059
 1060pp_fml(P) :-
 1061    copy_fml(P,F), fml2nnf(F,N), number_vars(N),
 1062    pp_fml(N,0,0), !, nl, nl.
 1063
 1064pp_inset(0).
 1065pp_inset(N) :-
 1066    N > 0, N1 is N - 1,
 1067    write('   '), pp_inset(N1).
 1068
 1069pp_fml_list([P],_,_,O1,D1) :-
 1070    pp_fml(P,O1,D1).
 1071pp_fml_list([P1,P2|Ps],Op,D,O1,D1) :-
 1072    pp_fml(P1,O1,D1), nl,
 1073    pp_inset(D), write(Op), nl,
 1074    pp_fml_list([P2|Ps],Op,D,D1,D1).
 1075
 1076pp_fml(P1 & P2,O,D) :-
 1077    flatten_op('&',[P1,P2],Ps),
 1078    D1 is D + 1,
 1079    O1 is O + 1,
 1080    pp_fml_list(Ps,'&',D,O1,D1).
 1081pp_fml(P1 | P2,O,D) :-
 1082    flatten_op('|',[P1,P2],Ps),
 1083    D1 is D + 1,
 1084    O1 is O + 1,
 1085    pp_fml_list(Ps,'|',D,O1,D1).
 1086pp_fml(~P,O,D) :-
 1087    D1 is D + 1,
 1088    pp_inset(O), write('~  '),
 1089    pp_fml(P,0,D1).
 1090pp_fml(P1 => P2,O,D) :-
 1091    D1 is D + 1,
 1092    pp_inset(O), pp_fml(P1,1,D1), nl,
 1093    pp_inset(D), write('=>'), nl,
 1094    pp_fml(P2,D1,D1).
 1095pp_fml(P1 <=> P2,O,D) :-
 1096    D1 is D + 1,
 1097    pp_inset(O), pp_fml(P1,1,D1), nl,
 1098    pp_inset(D), write('<=>'), nl,
 1099    pp_fml(P2,D1,D1).
 1100pp_fml(!(V:P),O,D) :-
 1101    D1 is D + 1,
 1102    pp_inset(O), write('!('), write(V), write('):'), nl,
 1103    pp_fml(P,D1,D1).
 1104pp_fml(?(V:P),O,D) :-
 1105    D1 is D + 1,
 1106    pp_inset(O), write('?('), write(V), write('):'), nl,
 1107    pp_fml(P,D1,D1).
 1108pp_fml(knows(A,P),O,D) :-
 1109    D1 is D + 1,
 1110    pp_inset(O), write('knows('), write(A), write(','), nl,
 1111    pp_fml(P,D1,D1), nl,
 1112    pp_inset(D), write(')').
 1113pp_fml(pknows(E,P),O,D) :-
 1114    D1 is D + 1,
 1115    pp_inset(O), write('pknows('), nl,
 1116    pp_epath(E,D1,D1), nl,
 1117    pp_inset(D), write('-----'), nl,
 1118    pp_fml(P,D1,D1), nl,
 1119    pp_inset(D), write(')').
 1120pp_fml(pknows0(E,P),O,D) :-
 1121    D1 is D + 1,
 1122    pp_inset(O), write('pknows0('), nl,
 1123    pp_epath(E,D1,D1), nl,
 1124    pp_inset(D), write('-----'), nl,
 1125    pp_fml(P,D1,D1), nl,
 1126    pp_inset(D), write(')').
 1127pp_fml(P,O,_) :-
 1128    is_atom(P),
 1129    pp_inset(O), write(P).
 1130
 1131
 1132fml2cnf(P,P) :-
 1133    is_atom(P).
 1134fml2cnf(P1 & P2,C1 & C2) :-
 1135    fml2cnf(P1,C1),
 1136    fml2cnf(P2,C2).
 1137fml2cnf(P1 | P2,C) :-
 1138    fml2cnf(P1,C1),
 1139    fml2cnf(P2,C2),
 1140    flatten_op('&',[C1],C1s),
 1141    flatten_op('&',[C2],C2s),
 1142    setof(Cp,fml2cnf_helper(C1s,C2s,Cp),Cs),
 1143    joinlist('&',Cs,C).
 1144
 1145fml2cnf_helper(Cjs1,Cjs2,C) :-
 1146    member(C1,Cjs1), member(C2,Cjs2), C = (C1 | C2).
 1147
 1148:- begin_tests(fluent,[sto(rational_trees)]). 1149
 1150test(simp1) :-
 1151    simplify(p & true,p).
 1152test(simp2) :-
 1153    simplify(p & false,false).
 1154test(simp3) :-
 1155    simplify(p | false,p).
 1156test(simp4) :-
 1157    simplify(p | true,true).
 1158test(simp5) :-
 1159    simplify(false | false,false).
 1160test(simp6) :-
 1161    simplify(false | (p & ~(a=a)),false).
 1162test(simp7) :-
 1163    simplify(true & true,true).
 1164test(simp8) :-
 1165    simplify(!([X:t]: p(X) & p(a)),!([X:t]:p(X)) & p(a)).
 1166test(simp9) :-
 1167    simplify(?([X:t]: p(X) & p(a)),?([X:t]:p(X)) & p(a)).
 1168test(simp10) :-
 1169    X1 = ?([X:t] : ((p & (X=nil)) | (q & (X=obs) & r ) | (?([Y:o]:(s(Y) & (X=pair(a,Y))))))),
 1170    X2 = (p | ?([Y:o] : s(Y)) | (q & r)),
 1171    simplify(X1,X2).
 1172
 1173test(val1) :-
 1174    var_given_value(X,X=a,a,true).
 1175test(val2) :-
 1176    var_given_value(X,(X=a) & (X=b),b,F), simplify(F,false).
 1177test(val3) :-
 1178    var_given_value(X,p(X) & q(a) & ?([Y:t]:X=Y),Val,_),
 1179    Val == Y.
 1180
 1181test(copy1) :-
 1182    F1 = !([X:t,Y:q] : p(X) & r(Y)),
 1183    copy_fml(F1,F2),
 1184    F1 =@= F2,
 1185    F1 \== F2.
 1186
 1187:- end_tests(fluent).