common_logic_modal.pl

    1:- module(common_logic_modalization,[qualify_nesc/2]).    2
    3:-  system:((
    4 op(1199,fx,('==>')), 
    5 op(1190,xfx,('::::')),
    6 op(1180,xfx,('==>')),
    7 op(1170,xfx,'<==>'),  
    8 op(1160,xfx,('<-')),
    9 op(1150,xfx,'=>'),
   10 op(1140,xfx,'<='),
   11 op(1130,xfx,'<=>'), 
   12 op(600,yfx,'&'), 
   13 op(600,yfx,'v'),
   14 op(350,xfx,'xor'),
   15 op(300,fx,'~'),
   16 op(300,fx,'-'))).   17
   18:- op(800,xfx,'=<>=').   19
   20/*
   21
   22
   23  qualify_modality( +FmlIn, -FmlOut, [options...]).
   24
   25
   26   converts terms like...
   27
   28         loves(joe,mary)
   29
   30   Into...
   31
   32         poss(loves(joe,mary)) => nesc(loves(joe,mary)).
   33
   34   settings are...
   35
   36
   37*/
   38
   39
   40
   41:- create_prolog_flag(logicmoo_modality,none,[keep(true)]).   42
   43:- thread_local(t_l:qualify_modally/0).

qualify_modality(?P, ?Q) is det

   45qualify_modality(OuterQuantKIF,OuterQuantKIF):- current_prolog_flag(logicmoo_modality,none),!.
   46qualify_modality(PQ,PQO):- qualify_nesc(PQ,PQO).

qualify_nesc(?P, ?Q) is det: Q = (poss(P)=>P).

   56% qualify_nesc(OuterQuantKIF,OuterQuantKIF):- \+ t_l:qualify_modally,!.
   57qualify_nesc(OuterQuantKIF,OuterQuantKIF):- var(OuterQuantKIF),!.
   58qualify_nesc(IN,OUT):-is_list(IN),must_maplist_det(qualify_nesc,IN,OUT),!.
   59qualify_nesc(OuterQuantKIF,OuterQuantKIF):- leave_as_is(OuterQuantKIF),!.
   60qualify_nesc(OuterQuantKIF,OuterQuantKIF):- contains_modal(OuterQuantKIF),!.
   61qualify_nesc(PQ,PQO):- PQ=..[F|Q],is_quantifier(F),append(LQ,[RQ],Q),qualify_nesc(RQ,RQQ),append(LQ,[RQQ],QQ),PQO=..[F|QQ],!.
   62% qualify_nesc(P<=>Q,PQ & QP):- !,qualify_nesc(P=>Q,PQ),qualify_nesc(Q=>P,QP).
   63
   64% full modality
   65qualify_nesc(P,(poss(P)=>nesc(P))):- current_prolog_flag(logicmoo_modality,full), !.
   66
   67% late modality
   68qualify_nesc(P,nesc(P)):- current_prolog_flag(logicmoo_modality,late), !.
   69
   70
   71% part modality
   72qualify_nesc( ~(IN), ~(poss(IN))):- current_prolog_flag(logicmoo_modality,part), !.
   73%qualify_nesc(P<=>Q,((nesc(P)<=>nesc(Q)) & (poss(P)<=>poss(Q)))):-!.
   74qualify_nesc(P=>Q,((poss(Q)&nesc(P))=>nesc(Q))):-  current_prolog_flag(logicmoo_modality,part), !.
   75%qualify_nesc(P=>Q,((nesc(P)=>nesc(Q)) & (poss(P)=>poss(Q)))):-!.
   76%qualify_nesc(P,(~nesc(P)=>nesc(P))):- \+ \+ (P = (_ & _) ; P = (_ v _)).
   77qualify_nesc(P,nesc(P)):- \+ current_prolog_flag(logicmoo_modality,full), !.
   78
   79% fallback
   80qualify_nesc(P,nesc(P)):- !.
   81
   82% never seen (but realistic)
   83qualify_nesc(P=>Q,(PP => (NP & QP =>NQ))):-!, weaken_to_poss(P,PP),weaken_to_poss(Q,QP),add_nesc(P,NP),add_nesc(Q,NQ).
   84qualify_nesc((P & Q),(PossPQ => (P & Q))):-  weaken_to_poss(P & Q, PossPQ),!.
   85
   86/*
   87qualify_nesc(IN,poss(IN)):- IN=..[F|_],should_be_poss(F),!.
   88qualify_nesc(Wff,(poss(Wff) => nesc(Wff))):- quietly(var_or_atomic(Var)),!.
   89qualify_nesc(Wff,(poss(Wff) => nesc(Wff))):- leave_as_is_logically(Wff),!.
   90qualify_nesc(Q,(PQ & Q)):-  weaken_to_poss(Q,PQ),!.
   91qualify_nesc(OuterQuantKIF,OuterQuantKIF):-!.
   92% qualify_nesc(IN,OUT):-IN=..[F|INL],logical_functor_pttp(F),!,must_maplist_det(qualify_nesc,INL,OUTL),OUT=..[F|OUTL].
   93*/

add_nesc(?X, ?X) is det: Add Necesity.

  101add_nesc(IN,OUT):-is_list(IN),must_maplist_det(add_nesc,IN,OUT),!.
  102add_nesc(OuterQuantKIF,OuterQuantKIF):- is_ftVar(OuterQuantKIF),!.
  103add_nesc(OuterQuantKIF,OuterQuantKIF):-leave_as_is(OuterQuantKIF),!.
  104add_nesc(OuterQuantKIF,OuterQuantKIF):-contains_modal(OuterQuantKIF),!.
  105add_nesc( ~(IN), nesc(~(IN))).
  106add_nesc(IN,OUT):-IN=..[F|INL],logical_functor_pttp(F),!,must_maplist_det(add_nesc,INL,OUTL),OUT=..[F|OUTL].
  107add_nesc(IN,nesc(IN)).
  108/*
  109add_nesc(nesc(OuterQuantKIF),nesc(OuterQuantKIF)):-!.
  110add_nesc(poss(OuterQuantKIF),poss(OuterQuantKIF)):-!.
  111add_nesc(P<=>Q,O):-!,add_nesc(((P=>Q) & (Q=>P)),O).
  112add_nesc(PQ,PQO):- PQ=..[F|Q],is_quantifier(F),append(LQ,[RQ],Q),add_nesc(RQ,RQQ),append(LQ,[RQQ],QQ),PQO=..[F|QQ],!.
  113add_nesc(IN,poss(IN)):-IN=..[F|_],should_be_poss(F),!.
  114add_nesc(P=>Q,((PP & P & QP) =>Q)):-  weaken_to_poss(P,PP),weaken_to_poss(Q,QP).
  115
  116add_nesc(Q,(PQ & Q)):-  weaken_to_poss(Q,PQ),!.
  117add_nesc((P & Q),(PQ & (P & Q))):-  weaken_to_poss(P & Q,PQ),!.
  118add_nesc(OuterQuantKIF,OuterQuantKIF):-!.
  119*/

add_poss_to(?PreCond, ?Wff6667, ?Wff6667) is det: Add Possibility Converted To.

  127add_poss_to([],Wff6667, Wff6667).
  128add_poss_to([PreCond|S],Wff6667, PreCondPOS):-!,
  129 add_poss_to(PreCond,Wff6667, PreCondM),
  130 add_poss_to(S,PreCondM, PreCondPOS).
  131
  132add_poss_to(PreCond,Wff6667, PreCond=>Wff6667):-prequent(PreCond).
  133add_poss_to(PreCond,Wff6667, Wff6667):-leave_as_is_logically(PreCond).
  134add_poss_to( ~(_PreCond),Wff6667, Wff6667).
  135add_poss_to(PreCond,Wff6667, (poss(PreCond)=>Wff6667)).
  136
  137
  138% weaken_to_poss(OuterQuantKIF,OuterQuantKIF):-!.
  139% weaken_to_poss(X,X):-!.

weaken_to_poss(?PQ, ?PQ) is det: Weaken statments from meaning Nesc to meaning Possibility.

  147weaken_to_poss(PQ,poss(PQ)):- var(PQ),!.
  148weaken_to_poss(poss(PQ),poss(PQ)):-!.
  149weaken_to_poss(nesc(PQ),poss(PQ)):-!.
  150weaken_to_poss(INL,OUTC):-is_list(INL),must_maplist_det(weaken_to_poss,INL,OUTL),
  151  F='&',OUT=..[F|OUTL],correct_arities(F,OUT,OUTC).
  152%weaken_to_poss(PQ,PQO):- PQ=..[F,V,Q],is_quantifier(F),weaken_to_poss(Q,QQ),PQO=..[F,V,QQ],!.
  153weaken_to_poss(OuterQuantKIF,poss(OuterQuantKIF)):- leave_as_is_logically(OuterQuantKIF),!.
  154weaken_to_poss( ~(IN), poss(~(IN))):-!.
  155weaken_to_poss(IN,OUT):-IN=..[F|INL],logical_functor_pttp(F),!,must_maplist_det(weaken_to_poss,INL,OUTL),OUT=..[F|OUTL].
  156weaken_to_poss(IN,poss(IN)).
  157
  158
  159% shall X => can X
  160% shall ~ X => ~ can X
  161% ~ shall X => can ~ X
  162
  163
  164
  165
  166
  167
  168
  169
  170
  171
  172
  173identical_refl(X,Y):- =<>=(X,Y),!.
  174
  175
  176
  177
  178
  179undess_head(H,H):- current_prolog_flag(logicmoo_propagation, modal),!.
  180
  181undess_head((H:-B),(HH:-B)):-!,undess_head(H,HH).
  182undess_head(proven_nesc(H),H):- !.
  183undess_head(H,H).
  184
  185
  186demodal_clauses(_KB,Var, Var):- \+compound(Var),!.
  187demodal_clauses(KB,(Head:-Body),HeadOBodyO):- !, demodal_head_body(KB,Head,Body,HeadOBodyO),!.
  188demodal_clauses(KB,List, ListO):- is_list(List), !,
  189 must_maplist_det(demodal_clauses(KB),List,ListM),!,
  190 kif_optionally_e(true,remove_unused_clauses,ListM,ListOM), 
  191 kif_optionally_e(true,dedupe_clauses,ListOM,ListO).
  192demodal_clauses(KB,Head,HeadOBodyO):- demodal_head_body(KB,Head,true,HeadOBodyO),!.
  193
  194
  195/*
  196demodal_head_body(KB,Head,Body,(Head:-BodyO)):- fail,
  197  term_attvars(Head,AttVars),
  198  AttVars \==  [],!,
  199  include(AttVars,is_skolem,HeadAttVars),
  200  term_attvars(Body,BodyAttVars),
  201  subtract_eq(HeadAttVars,BodyAttVars,SKList),
  202    transform_skolem_forms(SKList,HeadExtra),
  203    conjoin(HeadExtra,Body,BodyM),
  204    demodal_body(KB,Head,BodyM,BodyO),!.
  205*/
  206
  207
  208demodal_head_body(KB,Head,Body,HeadBodyO):-
  209   demodal_head(KB,Head,HeadM,Body,HeadExtra),
  210   (HeadM \== Head ; HeadExtra \== true),!, conjoin(HeadExtra,Body,BodyM),
  211   demodal_head_body1(KB,HeadM,BodyM,HeadBodyO),!.
  212
  213demodal_head_body(KB,Head,Body,OUT):- demodal_head_body1(KB,Head,Body,OUT).
  214
  215proven_negated_lit(_,_):-!,fail.
  216proven_negated_lit(C,proven_neg(Head)):- same_compound(C,proven_tru(Head)).
  217proven_negated_lit(C,proven_tru(Head)):- same_compound(C,proven_neg(Head)).
  218
  219demodal_head_body1(_KB,'$unused'(Head),Body,('$unused'(Head):-Body)):-!.
  220demodal_head_body1(_KB,Head,Body,('$unused'(Head):-Body)):- Body = fail_cause(_,_),!.
  221
  222demodal_head_body1(KB, (NEG_Head), 
  223        (   falsify(SKOLEM3)),Out):- same_compound(SKOLEM3,skolem(_,_)),proven_negated_lit(NEG_Head,POS_Head),
  224      demodal_head_body(KB, (POS_Head),
  225              (   (SKOLEM3)),Out).
  226
  227demodal_head_body1(KB, (NEG_Head), 
  228        (   falsify(SKOLEM3), B),Out):- same_compound(SKOLEM3,skolem(_,_)),proven_negated_lit(NEG_Head,POS_Head),
  229      demodal_head_body(KB, (POS_Head),
  230              (   (SKOLEM3) , B),Out).
  231
  232demodal_head_body1(KB, (NEG_Head), 
  233        (A,   falsify(SKOLEM3)),Out):- same_compound(SKOLEM3,skolem(_,_)),proven_negated_lit(NEG_Head,POS_Head),
  234      demodal_head_body(KB, (POS_Head),
  235              (A,   (SKOLEM3)),Out).
  236
  237demodal_head_body1(KB, (NEG_Head), 
  238        (A,   falsify(SKOLEM3), B),Out):- same_compound(SKOLEM3,skolem(_,_)),proven_negated_lit(NEG_Head,POS_Head),
  239      demodal_head_body(KB, (POS_Head),
  240              (A,   (SKOLEM3) , B),Out).
  241
  242
  243demodal_head_body1(_KB,Head,Body,('$unused'(Head):-fail_cause(unusable_body,Body))):- 
  244 unusable_body(Head,Body),!.
  245demodal_head_body1(KB,Head,Body,OUT):-
  246   demodal_body(KB,Head,Body,Body1),
  247   demodal_body(KB,Head,Body1,BodyM),
  248   (Body=@=BodyM -> OUT= (Head :- Body) ; 
  249     demodal_head_body1(KB,Head,BodyM,OUT)),!.
  250
  251
  252unusable_body(_,Var):- \+ compound(Var),!,fail.
  253unusable_body(_,fail_cause(_,_)).
  254unusable_body(_,fail_cause(_)).
  255unusable_body(_,(proven_not_reify(XX),_)):- !,nonvar(XX).
  256unusable_body(_,(A,B,_)):- negations_of_each_other(A,B).
  257unusable_body(Head,(A,B)):- !,(unusable_body(Head,A);unusable_body(Head,B)).
  258unusable_body(Head,(A;B)):- !,(unusable_body(Head,A);unusable_body(Head,B)).
  259unusable_body(_,\+ needs(_)).
  260unusable_body(_,fail).
  261unusable_body(_,falsify(skolem(_,_))).
  262
  263% unusable_body(_,proven_neg(needs(_))).
  264
  265negations_of_each_other(A,B):- A  =<>=  ~B.
  266negations_of_each_other(A,B):- ~A  =<>=  B.
  267
  268
  269guess_varnames(IO):-guess_varnames(IO,_).
  270guess_varnames(I,O):-guess_varnames(add_var_to_env,I,O).
  271
  272:- meta_predicate guess_varnames(2,*,*).  273guess_varnames(_Each,G,G):- \+ compound(G),!.
  274guess_varnames(Each, subrelation(V,N), subrelation(V,N)):- var(V), \+ variable_name(V,_), atomic(N),call(Each,N,V),!.
  275guess_varnames(Each, isNamed(V,N), isNamed(V,N)):- var(V), \+ variable_name(V,_), atomic(N),call(Each,N,V),!.
  276guess_varnames(Each, isNamed(V,H), isNamed(V,H)):- var(V), \+ variable_name(V,_),
  277   compound(H),functor(H,F,_),
  278   flag(skolem_count,SKN,SKN+1),
  279   toCamelcase(F,UF),atom_concat(UF,SKN,UF1),
  280   call(Each,UF1,V),!.
  281guess_varnames(Each,H,H ):- H=..[F,V],var(V),
  282  \+ variable_name(V,_), 
  283  \+ atom_concat('sk',_,F), 
  284  \+ atom_concat(_,'Of',F), 
  285  \+ atom_concat(_,'Fn',F),
  286  flag(skolem_count,SKN,SKN+1),
  287  toCamelcase(F,UF),atom_concat(UF,SKN,UF1),
  288  call(Each,UF1,V),!.
  289guess_varnames(Each,H,HH ):- H=..[F|ARGS],!,must_maplist_det(guess_varnames(Each),ARGS,ARGSO),!,HH=..[F|ARGSO].
  290guess_varnames(_Each, (G), (G)):- !.
  291
  292/*
  293LEM asserts (A v ~A) is nesisarily true.. But what if we rejected this? 
  294We still need to prove things.. like "prove A" or even "prove ~A" thus we are better of with:  <>(A v ~A)
  295
  296"not possibly all x" can be negated to "nesc all x" without the need to invert to existential quantification
  297
  298all x: ~P(x)
  299
  300all x: ~P(x)  =<>= = all x: ~<>P(x)  
  301
  302which can be negated to    all x: <>P(x)  without switching to existental quantification
  303
  304negates to  <> all P()
  305
  306
  307
  308meaning a new rule can make something that was once not possible to prove, become provable
  309<>~P or <>P can become either []P or []~P later (but afterwards will not change)
  310this doesnt nesc imply defeasably, but implies elaboration tollerance
  311
  312
  313
  314
  315
  316
  317(A v ~A) in order to deal with   ?(A v ~A)   ?A ? ~<>A
  318[]A v ~<>A
  319*/
  320body_contains(B,Cont):- notrace((compound(Cont),compound(SK),sub_term(SK,B),compound(SK),SK=Cont)),!.
  321
  322
  323% demodal_head(_KB,proven_not_reify(A),'$unused'(proven_not_reify(A)),_Body,true):- nonvar(A),!.
  324% demodal_head(_KB,proven_neg(needs(Head)),'$unused'(proven_neg(needs(Head))),_Body,true):- !.
  325
  326demodal_head(_KB,proven_nesc(skolem(X,Y)),make_existential(X,Y),_Body,true).
  327demodal_head(_KB,proven_tru(nesc(~FALSE)),proven_neg(FALSE),_Body,true):- nonvar(FALSE).
  328demodal_head(_KB,proven_neg(DIFF),proven_helper(equals(X,Y)),_Body,true):- same_compound(DIFF,different(X, Y)), !.
  329demodal_head(_KB,proven_neg(DIFF),proven_helper(dif_objs(X,Y)),_Body,true):- same_compound(DIFF,equals(X, Y)), !.
  330
  331demodal_head(_KB,proven_neg(skolem(X,Y)),('$unused'(make_existential(was_create_min,X,Y))),_Body,true):- functor(Y,skF,_).
  332demodal_head(_KB,proven_neg(skolem(X,if_all_different(A,B,C))),(make_existential(X,skF(A,B,X,C))),_Body,true).
  333demodal_head(_KB,proven_tru(H),deduce_tru(H),Body,true):- body_contains(Body,skolem(_,_)).
  334demodal_head(_KB,proven_neg(H),deduce_neg(H),Body,true):- body_contains(Body,skolem(_,_)).
  335demodal_head(KB,proven_nesc(H),proven_tru(HH),_Body,Out):-  demodal_any(KB,H,HH,Out),!.
  336demodal_head(KB,proven_nesc(H),proven_nesc(HH),_Body,Out):-  demodal_any(KB,H,HH,Out),!.
  337demodal_head(KB,proven_neg(H),proven_neg(HH),_Body,Out):-  demodal_any(KB,H,HH,Out),!.
  338
  339demodal_head(KB,Head,HeadM,_Body,HeadExtra):- demodal_any(KB,Head,HeadM,HeadExtra).
  340
  341
  342sharing_vars_vars(A,B):- term_variables(A,AV),term_variables(B,BV),member(VB,BV),member(VA,AV),VB =<>= VA.
  343same_compound(COMP,SAME):- compound(COMP),compound(SAME),COMP=@=SAME.
  344
  345
  346% demodal_any(_KB,different(A,B),not_equals(A,B),true):-!.
  347
  348demodal_any(_KB,P,P,true):- \+ compound(P),!.
  349demodal_any(_KB,P,P,true):- P=..[_,A],\+ compound(A),!.
  350
  351demodal_any(_KB,proven_not_nesc(different(A,B)),proven_nesc(equals(A,B)),true):-!.
  352demodal_any(_KB,proven_not_nesc(equals(A,B)),proven_nesc(different(A,B)),true):-!.
  353demodal_any(_KB,proven_not_nesc(mudEquals(A,B)), proven_nesc(different(A,B)),true):-!.
  354demodal_any(_KB, not_nesc(b_d(_7B2, nesc, poss), A v ~B), (~A & B),true) :-!.
  355demodal_any(_KB,proven_not_nesc(isa(A,B)),not_isa(A,B),true):- nonvar(B),!.
  356demodal_any(_KB,naf(proven_not_nesc(Head)),poss(Head),true):- !.
  357demodal_any(KB,nesc(_,Head),NHead,Out):- !,demodal_any(KB,nesc(Head),NHead,Out).
  358demodal_any(KB,poss(_,Head),NHead,Out):- !,demodal_any(KB,poss(Head),NHead,Out).
  359
  360demodal_any(KB,falsify(nesc(~P)),poss(PP),Out):-!,demodal_any(KB,P,PP,Out).
  361demodal_any(KB,nesc(G),PP,Out):- same_compound(G,nesc(P)),!,demodal_any(KB,nesc(P),PP,Out).
  362demodal_any(KB,poss(G),PP,Out):- same_compound(G,poss(P)),!,demodal_any(KB,poss(P),PP,Out).
  363demodal_any(KB,H,HH,Out):- H=..[F,A],demodal_any(KB,A,AA,Out),HH=..[F,AA].
  364demodal_any(_KB,Head,Head,true):- !.
  365% demodal_any(KB,Head,HeadO,true):-  demodal_clauses(KB,Head,HeadO).
  366
  367
  368is_xformed_body(ensure_cond).
  369is_xformed_body(never_cond).
  370is_xformed_body(skolem).
  371
  372demodal_body(_KB,_Head,Var, Var):- \+compound(Var),!.  
  373demodal_body(_KB,_Head, skolem(X,if_all_different(N,SkF,DFml)), not_in(X,skF(N,SkF,X,DFml))):-!.
  374demodal_body(_KB,_Head,Var, Var):- functor(Var,F,_),is_xformed_body(F),!.
  375
  376demodal_body(KB, Head, Body,BodyO):- demodal_any(KB,Body,BodyM,Conj), (BodyM \== Body;Conj \== true),  
  377  conjoin(Conj,BodyM,BodyMM),!,
  378  demodal_body(KB, Head, BodyMM,BodyO).
  379
  380% DISABLER demodal_body(_KB,_Head,Var, Var):-!.
  381
  382% demodal_body(KB, Head, Body, _):- dmsg(demodal_body(KB, Head, Body)),fail.
  383
  384demodal_body(KB, Head, (Var, Rest), NEW):- var(Var),!,demodal_body(KB, Head,  Rest, NewRest),conjoin(NewRest,Var,NEW).
  385demodal_body(_KB,_Head, poss(b_d(_7B2, nesc, poss),G), poss(G)).
  386demodal_body(_KB,_Head, nesc(b_d(_7B2, nesc, poss),G), nesc(G)).
  387
  388demodal_body(_KB, _Head, (A ; B) , ensure_cond(G,either(CA,CB))):- same_compound(A,ensure_cond(G,CA)),same_compound(B,ensure_cond(G1,CB)),G==G1,!.
  389
  390demodal_body(_KB, _Head, ((A , B) ; C) , ({ignore(A)}, C) ):- identical_refl(B,C),!.
  391demodal_body(_KB, _Head, (C ; (A , B) ) , ({ignore(A)}, C) ):- identical_refl(B,C),!.
  392
  393demodal_body(_KB, (Head), ensure_cond(_G, different(X, Y)),dif_objs(X,Y)):- compound(Head),member(XorY,[X,Y]),\+ contains_var(XorY,Head).
  394demodal_body(_KB, (_Head), ensure_cond(_G, different(X, Y)),dif_objs(X,Y)):- !.
  395
  396
  397
  398demodal_body(_KB, _Head,(dif_objs(X, Y),nesc(PRED)),(nesc(PRED)*->dif_objs(X, Y))):- compound(PRED),member(XorY,[X,Y]),contains_var(XorY,PRED).
  399
  400demodal_body(_KB, _Head, (A ; C), A ):- identical_refl(A,C),!.
  401
  402
  403demodal_body(_KB, _Head, (A , C), A ):- identical_refl(A,C),!.
  404demodal_body(_KB, _Head, neg(nesc(~(P))), nesc(poss(P)) ):-!.
  405demodal_body(_KB, proven_neg(_Head),(Body),fail_cause(naf_sk,Body)):-
  406  Body = (falsify(skolem(_X,Y,_Z)),falsify(CALL)),
  407  compound(CALL),compound(Y),!.
  408
  409demodal_body(_KB,  (_Head), 
  410        (   falsify(skolem(X, Y)),
  411            nesc(PRED1)
  412        ;   skolem(X, Y),
  413            falsify(PRED2)
  414        ),falsify(PRED2)):- PRED2 == PRED1,!.
  415
  416demodal_body(_KB,  (_Head), 
  417        (   falsify(skolem(X, Y)),
  418            _
  419        ;   skolem(X, Y),
  420            PRED2
  421        ),PRED2):- !.
  422
  423  
  424demodal_body(KB, Head, ((A0 , A1) ; (B0 , B1)), OUT):- A0 =<>= B0,!, demodal_body(KB, Head, (A1 ; B1), MID),
  425   demodal_body(KB, Head, (A0 , MID), OUT).
  426
  427demodal_body(KB, Head, ((A0 , A1) ; (B0 , B1)), OUT):- A1 =<>= B1,!, demodal_body(KB, Head, (A0 ; B0), MID),
  428   demodal_body(KB, Head, (MID , B1), OUT).
  429  
  430
  431demodal_body(KB, Head, (A ; B), OUT):- fail, demodal_body(KB, Head, A, AA),demodal_body(KB, Head, B, BB),
  432   (A ; B)  \==  (AA ; BB),!, demodal_body(KB, Head, (AA ; BB), OUT).
  433  
  434
  435demodal_body(_KB, _Head, ((A , B) , C), (A , B , C)):- nonvar(A),!.
  436demodal_body(_KB, _Head, (A , B , C), (A , B)):- identical_refl(A,C),!.
  437demodal_body(_KB, _Head, (A , B , C), (A , C)):- identical_refl(A,B),!.
  438demodal_body(_KB, _Head, (A , B , C), (A , C)):- identical_refl(C,B),!.
  439
  440
  441demodal_body(_KB,_Head, poss(poss( G)), poss(G)):- nonvar(G),!.
  442
  443demodal_body(KB,  Head, proven_not_neg(skolem(X,Y)), OUT):- !, demodal_body(KB,  Head, (skolem(X,Y)), OUT).
  444
  445demodal_body(_KB,  (make_existential(X,_)), proven_not_neg(G), ensure_cond(X,G)):- !.
  446demodal_body(_KB,  (make_existential(X,_)), proven_not_nesc(G), never_cond(X,G)):- !.
  447
  448demodal_body(KB,make_existential(X,SK), ((never_cond(XX, P); Q )), (ensure_cond(XX,P),QQ)):- 
  449    demodal_body(KB,make_existential(X,SK), Q,QQ),!.
  450
  451/*     
  452demodal_body(KB,  (make_existential(X,_)), proven_not_neg(G), ensure_cond(X,G)):- term_variables(G,Vars),memberchk(V,Vars),X =<>= V.
  453demodal_body(KB,  (make_existential(X,_)), proven_not_nesc(G), never_cond(X,G)):- term_variables(G,Vars),memberchk(V,Vars),X =<>= V.
  454demodal_body(KB,  (make_existential(X,_)), proven_not_neg(G), require_xconds(G)):-  contains_var(X,G).
  455% demodal_body(KB,  (make_existential(X,_)), proven_not_nesc(G), never_xconds(Vars,G)):- term_variables(G,Vars),contains_var(X,G).
  456demodal_body(KB,  (make_existential(_,SK)), proven_not_neg(G), expect_tru(G)):- sharing_vars_vars(SK,G).
  457demodal_body(KB,  (make_existential(_,SK)), proven_not_nesc(G), expect_fals(G)):- sharing_vars_vars(SK,G).
  458*/
  459
  460demodal_body(_KB,_Head,nesc(different(X,Y)),dif_objs(X,Y)):- !.
  461demodal_body(_KB,_Head,neg(different(X,Y)),sameObjects(X,Y)):- !.
  462demodal_body(_KB,_Head,nesc(different(X,Y)),dif_objs(XX,YY)):- (X @> Y -> XX/YY=X/Y ; XX/YY=Y/X).
  463demodal_body(_KB,_Head,neg(different(X,Y)),sameObjects(XX,YY)):- (X @> Y -> XX/YY=X/Y ; XX/YY=Y/X).
  464
  465
  466
  467demodal_body(_KB,_Head,(H,T),(T,H)) :-  \+ poss_or_skolem(H),poss_or_skolem(T).
  468
  469demodal_body(KB,Head,(A;B),BodyOut):- disjuncts_to_list((A;B),List),list_to_set(List,SET),List \== SET,!,must_maplist_det(demodal_body(KB,Head),SET,SET2),list_to_conjuncts((;),SET2,BodyOut).
  470demodal_body(KB,Head,(A,B),BodyOut):- conjuncts_to_list_det((A,B),List),list_to_set(List,SET),List \== SET,!,must_maplist_det(demodal_body(KB,Head),SET,SET2),list_to_conjuncts(SET2,BodyOut).
  471
  472demodal_body(KB,Head,[H|T],[HH|TT]):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  473demodal_body(KB,Head,(H;T),(HH;TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  474
  475
  476% demodal_body(_KB,  _Head, proven_neg(skolem(_,_)), fail_cause(naf_sk,proven_neg(skolem(_,_)))):-!.
  477% demodal_body(_KB,  _Head, proven_not_nesc(skolem(_,_)), fail_cause(naf_neg_sk,proven_not_nesc(skolem(_,_)))):-!.
  478% demodal_body(_KB,  never_any(_) , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,never_any(skolem(_,_))).
  479
  480demodal_body(_KB,  _ , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,never_any(skolem(_,_))).
  481demodal_body(_KB,  _ , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,never_cond(_,skolem(_,_))).
  482demodal_body(_KB,  _ , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,neg(skolem(_,_))).
  483demodal_body(_KB,  _ , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,never_deduce(skolem(_,_))).
  484% demodal_body(_KB,  _ , Body ,  fail_cause(naf_sk,Body)) :- body_contains(Body,falsify(skolem(_,_))).
  485
  486demodal_body(_KB,  _, neg(nesc(~P)),poss(P)):-!.
  487
  488demodal_body(_KB,  pro_tru(_Head), proven_not_neg(X), nesc(X)):-!.
  489demodal_body(_KB,  pro_tru(_Head), proven_not_nesc(X), neg(X)):-!.
  490
  491demodal_body(_KB,  con_neg(_Head), proven_not_neg(X), nesc(X)):-!.
  492demodal_body(_KB,  con_neg(_Head), proven_not_nesc(X), neg(X)):-!.
  493
  494
  495demodal_body(_KB,   (_Head), proven_not_neg(X), nesc(X)):-!.
  496demodal_body(_KB,   (_Head), proven_not_nesc(X), falsify(X)):-!.
  497
  498demodal_body(KB,Head,(H,T),(HH,TT)):- T\=(_,_),!, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  499demodal_body(KB,Head,(H,T),(HH,TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  500
  501
  502demodal_body(KB,Head,H,HH ):- H=..[F|ARGS],!,must_maplist_det(demodal_body(KB,Head),ARGS,ARGSO),!,HH=..[F|ARGSO].
  503demodal_body(_KB,_Head, (G), (G)):- !.
  504
  505
  506:- if(false).  507demodal_body(_KB, _Head, ((A , B) ; (C , D)), (A , (B ; D))):- identical_refl(A,C),!.
  508demodal_body(_KB, _Head, proven_nesc(X),  X).
  509demodal_body(_KB, _Head, proven_neg(X), ~ X).
  510% demodal_body(_KB, _Head, proven_not_nesc(X), \+ X).
  511demodal_body(_KB, proven_neg(_Head), \+ ~ CMP, true):- compound(CMP),CMP=(skolem(_,_)).
  512% demodal_body(_KB, _Head, ((A ; B), C), (C, once(B ; A))).
  513% demodal_body(_KB, _Head, (C, (A ; B)), ((B ; A), C)).
  514demodal_body(_KB, proven_neg(Head), (Other,(\+ BHead ; ~Other1)),naf(BHead)):- BHead  =<>=  Head,Other=Other1.
  515demodal_body(_KB, proven_neg(Head), (Other,( ~Other1 ; \+ BHead )),naf(BHead)):- BHead  =<>=  Head,Other=Other1.
  516demodal_body(_KB, _Head, (A, proven_isa(I, C)), (proven_isa(I, C), A)):- A \= proven_isa(_, _).
  517% demodal_clauses(KB,G,O):- G=..[F,H], \+ leave_as_is(H), H=..[HF,HH], atom_compat(F,HF,HHF),!, GG=..[HHF,HH], demodal_clauses(KB,GG,O).
  518demodal_body(_KB,_Head,naf(~(CMP)),CMP):- poss_or_skolem(CMP).
  519demodal_body(_KB,Head, v(A, ~(B)), ~(B)):- A =<>= Head,!.
  520demodal_body(_KB,Head, v(~(B), A), ~(B)):- A =<>= Head,!.
  521demodal_body(_KB,Head, v(A, B), B):- A =<>= Head,!.
  522demodal_body(_KB,Head, v(B, A), B):- A =<>= Head,!.
  523demodal_body(_KB, _Head, poss(A & B), (poss(A) , poss(B))):-nonvar(A),!.
  524%demodal_body(_KB, ~(_Head),(G1,G2), (G1 , \+ GG2)):- G2 \= (_,_), G2  =<>=  ~(GG2).
  525%demodal_body(_KB,_Head,(G1,G2), (G1, poss(GG2) )):- G2 \= (_,_), G2  =<>=  ~(GG2), nonvar(GG2).
  526demodal_body(KB,Head,(H & T),(HH,TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  527demodal_body(KB,Head,(H,T),(HH,TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  528demodal_body(KB,Head,(H v T),(HH v TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  529% demodal_body(_KB, _Head, G, G):- !.
  530demodal_body(_KB, Head, G, true):- G =<>= Head, unusual_body,!.
  531% demodal_body(_KB,_Head, poss(isa(I,C)), isa(I,C)):- !.
  532demodal_body(_KB,_Head, naf(~(G)), poss(G)):- nonvar(G),!.
  533demodal_body(_KB,_Head, ~(~(G)), (G)):- nonvar(G), unusual_body,!.
  534demodal_body(_KB, _Head, not_nesc(b_d(_KB2, nesc, poss), A v ~B), (~A , B)) :-!.
  535demodal_body(KB,Head, v(~(A), B), BB):- demodal_body(KB,Head,A,AA),AA =<>= Head,!,demodal_body(KB,Head,B,BB).
  536%demodal_body(KB,Head, v(~(B), A), BB):- demodal_body(KB,Head,A,AA),AA =<>= Head,!,demodal_body(KB,Head,B,BB).
  537demodal_body(KB,Head, v(~(A), B), (AA *-> BB)):- nonvar(A),!,demodal_body(KB,Head,A,AA),demodal_body(KB,Head,B,BB).
  538%demodal_body(_KB,_Head, \+ (~(G)), proven(G)):- nonvar(G),!.
  539demodal_body(_KB,_Head, \+ (~(G)), poss(G)):- nonvar(G),!.
  540demodal_body(_KB, _Head, ( H, poss(G) ) , poss(G)):- H =<>= G , unusual_body.
  541demodal_body(_KB, _Head, ( H, (G) ) , (G)):- H =<>= G, unusual_body.
  542demodal_body(_KB, _Head, ( H, G ) , G):- H =<>= true, unusual_body.
  543demodal_body(_KB, _Head, ( G, H ) , G):- H =<>= true, unusual_body.
  544demodal_body(_KB, _Head, ( G *-> H ) , G):- H =<>= true, unusual_body.
  545demodal_body(_KB, _Head, ( H *-> G ) , G):- H =<>= true, unusual_body.
  546%demodal_body(_KB, Head, ( H, poss(G) ) , (H, G)):- pos_or_isa(H), pred_of(Head,GHead)-> G \= GHead,!.
  547%demodal_body(_KB, Head, ( poss(G) , H) , (G, H)):-  pos_or_isa(H), pred_of(Head,GHead)-> G \= GHead,!.
  548%demodal_body(_KB, Head, ( poss(G) ) , (G)):-  shared_vars(Head,G,SVG),SVG == [].
  549%demodal_body(_KB, Head, ( poss(G) ) , (G)):- Head \= ~(_),!.
  550demodal_body(_KB,_Head, poss(poss( G)), poss(G)):- nonvar(G),!.
  551demodal_body(KB,Head,[H|T],[HH|TT]):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  552demodal_body(KB,Head,(H;T),(HH;TT)):- !, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  553demodal_body(KB,Head,(H,T),(HH,TT)):- current_prolog_flag(logicmoo_propagation, modal),
  554   T\=(_,_),!, must(( demodal_body(KB,Head,H,HH),demodal_body(KB,Head,T,TT))),!.
  555% demodal_body(_KB,_Head, (G), (G)):- current_prolog_flag(logicmoo_propagation, modal),!.
  556demodal_body(KB,Head,H,HH ):- H=..[F|ARGS],!,must_maplist_det(demodal_body(KB,Head),ARGS,ARGSO),!,HH=..[F|ARGSO].
  557:- endif.  558
  559
  560
  561
  562
  563
  564:- fixup_exports.