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