1% File: /opt/PrologMUD/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_compiler.pl
    2%:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).
    3:- module(common_logic_compiler,         
    4          [ 
    5      nnf/3, 
    6           pfn4/3, cf/5,
    7          % op(300,fx,'-'),
    8          /*op(1150,xfx,'=>'),
    9          op(1150,xfx,'<=>'),
   10          op(350,xfx,'xor'),
   11          op(400,yfx,'&'),  
   12          op(500,yfx,'v'),*/
   13            atom_compat/3,
   14            axiom_lhs_to_rhs/3,
   15            b_d_p/2,
   16            boxRule/3,
   17            cf_to_flattened_clauses/4,
   18            cf_to_flattened_clauses_0/4,
   19            cirRule/3,
   20            clausify/4,
   21            clean_repeats_d/2,
   22            cnf/3,
   23            cnf1/3,
   24            correct_boxlog/4,
   25            correct_boxlog_0/4,
   26            correct_cls/3,
   27            correct_cls0/3,
   28            corrected_modal/3,
   29            corrected_modal0/3,
   30            corrected_modal_recurse/3,
   31            corrected_modal_recurse0/3,
   32            ct_op/1,
   33            delete_sublits/3,
   34            to_modal1/3,
   35            is_skolem_setting/1,
   36            demodal_sents/3,
   37            diaRule/3,
   38            dnf/3,
   39            dnf1/3,
   40            expand_cl/3,
   41            flattenConjs/3,
   42            flatten_clauses/2,
   43            get_quantifier_isa/3,
   44            inclause/6,
   45            incorrect_cl/2,
   46            invert_modal/3,
   47            is_lit_atom/1,
   48            is_sent_op_modality/1,
   49            logical_neg/3,
   50            logical_pos/3,
   51            logically_matches/3,
   52            make_1_cl/4,
   53            make_clause_from_set/3,
   54            make_clause_set/3,
   55            make_clauses/3,
   56            make_each/3,
   57            
   58            modal2sent/2,
   59            mpred_quf/2,
   60            mpred_quf_0/2,
   61            neg_op/1,
   62            negate/3,
   63            negate0/3,
   64            negate_one/3,
   65            negate_one_maybe/3,
   66       nnf/3,
   67       nnf/5,
   68       
   69       
   70            nonegate/3,
   71            nonvar_unify/2,
   72            notin/2,
   73            nowrap_one/3,
   74            pfn4/3,
   75            pfn4/4,
   76            putin/3,
   77            removeQ/3,
   78            removeQ/4,
   79            removeQ_LC/4,
   80            removes_literal/2,
   81            
   82            share_scopes/2,
   83            simplify_atom/2,
   84            simplify_cheap/2,
   85            simplify_cheap_must/2,
   86
   87            % nnf_args/5,
   88       nnf_args/8,
   89            third_order/1,
   90            to_poss/3,
   91            to_regular_cl/4,
   92            unbuiltin_negate/3,
   93            unbuiltin_negate/4,
   94            until_op/1,
   95            variants_are_equal/3
   96          ]).

common_logic_compiler

Provides a prolog database replacement that uses an interpretation of KIF

t/N hybridRule/2

Logicmoo Project PrologMUD: A MUD server written in Prolog Maintainer: Douglas Miles Dec 13, 2035

Compute normal forms for SHOIQ formulae. Skolemize SHOI<Q> formula.

Copyright (C) 1999 Anthony A. Aaby <aabyan@wwc.edu> Copyright (C) 2006-2007 Stasinos Konstantopoulos <stasinos@users.sourceforge.net> 1999-2015 Douglas R. Miles <logicmoo@gmail.com>

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

References

[1] Planning with First-Order Temporally Extended Goals Using Heuristic Search, Baier, J. and McIlraith, S., 2006. Proceedings of the 21st National Conference on Artificial Intelligence (AAAI06), July, Boston, MA

FORMULA SYNTAX

~( A) &(F, F) v(F, F) '=>'(F, F) '<=>'(F, F) all(X,A) exists(X,A) atleast(X,N,A) atmost(X,N,A)

Expressions

A BNF grammar for Expresions is the following:

BEXPR ::= <fluent-term> | ~(FACT) | FACT BEXPR ::= or(BEXPR,BEXPR) | and(BEXPR,BEXPR) | not(BEXPR)

Temporal Boolean Expressions

BNF grammar:

TBE ::= BEXPR | final TBE ::= always(TBE) | eventually(TBE) | until(TBE,TBE) | release(CT,TBE,TBE) | cir(CT,TBE)

*/

  173%=%   mpred_clausify.P
  174%=%      SWI-Prolog version
  175%=%   Convert wffs to list of normal logic clauses
  176%=%
  177%=%   and       &  
  178%=%   or        v
  179%=%   not       ~
  180%=%   xor       xor
  181%=%   implies   =>   
  182%=%   iff       <=>  
  183%=%   all       all(X,0)
  184%=%   some      exists(Y,0)
  185%=%
  186%=%    all(X,p(X) => exists(Y, r(Y) & q(X,Y))) 
  187%=%  ===============
  188%=%    p(X) => r(sk1(X)) & q(X,sk1(X))
  189%=%  ===============
  190%=%    r(sk1(X)):- p(X).
  191%=%    q(X,sk1(X)):- p(X).
  192
  193
  194:- include(library('logicmoo/common_logic/common_header.pi')).  195%:- user:ensure_loaded(library(pfc)).
  196%:- endif.
  197%:- reexport(library('logicmoo/common_logic/common_logic_exists.pl')).
  198
  199% :- use_module(library(dictoo)).
  200:- set_how_virtualize_file(bodies).  201
  202
  203:- include(common_logic_convert).  204
  205% % :- '$set_source_module'(common_logic_compiler).
  206
  207% :- use_module(logicmoo(util/logicmoo_util_preddefs)).
  208:-
  209            op(1150,fx,(was_dynamic)),
  210            op(1150,fx,(was_multifile)),
  211            op(1150,fy,(was_module_transparent)),
  212            op(1150,fx,(was_export)).  213
  214
  215:-ain(baseKB:predicateConventionMt(mud_test,baseKB)).  216
  217% :-reexport(library('logicmoo/common_logic/common_logic_snark')).
  218
  219
  220:- multifile((        
  221        baseKB:feature_test/0,
  222        baseKB:regression_test/0,
  223        baseKB:sanity_test/0)).  224:- dynamic((        
  225        baseKB:feature_test/0,
  226        baseKB:regression_test/0,
  227        baseKB:sanity_test/0)).  228:- multifile((        
  229        baseKB:feature_test/1,
  230        baseKB:regression_test/1,
  231        baseKB:sanity_test/1)).  232:- dynamic((        
  233        baseKB:feature_test/1,
  234        baseKB:regression_test/1,
  235        baseKB:sanity_test/1)).  236
  237% % :- '$set_source_module'(common_logic_compiler).
  238
  239
  240% :- use_module(logicmoo(snark/common_logic_sexpr)).
  241
  242:- dynamic user:file_search_path/2.  243:- multifile user:file_search_path/2.  244:- prolog_load_context(source,File),file_directory_name(File,Dir),directory_file_path(_,Short,Dir),asserta_if_new(user:file_search_path(Short,Dir)).  245
  246
  247:-  system:((
  248 op(1199,fx,('==>')), 
  249 op(1190,xfx,('::::')),
  250 op(1180,xfx,('==>')),
  251 op(1170,xfx,'<==>'),  
  252 op(1160,xfx,('<-')),
  253 op(1150,xfx,'=>'),
  254 op(1140,xfx,'<='),
  255 op(1130,xfx,'<=>'), 
  256 op(600,yfx,'&'), 
  257 op(600,yfx,'v'),
  258 op(350,xfx,'xor'),
  259 op(300,fx,'~'),
  260 op(300,fx,'-'))).  261
  262
  263
  264% :- use_module(logicmoo(pttp/dbase_i_mpred_pttp_testing)). 
  265% :- use_module(logicmoo(pttp/dbase_i_mpred_pttp)). 
  266
  267%  all(R, room(R) => exists(D, (door(D) & has(R,D))))
  268% for any arbitrary R, if R is a room then there exists some object D that is a door, and R has a D.
  269% door(sk6(_G180)):- room(_G180)
  270% has(_G180,sk6(_G180)):- room(_G180)
  271%  R is not a room if D is a door and R doesn't have D
  272% if there are no doors anywhere then there must not be rooms
  273% - room(R):- - has(R,_).
  274
  275
  276% SWI Prolog modules do not export operators by default
  277% so they must be explicitly placed in the user namespace
  278
  279:- %(current_prolog_flag(argv,[pl|_]) -> )
  280     %op(400, fy, baseKB:(nesc) ),	% Necessity, Always
  281     %op(400, fy, baseKB:(poss) ),	% Possibly, Eventually
  282     op(400, fy, baseKB:(cir) ),	% Next time
  283     op(1075,xfx,user:'<-'),
  284  
  285  
  286     %op(400,fy,nesc),		% Necessity, Always
  287     %op(400,fy,poss),		% Possibly, Eventually
  288     op(400,fy,cir),		% Next time
  289
  290     op(300,fx,'-'),
  291     op(300,fx,'~'),
  292     op(1075,xfx,'=>'),
  293     op(1075,xfx,'<-'),
  294     op(1075,xfx,'<=>'),
  295     op(350,xfx,'xor'),
  296     op(400,yfx,'&'),  
  297     op(500,yfx,'v')
  298     ,!.  299
  300
  301
  302:- create_prolog_flag(logicmoo_propagation, modal,[keep(true)]).   % vs "unit"
  303:- create_prolog_flag(logicmoo_modality,late,[keep(true)]).  304
  305:- thread_local(t_l:using_feature/1).  306is_using_feature(Feature):- t_l:using_feature(Feature).
  307
  308%=
 to_poss(KB, ?BDT, ?BDT) is det
Converted To Possibility.
  314to_poss(KB,X,poss(BDT,X)):- is_ftVar(X),share_scopes(KB,BDT),!.
  315to_poss(KB,poss(BDT,X),poss(BDT,X)):-nonvar(BDT),!,share_scopes(KB,BDT),!.
  316to_poss(KB,X,poss(BDT,X)):-share_scopes(KB,BDT),!.
  317
  318% to_nesc(KB,X,nesc(BDT,X)):- is_ftVar(X),share_scopes(KB,BDT),!.
  319to_nesc(KB,X,nesc(BDT,X)):- \+ compound(X), share_scopes(KB,BDT),!.
  320to_nesc(_KB,nesc(BDT,X),nesc(BDT,X)):-!. % nonvar(BDT),!,share_scopes(KB,BDT),!.
  321to_nesc(_KB,nesc(X),nesc(X)):-!. % nonvar(BDT),!,share_scopes(KB,BDT),!.
  322to_nesc(KB,X,nesc(BDT,X)):-share_scopes(KB,BDT),!.
  323
  324
  325:- thread_local(t_l:current_form/1).  326
  327:- style_check(+singleton).
 nnf(+KB, +Fml, ?NNF) is det
Negated Normal Form.
  334nnf(KB,FmlNV,NNF):-
  335  must(quietly(unnumbervars_with_names((KB,FmlNV),(KB0,FmlNV0)))),
  336   must( \+ contains_dvar(KB0:FmlNV0)),
  337   nnf0(KB0,FmlNV0,NNF),!.
  338
  339%=
 nnf0(?KB, ?Fml, ?NNF) is det
Negated Normal Form Primary Helper.
  345nnf0(KB,Fml,NNF):- 
  346 copy_term(Fml,Original),
  347 % ignore(KB='$VAR'('KB')),
  348   locally_tl(current_form(Original),nnf(KB,Fml,[],NNF,_)),!.
  349
  350:- thread_local(t_l:skolem_setting/1).  351
  352%=
 is_skolem_setting(?S) is det
If Is A Skolem Setting.
  359% is_skolem_setting_default(push_skolem).
  360is_skolem_setting_default(in_nnf_implies).
  361is_skolem_setting(S):- t_l:skolem_setting(SS)->S=SS;is_skolem_setting_default(S).
  362%t_l:skolem_setting(push_skolem).
  363%t_l:skolem_setting(attvar).
  364%t_l:skolem_setting(in_nnf).
  365%t_l:skolem_setting(in_nnf_implies).
  366%t_l:skolem_setting(combine(=>)).
  367%t_l:skolem_setting(shared).
  368%t_l:skolem_setting(label).
  369%t_l:skolem_setting(removeQ).
  370%t_l:skolem_setting(eliminate).
  371%t_l:skolem_setting(ignore).
  372
  373
  374%=
 nnf_dnf(?KB, ?Fml, ?DNF) is det
Negated Normal Form Disjunctive Normal Form.
  380nnf_dnf(KB,Fml,DNF):-
  381 locally_tl(skolem_setting(ignore),
  382  (removeQ(KB,Fml,FmlUQ),
  383  nnf(KB,FmlUQ,NNF),
  384   dnf(KB,NNF,DNF))).
  385
  386
  387
  388%=
 get_quantifier_isa(?VALUE1, ?VALUE2, ?VALUE3) is det
get quantifier (isa/2).
  395get_quantifier_isa([X,Col],X,Col):-var(X),nonvar(Col).
 logically_matches(?KB, ?A, ?B) is det
Logically Matches.
  403logically_matches(_KB,_A,_B):-!,fail.
  404logically_matches(KB,A,B):-nonvar(KB),!,logically_matches(_KB,A,B).
  405logically_matches(_,A,B):- (var(A);var(B)),!,A=B.
  406logically_matches(KB,all(_,A),B):-!,logically_matches(KB,A,B).
  407logically_matches(KB,B,all(_,A)):-!,logically_matches(KB,A,B).
  408logically_matches(KB,exists(V,A),exists(V,B)):-!,logically_matches(KB,A,B).
  409logically_matches(KB,[A],B):-!,logically_matches(KB,B,A).
  410logically_matches(KB,A,B):- once(corrected_modal_recurse(KB,A,AM)),A\=@=AM,!,logically_matches(KB,B,AM).
  411logically_matches(_,A,A).
  412
  413
  414is_leave_alone(P):- \+ compound(P),!.
  415is_leave_alone(P):- leave_as_is_logically(P),!.
  416is_leave_alone(P):- functor(P,F,A),is_leave_alone_pfa(P,F,A).
  417
  418is_leave_alone_pfa(_,F,_):- arg(_,v((v),(&),(=>),(<=>),(all),(exists),(~)),F),!,fail.
  419is_leave_alone_pfa(_,assertTemplateReln,_).
  420is_leave_alone_pfa(_,skolem,_).
  421is_leave_alone_pfa(_,different,_).
  422is_leave_alone_pfa(_,mudEquals,2).
  423
  424
  425
  426not_contains_var(X,FmlB):- \+ contains_var(X,FmlB).
  427
  428split_dlog_formula(FmlAB,OP,FmlA,unused):- FmlAB=..[OP,FmlA],move_inward_sent_op(OP),!.
  429split_dlog_formula(FmlAB,OP,FmlA,FmlB):- FmlAB=..[OP,FmlA,FmlB],move_inward_sent_op(OP),!.
  430unsplit_dlog_formula(OP,FmlA,U,FmlAB):- U==unused, FmlAB=..[OP,FmlA].
  431unsplit_dlog_formula(OP,FmlA,FmlB,FmlAB):- FmlAB=..[OP,FmlA,FmlB].
  432
  433move_inward_sent_op(&). move_inward_sent_op(v). move_inward_sent_op(<=>). move_inward_sent_op(=>). move_inward_sent_op(~). 
  434move_inward_sent_op(nesc). move_inward_sent_op(poss).
  435
  436
  437:- discontiguous(nnf1/5).  438:- discontiguous(axiom_lhs_to_rhs/3).  439
  440discovered_var(_Fml,_Slots).
  441discovered_term_slots(_Fml,_Slots).
  442
  443% =================================
  444% ====== drive negation inward ===
  445% =================================
 nnf(KB, +Fml, +FreeV, -NNF, -Paths) is det
Fml,NNF: See above. FreeV: List of free variables in Fml. Paths: Number of disjunctive paths in Fml.
  453% for tracing
  454% nnf(KB,Fin,FreeV,NNF,Paths):- dmsg(nnf(KB,Fin,FreeV,NNF,Paths)),fail.
  455% NonVar used in OUTPUT VAR
  456nnf(KB,Lit,FreeV,LitO,N):-nonvar(LitO),!,nnf1(KB,Lit,FreeV,LitM,N),!,LitM=LitO.
  457nnf(KB,Lit,FreeV,LitO,N):-var(FreeV),!,trace_or_throw(bad_nnf(KB,Lit,FreeV,LitO,N)).
  458nnf(KB,Lit,FreeV,LitO,N):- 
  459  (nb_current('$nnf_outer',Was);Was=[]),
  460  b_setval('$nnf_outer',[Lit|Was]),
  461  nnf1(KB,Lit,FreeV,LitO,N),!.
  462
  463% for tracing
  464% nnf1(KB,Fin,FreeV,NNF,Paths):- dmsg(nnf1(KB,Fin,FreeV,NNF,Paths)),fail.
  465
  466% Sentence was a Variable
  467nnf1(_KB, Lit,FreeV, Lit,1):- is_ftVar(Lit),!, %push_cond(Lit,ftSentence),
  468 discovered_var(Lit,FreeV).
  469nnf1(_KB,Lit,_FreeV,Lit,1):- leave_as_is(Lit),!.
  470nnf1(_KB,~(Lit),_FreeV,~(Lit),1):- leave_as_is(Lit),!.
  471nnf1(_KB,~(Lit),FreeV,~(Lit),1):- is_ftVar(Lit),!, %push_cond(Lit,ftSentence),
  472 discovered_var(Lit,FreeV).
  473
  474
  475
  476
  477% =================================
  478% "Already Horn clauses?"
  479% =================================
  480nnf1(KB,(Q :- P),FreeV,(Q :- PP),Paths):- nnf1(KB,P,FreeV,PP,Paths),!.
  481
  482nnf1(KB,(Q :- P),FreeV,Lit,N):- nnf1(KB,~(Q) => ~(ante(P)),FreeV,Lit,N).
  483
  484
  485
  486% Skipped Args
  487nnf1(_KB,Lit,FreeV,Lit,1):- is_list(Lit),!,discovered_term_slots(Lit,FreeV).
  488% nnf1(_KB,Lit,FreeV,Lit,1):- is_leave_alone(Lit),!,discovered_term_slots(Lit,FreeV).
  489
  490% Catch and REwrite Temporal/Modals missed by preprocessor
  491nnf1(KB,Fin,FreeV,NNF,Paths):- corrected_modal(KB,Fin,F)-> Fin \=@= F,!,nnf1(KB,F,FreeV,NNF,Paths).
  492
  493
  494
  495
  496
  497% =================================
  498% Existential Quantification (defined in common_logic_exists)
  499% =================================
  500
  501nnf1(KB,NNF,NewVars,NNF2,Paths):- 
  502  nnf_ex(KB,NNF,NewVars,NNF2,Paths),!.
  503
  504/*
  505nnf1(KB,'tColOfCollectionSubsetFn'(Col,'tSetOfTheSetOfFn'(Var,Formulas)),FreeV,Var,2):- is_ftVar(Var), \+ is_ftVar(Col),
  506  nnf(KB,all(Var,isa(Var,Col)&Formulas),FreeV,SubForms,_),   
  507   asserta(added_constraints(KB,Var,SubForms)).
  508*/
  509    
  510% Simplification
  511nnf1(KB,~(nesc(BDT,~(F))),FreeV,BOX,Paths):- nonvar(F),!,
  512   nnf1(KB,poss(BDT,F),FreeV,BOX,Paths).
  513
  514nnf1(KB,~(poss(BDT,~(F))),FreeV,BOX,Paths):- nonvar(F),!,
  515   nnf1(KB,nesc(BDT,F),FreeV,BOX,Paths).
  516
  517nnf1(KB,~(nesc(BDT,F)),FreeV,BOX,Paths):- nonvar(F),!,
  518   nnf1(KB,poss(BDT,~(F)),FreeV,BOX,Paths).
  519
  520nnf1(KB,~(poss(BDT,F)),FreeV,BOX,Paths):- nonvar(F),!,
  521   nnf1(KB,nesc(BDT,~(F)),FreeV,BOX,Paths).
  522
  523% =================================
  524% Necessity, Always
  525% =================================
  526
  527nnf1(KB,nesc(BDT,F),FreeV,BOX,Paths):- 
  528   nnf(KB,F,FreeV,NNF,Paths), cnf(KB,NNF,CNF), boxRule(KB,nesc(BDT,CNF), BOX),!.
  529
  530nnf1(KB,nesc(Fin),FreeV,NNF,Paths):- !, nnf(KB,Fin,FreeV,NNF,Paths).
  531nnf1(KB,nesc(_,Fin),FreeV,NNF,Paths):- !, nnf(KB,Fin,FreeV,NNF,Paths).
  532
  533
  534% =================================
  535% Possibly
  536% =================================
  537
  538% dmiles thinks this is ok
  539nnf1(KB,poss(BDT,PQ),FreeV,DIA,Paths):- fail, compound(PQ),PQ = (P=>Q), !,
  540   nnf1(KB,poss(BDT,P)=>Q,FreeV,DIA,Paths).
  541
  542nnf1(KB,poss(BDT,F),FreeV,DIA,Paths):- 
  543   nnf(KB,F,FreeV,NNF,Paths), dnf(KB,NNF,DNF), diaRule(KB,poss(BDT,DNF), DIA).
  544
  545% =================================
  546% Possibly, Eventually / Beliefs / Knows
  547% =================================
  548
  549nnf1(KB, ~( Fml),FreeV,NNF,Paths):- nonvar(Fml),   
  550      (Fml = (beliefs(BDT,~(F))) -> Fml1 = knows(BDT, ( F));
  551       Fml = (knows(BDT,~(F))) -> Fml1 = beliefs(BDT, ( F))
  552	),!,
  553       nnf(KB,Fml1,FreeV,NNF,Paths).
 axiom_lhs_to_rhs(?KB, :LHS, :RHS) is det
Axiom Left-hand-side Converted To Right-hand-side.
  560axiom_lhs_to_rhs(_KB, poss(BDT,beliefs(A,~(F1))),~(nesc(BDT,knows(A,F1)))).
  561axiom_lhs_to_rhs(_KB, all(Vs,poss(BDT,A & B)) ,  ~(exists(Vs,nesc(BDT,A & B)))):- is_ftVar(Vs),!.
  562
  563% disabled
  564nnf1(KB,Fin,FreeV,DIA,Paths):-  fail,  copy_term(Fin,Fml),axiom_lhs_to_rhs(KB,F1,F2) , 
  565 \+ \+ (numbervars(Fin,0,_,[attvar(bind)]),logically_matches(KB,Fin,F1)),
  566  show_success(nnf,(nop(Fml),logically_matches(KB,Fin,F1))),show_call(why,nnf(KB,F2,FreeV,DIA,Paths)).
  567
  568%   poss(beliefs(A,~(F1))) ->  poss(~(knows(A,F1))) ->  ~(nesc(knows(A,F1)))
  569
  570nnf1(KB,cir(CT,F),FreeV,CIR,Paths):-
  571      nnf(KB,F,FreeV,NNF,Paths), 
  572      cirRule(KB,cir(CT,NNF), CIR),!.
  573
  574% % axiom_lhs_to_rhs(KB,poss(- (- LIT)),poss(LIT)):-set_is_lit(LIT).
  575:- style_check(+singleton).  576
  577% =================================
  578% Typed (ForAll ((?x Man)(?y Woman)) ...                     )
  579% =================================
  580
  581nnf1(KB,all(XL,NNF),FreeV,FmlO,Paths):- is_list(XL),
  582    (get_quantifier_isa(XL,X,Col) -> 
  583      nnf(KB,all(X,(isa(X,Col)=>NNF)),FreeV,FmlO,Paths);
  584      (XL=[X|MORE],!,
  585      (MORE==[] -> 
  586            nnf(KB,all(X,NNF),FreeV,FmlO,Paths);
  587            nnf(KB,all(X,all(MORE,NNF)),FreeV,FmlO,Paths)))).
  588
  589% =================================
  590% Global Typed (ForAll ?x  ... )
  591% =================================
  592nnf1(KB,all(X,NNF),FreeV,all(X,NNF2),Paths):- is_using_feature(quants_removed_in_removeQ),!,
  593   add_to_vars(X,FreeV,NewVars),
  594   nnf(KB,NNF,NewVars,NNF2,Paths).
  595   
  596
  597% =================================
  598% Untped (ForAll ?x  ... )
  599% =================================
  600nnf1(KB,all(X,NNF),FreeV, NNF2, Paths):- % is_using_feature(quants_removed_in_NNF),!,     
  601   add_to_vars(X,FreeV,NewVars),
  602   nnf(KB,NNF,NewVars,NNF2,Paths).
  603
  604% =================================
  605%  Temporal LTL/CTL/CTL* Logic
  606% =================================
  607
  608% Release: \phi releases \psi if \psi is true until the first position in which 
  609%  \phi is true (or forever if such a position does not exist). 
  610nnf1(KB,release(CT,CurrentPsi,ReleaserPhi),FreeV,NNF,Paths):- 
  611   share_scopes(KB,CT),!,
  612   Fml1 = (ReleaserPhi => ~(CurrentPsi)),
  613  nnf(KB,Fml1,FreeV,NNF,Paths).
  614
  615% Until: \psi holds at the current or a future position, and \phi has to hold until that position. At that position \phi does not have to hold any more
  616nnf1(KB,until(CurrentPsi,DisablerPhi),FreeV,NNF,Paths):- 
  617  Fml1 = (CurrentPsi v (DisablerPhi => ~(CurrentPsi))),
  618  nnf(KB,Fml1,FreeV,NNF,Paths).
  619
  620% ~(until(Future,Current)) -> ( always(~(Current)) v until(~(Current),(~(Future) & ~(Current))))
  621nnf1(KB,~(until(CT,Future,Current)),FreeV,NNF,Paths):- 
  622
  623   nnf(KB, ~( Future),FreeV,NNFuture,_),
  624   nnf(KB, ~( Current),FreeV,NNCurrent,_),
  625   share_scopes(KB,CT),!,
  626   Fml1 = v(always(NNCurrent), until(CT,NNCurrent,&(NNFuture,NNCurrent))),
  627   nnf(KB,Fml1,FreeV,NNF,Paths).
  628   
  629% ~(cir)(CT,Future) -> cir(CT,~(Future))
  630nnf1(KB,~(cir(CT,Future)),FreeV,NNF,Paths):- 
  631   nnf(KB,cir(CT,~(Future)),FreeV,NNF,Paths),!.
  632
  633% A until B means it B starts after the ending of A
  634axiom_lhs_to_rhs(KB,startsAfterEndingOf(B,A),until(CT,A,B)):- share_scopes(KB,CT),!,set_is_lit(A),set_is_lit(B),!.
  635
  636nnf1(KB,until(CT,A,B),FreeV,NNF,Paths):-  set_is_lit(A),set_is_lit(B),  share_scopes(KB,CT),!,
  637      nnf(KB,A,FreeV,NNF1,Paths1),
  638      nnf(KB,B,FreeV,NNF2,Paths2),
  639	Paths is Paths1 + Paths2,
  640        set_is_lit(NNF1),
  641        set_is_lit(NNF2),
  642	NNF = until(CT,NNF1, NNF2).
  643
  644nnf1(KB,holdsIn(TIMESPAN,TRUTH),FreeV,NNF,Paths):-  
  645  nnf(KB,occuring(TIMESPAN) => TRUTH,FreeV,NNF,Paths).
  646
  647nnf1(KB,holdsIn(TIMESPAN,TRUTH),FreeV,NNF,Paths):-  nnf(KB,temporallySubsumes(TIMESPAN,TRUTH),FreeV,NNF,Paths).
  648
  649nnf1(KB,temporallySubsumes(TIMESPAN,TRUTH),FreeV,NNF,Paths):-  
  650 nnf(KB,(until(CT,TRUTH,~(TIMESPAN))&until(CT,~(TRUTH),TIMESPAN)),FreeV,NNF,Paths).
  651
  652% =================================
  653% Equality
  654% =================================
  655
  656nnf1(KB, ~( different(X , Y)),FreeV,NNF,Paths):- !, nnf(KB, ( equals(X , Y)),FreeV,NNF,Paths).
  657nnf1(KB, ~( equals(X , Y)),FreeV,NNF,Paths):- !, nnf(KB, ( different(X , Y)),FreeV,NNF,Paths).
  658
  659nnf1(KB, ~( ~(different(X , Y))),FreeV,NNF,Paths):- !, nnf(KB, ( ~(equals(X , Y))),FreeV,NNF,Paths).
  660nnf1(KB, ~( ~(equals(X , Y))),FreeV,NNF,Paths):- !, nnf(KB, ( ~(different(X , Y))),FreeV,NNF,Paths).
  661
  662%nnf1(KB,hasName(Entity,Name),FreeV,NNF,Paths):- nonvar(Entity),
  663%   nnf(KB,equals(Entity,Entity0) => hasName(Entity0,Name),FreeV,NNF,Paths).
  664
  665% =================================
  666% Back to Normal NNF-ing 
  667% =================================
  668
  669nnf1(KB, ~( xor(X , Y)),FreeV,NNF,Paths):-
  670   !,
  671  nnf(KB, ((X & Y) v ( ~( X) &  ~( Y))),FreeV,NNF,Paths).
  672   
  673nnf1(KB,xor(X , Y),FreeV,NNF,Paths):-
  674   !,
  675  nnf(KB,((X v Y) & ( ~( X) v  ~( Y))),FreeV,NNF,Paths).
  676   
  677nnf1(KB,(C => (A & B)),FreeV,NNFO,PathsO):- is_using_feature(two_implications),!,
  678      nnf(KB,A,FreeV,NNF1,Paths1),contains_no_negs(NNF1),
  679      nnf(KB,B,FreeV,NNF2,Paths2),contains_no_negs(NNF2),        
  680        to_poss(KB,NNF1,NNF1WFFChk),to_poss(KB,NNF2,NNF2WFFChk),
  681        FullNNF2 = ((NNF1WFFChk => (C => NNF2))),
  682        FullNNF1 = ((NNF2WFFChk => (C => NNF1))),
  683	PathsO is Paths1 * Paths2,
  684	(Paths1 > Paths2 -> NNF = (FullNNF2 & FullNNF1);
  685		            NNF = (FullNNF1 & FullNNF2)),
  686       did_use_hack(two_implications),
  687       nnf(KB,NNF,FreeV,NNFO,PathsO).
  688
  689% not disabled
  690nnf1(KB,(A & B),FreeV,NNF,Paths):- fail, nb_current('$nnf_outer',[_,Was|_]), \+ has_modals(Was),!,
  691  % is_using_feature(co_mingling),!,
  692  to_poss(KB,A,PA),to_poss(KB,B,PB),
  693   NEWFORM = ((PB => A) & (PA => B)) ,
  694   nnf(KB,NEWFORM,FreeV,NNF,Paths).
  695
  696nnf1(KB,(A & B),FreeV,NNF,Paths):- !,
  697      nnf(KB,A,FreeV,NNF1,Paths1),
  698      nnf(KB,B,FreeV,NNF2,Paths2),
  699	Paths is Paths1 * Paths2,
  700	(Paths1 > Paths2 -> NNF = (NNF2 & NNF1);
  701		            NNF = (NNF1 & NNF2)).
  702
  703nnf1(KB,<=>(A,B),FreeV,NNFO,Paths):- !,
  704      nnf(KB,A=>B,FreeV,NNF1,Paths1),
  705      nnf(KB,B=>A,FreeV,NNF2,Paths2),
  706	Paths is Paths1 * Paths2,
  707	(Paths1 > Paths2 -> NNF = (NNF2 & NNF1);
  708		            NNF = (NNF1 & NNF2)),
  709       nnf(KB,NNF,FreeV,NNFO,Paths).
  710
  711nnf1(KB,(A v B),FreeV,NNF,Paths):-
  712        nnf(KB,A,FreeV,NNF1,Paths1),
  713	nnf(KB,B,FreeV,NNF2,Paths2),
  714	Paths is Paths1 + Paths2,
  715	(Paths1 > Paths2 -> NNF = (NNF2 v NNF1);
  716		            NNF = (NNF1 v NNF2)).
  717
  718
  719nnf1(KB, ~( Fml),FreeV,NNF,Paths):- nonvar(Fml), Fml = ~( A) ,!, nnf(KB,A,FreeV,NNF,Paths).
  720nnf1(KB, ~( Fml),FreeV,NNF,Paths):- nonvar(Fml),   
  721
  722        (Fml = ( ~( A)) -> must(double_neg(KB,A,Fml1));
  723         Fml = (nesc(BDT,F)) -> Fml1 = poss(BDT, ~( F));
  724	 Fml = (poss(BDT,F)) -> Fml1 = nesc(BDT, ~( F));
  725
  726	 Fml = (cir(CT,F)) -> Fml1 = cir(CT, ~( F));
  727	 Fml = (until(CT,A,B)) -> 
  728            (nnf(KB, ~( A),FreeV,NNA,_), nnf(KB, ~( B),FreeV,NNB,_),Fml1 = v(always(CT,NNB), until(CT,NNB,&(NNA,NNB))));
  729             
  730         Fml = (exists(X,F)) -> Fml1 = all(X, ~( F));
  731         Fml = (quant(atleast(N),X,F)) -> Fml1 = quant(atmost(N),X,F);
  732         Fml = (quant(atmost(N),X,F)) -> Fml1 = quant(atleast(N),X,F);
  733
  734	 Fml = ((A v B)) -> Fml1 = ( ~( A) &  ~( B) );
  735	 Fml = ((A & B)) -> Fml1 = ( ~( A) v  ~( B) );
  736	 Fml = ('=>'(A,B)) -> Fml1 = ( A  & ~( B) );
  737	 Fml = ('<=>'(A,B)) -> Fml1 = v(&(A,  ~( B)) , &( ~( A), B) )
  738	),!,
  739        must((share_scopes(KB,BDT),share_scopes(KB,CT))),!,
  740	nnf(KB,Fml1,FreeV,NNF,Paths).
  741
  742nnf1(KB,Fml,FreeV,NNF,Paths):-  
  743	(Fml = '=>'(A,B) -> Fml1 = v( ~( A), B );         
  744	 Fml = '<=>'(A,B) -> Fml1 = v(&(A, B), &( ~( A),  ~( B)) );
  745         Fml = '<=>'(A,B) -> Fml1 = v('=>'(A, B), '=>'(B, A) )
  746	),!, nnf(KB,Fml1,FreeV,NNF,Paths).
  747
  748
  749/*
  750
  751% =================================
  752% Higher Order
  753% =================================
  754
  755nnf1(KB,Fml,FreeV,Out,Path):- Fml=..[F,A],third_order(F),  
  756  nnf(KB,A,FreeV,NNF1,Path1),!,
  757  Fml2=..[F,KB,NNF1],nnf(KB,Fml2,FreeV,Out,Path2),Path is Path1+Path2.
  758*/
  759
  760/*
  761
  762nnf1(KB,[F|ARGS],FreeV,[F2|ARGS2],N):- !,
  763   nnf(KB,F,FreeV,F2,N1),
  764   nnf(KB,ARGS,FreeV,ARGS2,N2),
  765   N is N1 + N2 - 1.
  766
  767nnf1(KB,Fml,FreeV,Out,Paths):- 
  768   Fml=..[F|FmlA], 
  769   arg(_,v((v),(&),(=>),(<=>)),F),!,
  770   nnf_l(KB,FmlA,FreeV,NNF,Paths),
  771   Out =..[F|NNF],!.
  772
  773*/
  774
  775% =================================
  776% Forth Order Logic
  777% =================================
  778nnf1(KB,Fml,FreeV,FmlO,Paths):- no_poss(Fml),
  779  breakup_nnf(KB,Fml,FmlM),
  780  Fml\=@=FmlM,
  781  nnf(KB,FmlM,FreeV,FmlO,Paths).
  782
  783
  784% nnf(KB,Fml,_,Fml,1):- Fml=..[F,KB,_],third_order(F),!.
  785
  786
  787% =================================
  788% Logical Atoms
  789% =================================
  790
  791nnf1(_KB,mudEquals(A,B),FreeV,mudEquals(A,B),1):- is_ftVar(A), !,no_freev(FreeV).
  792
  793nnf1(KB, ~( Fml),FreeV,NNF,Paths):- nonvar(Fml), Fml = all(X,F), nnf(KB,exists(X, ~( F)),FreeV,NNF,Paths).
  794
  795nnf1(KB,Fml,FreeV,FmlO,N):- 
  796  compound(Fml),
  797  \+ is_precond_like(Fml),
  798  arg(_,Fml,Function),
  799  compound(Function),
  800  quietly(is_function_expr('=>',Function)),
  801  % quietly(\+ has_function(Function)),
  802  function_to_predicate(Function,NewVar,PredifiedFunction),!,
  803  subst(Fml,Function,NewVar,FmlMid),!,
  804  nnf(KB,all(NewVar,(PredifiedFunction => FmlMid)),FreeV,FmlO,N).
  805
  806nnf1(_KB,PreCond,FreeV,PreCond,1):- is_precond_like(PreCond), !,no_freev(FreeV).
  807
  808
  809% nnf(KB, IN,FreeV,OUT,Paths):- simplify_cheap(IN,MID),IN\=@=MID,nnf(KB, MID,FreeV,OUT,Paths).
  810% nnf(_KB , IN,[],OUT,1):- mnf(IN,OUT),IN\=OUT,!.
  811
  812nnf1(KB,Fml,FreeV,FmlO,N):- must((nonegate(KB,Fml,FmlM),nnf_lit(KB,FmlM,FreeV,FmlO,N))).
  813
  814nnf1(_KB,Fml,_,Fml,1):-!.
  815
  816
  817nnf_l(KB,[FmlA],FreeVA,[NNFA],PathsA):-!,
  818 nnf(KB,FmlA,FreeVA,NNFA,PathsA),!.
  819nnf_l(KB,[FmlA|FmlS],FreeV,[NNFA|NNFS],Paths):-
  820 nnf(KB,FmlA,FreeVA,NNFA,PathsA),
  821 nnf_l(KB,FmlS,FreeVS,NNFS,PathsS),
  822 append(FreeVS,FreeVA,FreeV),
  823 Paths is PathsA + PathsS.
  824nnf_l(_KB,[],[],[],0).
  825
  826
  827no_poss(Fml):- sub_term(Term,Fml),compound(Term),functor(Term,poss,_),!,fail.
  828no_poss(_Fml).
  829
  830no_freev(FreeV):- ignore(FreeV=[]).
  831add_to_vars(X,FreeV,NewVars):- is_list(FreeV),!,list_to_set([X|FreeV],NewVars).
  832add_to_vars(X,FreeV,NewVars):- [X|FreeV]=NewVars.
  833
  834nnf_lit(KB,all(X,Fml),FreeV,all(X,FmlO),N):- nonvar(Fml),!,nnf_lit(KB,Fml,FreeV,FmlO,N).
  835nnf_lit(KB, ~( Fml),FreeV, ~( FmlO),N):- nonvar(Fml),!,nnf_lit(KB,Fml,FreeV,FmlO,N).
  836
  837nnf_lit(_KB,Fml,FreeV,Fml,1):- 
functor(Fml,_,N),N>2,!,no_freev(FreeV).
  838nnf_lit(KB,Fml,FreeV,FmlO,N3):- 
  839   Fml=..[F|ARGS],
  840   nnf_args(Fml,F,1,KB,ARGS,FreeV,FARGS,N1),
  841   Fml2=..[F|FARGS],
  842   (Fml2 \=@= Fml -> 
  843     ((nnf(KB,Fml2,FreeV,FmlO,N2),N3 is (N1 + N2 -1 )));
  844      must((FmlO=Fml2, N3 is N1))).
  845nnf_args(_Sent,_F,_N,_KB,[],_FreeV,[],0):- !.
  846
  847nnf_args(Sent,F,N,KB,[A|RGS],FreeV,[FA|ARGS],N3):- 
 
  848 nop(closure_push(FA,admittedArgument(FA,N,F))),
  849 % push_cond(A,argIsaFn(F,N)),
  850 must((nnf_arg(KB,A,FreeV,FA,N1),sanity(number(N1)))),!,
  851 % push_cond(FA,argIsaFn(F,N)),
  852 % annote(lit,FA,Sent),
  853  NPlus1 is N + 1,
  854  nnf_args(Sent,F,NPlus1,KB,RGS,FreeV,ARGS,N2),
!,
  855  must(N3 is (N1 + N2 -1)).
  856
  857
  858nnf_arg(_KB,A,FreeV,A,1):- quietly(is_arg_leave_alone(A)),!,no_freev(FreeV).
  859nnf_arg(KB,A,FreeV,FA,N1):-  nnf(KB,A,FreeV,FA,N1).
  860
  861is_arg_leave_alone(A):- ground(A).
  862is_arg_leave_alone(A):- is_lit_atom(A).
 is_lit_atom(?IN) is det
If Is A Literal Atom.
  868is_lit_atom(IN):- leave_as_is_logically(IN),!.
  869is_lit_atom(IN):- \+ is_sent_with_f(IN).
  870
  871is_sent_with_f(In):- is_a_sent_funct(F),subst(In,F,*,O),O \== In,!.
  872
  873is_a_sent_funct((&)).
  874is_a_sent_funct((v)).
  875is_a_sent_funct((all)).
  876is_a_sent_funct((exists)).
  877is_a_sent_funct((=>)).
  878is_a_sent_funct((<=>)).
  879is_a_sent_funct((~)).
  880
  881is_sent_like(XY):- \+ compound(XY),!,fail.
  882is_sent_like(_ & _).
  883is_sent_like(_ v _).
  884is_sent_like(_ => _).
  885is_sent_like(_ <=> _).
  886is_sent_like(all(_ , _)).
  887is_sent_like(exists(_ , _)).
  888% is_sent_like(~(_) ).
  889is_sent_like(~(XY)):- is_sent_like(XY).
  890
  891must_distribute_maybe(KB,PAB,Was,OUT):-
  892  subst(PAB,Was,NewArg,NewPab),
  893  functor(PAB,F,_),
  894  must((arg(N,PAB,Arg),Arg==Was)),
  895  copy_term(NewPab:NewArg,CNewPab:CWas),
  896  CWas='$$val$$',
  897  must(distribute_on(F-N,KB,
  898      subst(CNewPab,CWas),Was,OUT)).
  899
  900:- meta_predicate distribute_on(*,*,2,?,?).  901
  902distribute_on(_What,_KB,RE,XY,SAME):- \+ is_sent_like(XY),!, reconstuct(RE,XY,SAME).
  903distribute_on(_What,KB,RE,XY,SAME):- compound(KB),functor(XY,F,_), cant_distrubute_on(F,KB),!,reconstuct(RE,XY,SAME).
  904distribute_on(What,_KB,RE,XY,SAME):- functor(XY,F,_), cant_distrubute_on(F,What),!, reconstuct(RE,XY,SAME).
  905distribute_on(What,KB,RE,((X v Y)),(RECON1 v RECON2)) :- !, distribute_on(What,KB,RE,X,RECON1), distribute_on(What,KB,RE,Y,RECON2).
  906distribute_on(What,KB,RE,((X & Y)),(RECON1 & RECON2)) :- !, distribute_on(What,KB,RE,X,RECON1), distribute_on(What,KB,RE,Y,RECON2).
  907distribute_on(What,KB,RE,((X => Y)),(RECON1 => RECON2)) :- ! , distribute_on(What,KB,RE,X,RECON1), distribute_on(What,KB,RE,Y,RECON2).
  908distribute_on(What,KB,RE,((X <=> Y)),(RECON1 <=> RECON2)) :- ! , distribute_on(What,KB,RE,X,RECON1), distribute_on(What,KB,RE,Y,RECON2).
  909distribute_on(What,KB,RE,(all(V, X)),all(V , RECON1)) :- ! , distribute_on(What,KB,RE,X,RECON1).
  910distribute_on(What,KB,RE,(exists(V, X)),exists(V , RECON1)) :- ! , distribute_on(What,KB,RE,X,RECON1).
  911distribute_on(What,KB,RE, ~(X) , RECON1) :- breakup_nnf(KB,~(X),Xp), ( ~(X) ) \== Xp, ! , distribute_on(What,KB,RE,Xp,RECON1).
  912distribute_on(What,KB,RE, X , RECON1) :- breakup_nnf(KB, X,Xp), ( X ) \== Xp, ! , distribute_on(What,KB,RE,Xp,RECON1).
  913distribute_on(_What,_KB,RE,XY,SAME):- reconstuct(RE,XY,SAME),!.
  914
  915:- meta_predicate reconstuct(2,?,?).  916
  917reconstuct(RE,Arg,OUT):- must(call(RE,Arg,OUT)).
  918
  919can_distrubute_on(Sent,F-N):- !, can_distrubute_on(Sent,F,N).
  920can_distrubute_on(Sent,FN):-  can_distrubute_on(Sent,FN,0).
  921
  922cant_distrubute_on(Sent,F-N):- !, cant_distrubute_on(Sent,F,N).
  923cant_distrubute_on(Sent,FN):- cant_distrubute_on(Sent,FN,0).
  924
  925
  926can_distrubute_on(Sent,F,N):- \+ cant_distrubute_on(Sent,F,N),!,fail.
  927can_distrubute_on(_Sent,_F,_A).
  928
  929% % cant_distrubute_on(exists,F,A):- cant_distrubute_on(&,F,A).
  930% % cant_distrubute_on(all,F,A):- cant_distrubute_on(v,F,A).
  931
  932cant_distrubute_on(v,release,3).
  933cant_distrubute_on(&,release,2).
  934
  935cant_distrubute_on(v,until,2).
  936cant_distrubute_on(&,until,3).
  937
  938% <Thanatological> Yeah ... it doesn''t appear that knowledge is distributive over disjuction.
  939cant_distrubute_on(v,knows,2).
  940cant_distrubute_on(&,beliefs,2).
  941
  942%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  943% breakup_nnf(KB,+F1,?F2)
  944% uses LTL equivalencies to split up LTL formulae
  945% for example, always((f & g)) is converted
  946% into (always(f) & always(g))
  947% These transformations are useful to prevent
  948% blowup in the size of the automata
  949%
  950% ?- breakup_nnf(KB,sometimes((f & g)),X).
  951% X = (sometimes(f) & sometimes(g)).
  952
  953
  954
  955%breakup_nnf(KB,eventually(F),X) :- !, breakup_nnf(KB,until(CT,true,F),X).
  956%breakup_nnf(KB,~(eventually(F)),X) :- !, breakup_nnf(KB,~(until(CT,true,F)),X).
  957
  958breakup_nnf(_,Y,Y):- \+ compound(Y),!.
  959breakup_nnf(_,Y,Y):- is_ftVar(Y),!.
  960breakup_nnf(KB,cir(CT,(X & Y)),(cir(CT,Xp) & cir(CT,Yp))) :- ! , breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  961breakup_nnf(KB,cir(CT,X),cir(CT,Xp)) :- !,  breakup_nnf(KB,X,Xp).
  962
  963breakup_nnf(KB,until(CT,(X & Y),Z),(U & V)) :- !, breakup_nnf(KB,until(CT,X,Z),U), breakup_nnf(KB,until(CT,Y,Z),V).
  964breakup_nnf(KB,until(CT,X,(Y v Z)),(U v V)) :- !, breakup_nnf(KB,until(CT,X,Y),U), breakup_nnf(KB,until(CT,X,Z),V).
  965breakup_nnf(KB,until(CT,X,Y),until(CT,Xp,Yp)) :- !, breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).                                        
  966
  967breakup_nnf(KB,release(CT,(X v Y),Z),(U v V)) :- !, breakup_nnf(KB,release(CT,X,Z),U), breakup_nnf(KB,release(CT,Y,Z),V).
  968breakup_nnf(KB,release(CT,X,(Y & Z)),(U & V)) :- !, breakup_nnf(KB,release(CT,X,Y),U), breakup_nnf(KB,release(CT,X,Z),V).
  969breakup_nnf(KB,release(CT,X,Y),release(CT,Xp,Yp)) :- !, breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  970
  971
  972/*
  973breakup_nnf(KB,knows(Agt,(X v Y)), ~(beliefs(Agt,(~(X) & ~(Y))))) :- !,
  974	breakup_nnf(KB,X,Xp),
  975	breakup_nnf(KB,Y,Yp).
  976
  977breakup_nnf(KB,knows(AG,(~(X) v ~(Y))), ~(beliefs(AG,(U & V)))) :- !, 
  978   breakup_nnf(KB,X,U), breakup_nnf(KB,Y,V).
  979
  980*/
  981
  982breakup_nnf(KB,beliefs(Agt,(X & Y)),(beliefs(Agt,Xp) & beliefs(Agt,Yp))) :- ! ,  breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  983% wrong .. breakup_nnf(KB,knows(Agt,(X v Y)),(beliefs(Agt,Xp) v beliefs(Agt,Yp))) :- ! ,  breakup_nnf(KB,X,Xp),breakup_nnf(KB,Y,Yp).
  984
  985breakup_nnf(KB,(X & Y),(Xp & Yp)) :- breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  986breakup_nnf(KB,(X v Y),(Xp v Yp)) :- breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  987breakup_nnf(KB,~(X),~(Xp)) :- breakup_nnf(KB,X,Xp).
  988breakup_nnf(KB,(X => Y),(Xp => Yp)) :- breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  989breakup_nnf(KB,(X <=> Y),(Xp <=> Yp)) :- breakup_nnf(KB,X,Xp), breakup_nnf(KB,Y,Yp).
  990
  991breakup_nnf(KB,PAB,OUT):- \+ is_sent_like(PAB), arg(_,PAB,XY),is_sent_like(XY),!,must(must_distribute_maybe(KB,PAB,XY,OUT)).
  992breakup_nnf(KB,knows(E,P),knows(E,Q)) :- nnf(KB,P,[],Q,_), !.
  993
  994breakup_nnf(_KB,X,X).
  995
  996
  997
  998/*
  999mnf(Var,Var):-leave_as_is_logically(Var),!.
 1000mnf(Fml,Out):-boxRule(_,Fml,M),Fml\=M,mnf(M,Out).
 1001mnf(Fml,Out):-diaRule(_,Fml,M),Fml\=M,mnf(M,Out).
 1002mnf(poss(DBT,A=>B),Out):- diaRule(_,poss(DBT,v( ~(-,B),A)),M),mnf(M,Out).
 1003mnf(nesc(DBT,A=>B),Out):- mnf(v( ~(-,nesc(DBT, B)), nesc(DBT,A)),M),mnf(M,Out).
 1004mnf([F|Fml],Out):- arg(_,v((v),(&),(=>),(<=>)),F),mnf(Fml,NNF),Out =..[F| NNF].
 1005mnf(Var,Var):-!.
 1006*/
 1007
 1008% poss(P=>Q) ==>  poss( - Q v P )  ==>  - nesc( - ( - Q v P ) ) ==>  - nesc( Q & -P  )    .. how can i get the  nesc/poss very close to the P and Q ?
 1009
 1010% poss(P=>Q)  ==>   ( -nesc(-P) =>  -nesc(-Q) )   ?
 1011
 1012% poss(P=>Q)  ===>   poss( - Q v P ) ===>   poss(- Q) v poss(P)  ===>   - nesc(Q) v poss(P)   ===>      poss(P)=>nesc(Q)  
 1013
 1014% poss(DBT, ~(B) v A) => -nesc(q & -p)
 1015
 1016
 1017%=
 third_order(?VALUE1) is det
Third Order.
 1023third_order(asserted_t).
 1024
 1025
 1026% boxRule(KB,A,B):- convertAndCall(as_dlog,boxRule(KB,A,B)).
 1027
 1028%=
 boxRule(?KB, ?BOX, ?BOX) is det
Datalog Rule.
 1034boxRule(_KB,BOX, BOX):-leave_as_is_logically(BOX),!.
 1035boxRule(KB,nesc(BDT,(A & B)), (BA & BB)):- nonvar(A),!, boxRule(KB,nesc(BDT,A),BA), boxRule(KB,nesc(BDT,B),BB).
 1036% boxRule(KB,nesc(BDT, IN), BOX):- \+ is_lit_atom(IN), share_scopes(KB,BDT), nnf(KB, ~( nesc(BDT,  ~( IN))),BOX).
 1037boxRule(_KB,BOX, BOX).
 1038 
 1039leave_as_is_logically(F):-quietly(leave_as_is_logically0(F)).
 1040
 1041leave_as_is_logically0(Box):- var_or_atomic(Box),!.
 1042leave_as_is_logically0(_:P):-!,leave_as_is_logically0(P).
 1043%leave_as_is_logically0(\+ P):-!,leave_as_is_logically0(P).
 1044leave_as_is_logically0((P:-TRUE)):-!,is_true(TRUE),leave_as_is_logically0(P).
 1045leave_as_is_logically0(DB):-functor(DB,F,A),leave_as_is_logically_fa(F,A),!.
 1046leave_as_is_logically0(NART):-functor(NART,nartR,_),!,ground(NART).
 1047
 1048leave_as_is_logically0(LIST):- is_list(LIST),!, maplist(leave_as_is_logically0,LIST).
 1049% leave_as_is_logically0(~(Box)):- leave_as_is_logically0(Box).
 1050
 1051:- kb_global(baseKB:workflow_holder_queue/1). 1052leave_as_is_logically_fa(meta_argtypes,1).
 1053leave_as_is_logically_fa(skolem,_).
 1054leave_as_is_logically_fa({},1).
 1055leave_as_is_logically_fa(onSpawn,1).
 1056leave_as_is_logically_fa(F,1):-clause_b(workflow_holder_queue(F)),!.
 1057leave_as_is_logically_fa(F,A):-mpred_database_term(F,A,Type),Type\=fact(_),Type\=rule,!.
 1058
 1059%=
 diaRule(?KB, ?A, ?B) is det
Dia Rule.
 1065diaRule(KB,A,B):- convertAndCall(as_dlog,diaRule(KB,A,B)).
 1066diaRule(_KB,BOX, BOX):-leave_as_is_logically(BOX),!.
 1067diaRule(KB,poss(BDT,(A v B)), v(DA,DB)):- !, diaRule(KB,poss(BDT,A),DA), diaRule(KB,poss(BDT,B),DB).
 1068% dmiles thinks this is ok
 1069% diaRule(KB,poss(BDT,(A & B)), &(DA,DB)):- !, diaRule(KB,poss(BDT,A),DA), diaRule(KB,poss(BDT,B),DB).
 1070diaRule(_KB,DIA, DIA).
 1071
 1072
 1073%=
 cirRule(?KB, ?A, ?B) is det
Cir Rule.
 1079cirRule(KB,A,B):- convertAndCall(as_dlog,cirRule(KB,A,B)).
 1080cirRule(_KB,BOX, BOX):-leave_as_is_logically(BOX),!.
 1081cirRule(KB,cir(CT,(A v B)), v(DA,DB)):- !, cirRule(KB,cir(CT,A),DA), cirRule(KB,cir(CT,B),DB).
 1082cirRule(KB,cir(CT,(A & B)), &(DA,DB)):- !, cirRule(KB,cir(CT,A),DA), cirRule(KB,cir(CT,B),DB).
 1083cirRule(_KB,CIR, CIR).
 1084
 1085
 1086
 1087%=
 corrected_modal_recurse(?VALUE1, ?Var, ?OUT) is det
Corrected Modal Recurse.
 1093corrected_modal_recurse(_,Var,OUT):-leave_as_is_logically(Var),!,OUT=Var.
 1094corrected_modal_recurse(KB, IN, OUT):- corrected_modal(KB,IN,OUTM),!,OUT=OUTM.
 1095corrected_modal_recurse(KB, IN, OUTM):- corrected_modal_recurse0(KB, IN, M),!,
 1096  (IN=@=M->OUT=M;corrected_modal_recurse(KB, M, OUT)),!,OUT=OUTM.
 1097
 1098
 1099%=
 corrected_modal_recurse0(?VALUE1, ?Var, ?OUT) is det
Corrected Modal Recurse Primary Helper.
 1105corrected_modal_recurse0(_,Var,OUT):-leave_as_is_logically(Var),!,OUT=Var.
 1106corrected_modal_recurse0(KB, IN,FOO):-  is_list(IN),!, must_maplist_det(corrected_modal_recurse(KB), IN,FOO ),!.
 1107corrected_modal_recurse0(KB, H,FOO):-  compound(H),!,H=..[F|ARGS], must_maplist_det(corrected_modal_recurse(KB), ARGS,FOOL ),!,FOO=..[F|FOOL].
 1108corrected_modal_recurse0(_, INOUT,  INOUT):- !.
 1109
 1110
 1111
 1112
 1113%=
 corrected_modal(?KB, ?IN, ?OUTM) is det
Corrected Modal.
 1119corrected_modal(KB,I,O):- expandQuants(KB,I,M)->I\=@=M,rejiggle_quants(KB,M,O).
 1120corrected_modal(KB,IN,OUTM):-
 1121  corrected_modal0(KB,IN,M),!,must(corrected_modal_recurse0(KB,M,OUT)),!,OUT=OUTM.
 1122
 1123
 1124
 1125%=
 corrected_modal0(?VALUE1, ?Var, :TermARG3) is det
Corrected Modal Primary Helper.
 1131corrected_modal0(_,Var,_):-leave_as_is_logically(Var),!,fail.
 1132corrected_modal0(_,nesc(BDT,F),nesc(BDT,F)):-!.
 1133corrected_modal0(_,poss(BDT,F),poss(BDT,F)):-!.
 1134corrected_modal0(_,until(CT,A,B),until(CT,A,B)):-!.
 1135corrected_modal0(_,cir(CT,F),cir(CT,F)):-!.
 1136corrected_modal0(KB,BF,nesc(b_d(KB,B,D),F)):- BF=..[B,F],b_d_p(B,D).
 1137corrected_modal0(KB,BF,poss(b_d(KB,B,D),F)):- BF=..[D,F],b_d_p(B,D).
 1138corrected_modal0(KB,CF,cir(ct(KB,CT),F)):- CF=..[CT,F],ct_op(CT).
 1139corrected_modal0(KB,CF,until(ct(KB,CT),A,B)):- CF=..[CT,A,B],until_op(CT).
 1140corrected_modal0(_,BF,nesc(b_d(KB,B,D),F)):- BF=..[B,KB,F],b_d_p(B,D).
 1141corrected_modal0(_,BF,poss(b_d(KB,B,D),F)):- BF=..[D,KB,F],b_d_p(B,D).
 1142corrected_modal0(_,CF,cir(ct(KB,CT),F)):- CF=..[CT,KB,F],ct_op(CT).
 1143corrected_modal0(KB,CF,until(ct(KB,CT),A,B)):- CF=..[CT,KB,A,B],until_op(CT).
 1144
 1145
 1146
 1147%=
 share_scopes(?KB, ?BDT) is det
Share Scopes.
 1153share_scopes(KB,BDT):-compound(BDT),ignore(arg(1,BDT,KB)),!.
 1154share_scopes(KB,ENV):-ignore(KB=ENV),!.
 1155
 1156/*
 1157share_scopes(KB,Z,CT,BDT):- ignore(Z=ct(KB,SymNeg)),ignore(BDT=bt(KB,SymNesc,SymPoss)),ignore(CT=ct(KB,SymAllways)),
 1158  ignore(KB=KB),ignore(KB=ct(KB,SymAllways)),ignore(KB=ct(KB,SymUntil)),
 1159  ignore(SymNeg=(-)),
 1160  ignore(SymUntil=(until)),
 1161  ignore(SymNesc=(nesc)),
 1162  ignore(SymPoss=(poss)),
 1163  ignore(SymAllways=(allways)).
 1164*/
 1165
 1166%=
 until_op(?VALUE1) is det
Until Oper..
 1172until_op(until).
 1173
 1174
 1175%=
 ct_op(?VALUE1) is det
Ct Oper..
 1181ct_op(cir).
 1182ct_op(nextly).
 1183
 1184
 1185%ct_op(ist).
 1186%ct_op(asserted_t).
 1187
 1188
 1189%=
 neg_op(?VALUE1) is det
Negated Oper..
 1195neg_op(not).
 1196neg_op(~).
 1197neg_op(~).
 1198neg_op(-).
 1199neg_op('\\+').
 1200
 1201
 1202%=
 b_d_p(?VALUE1, ?VALUE2) is det
Backtackable (debug) Pred.
 1208b_d_p(nesc,poss).
 1209b_d_p(box,dia).
 1210%b_d_p(knows,beliefs).
 1211b_d_p(always,eventually).
 1212b_d_p_1(sometimes,always).
 1213
 1214% b_d(KB,A,I):- genlPreds(I,A).
 1215
 1216%=%
 1217%=%  Conjunctive Normal Form (CNF) : assumes Fml in NNF
 1218%=%
 1219% Usage: cnf(KB, +NNF, ?CNF )
 1220
 1221%=
 cnf(?KB, ?A, ?B) is det
Confunctive Normal Form.
 1227cnf(KB,A,B):- convertAndCall(as_dlog,cnf(KB,A,B)).
 1228cnf(_KB,AS_IS,       AS_IS):-leave_as_is_logically(AS_IS),!.
 1229cnf(KB,&(P,Q), &(P1,Q1)):- !, cnf(KB,P, P1), cnf(KB,Q, Q1).
 1230cnf(KB,v(P,Q),     CNF):- !, cnf(KB,P, P1), cnf(KB,Q, Q1), cnf1(KB, v(P1,Q1), CNF ).
 1231cnf(_KB,CNF,       CNF).
 1232
 1233
 1234%=
 cnf1(?KB, ?AS_IS, ?AS_IS) is det
Confunctive Normal Form Secondary Helper.
 1240cnf1(_KB,AS_IS,       AS_IS):-leave_as_is_logically(AS_IS),!.
 1241cnf1(KB, v(LEFT, R), &(P1,Q1) ):- nonvar_unify(LEFT , &(P,Q)), !, cnf1(KB, v(P,R), P1), cnf1(KB, v(Q,R), Q1).
 1242cnf1(KB, v(P, RIGHT), &(P1,Q1) ):- nonvar_unify(RIGHT , &(Q,R)), !, cnf1(KB, v(P,Q), P1), cnf1(KB, v(P,R), Q1).
 1243cnf1(_KB, CNF,                 CNF).
 1244
 1245
 1246%=
 nonvar_unify(?NONVAR, ?UNIFY) is det
Nonvar Unify.
 1252nonvar_unify(NONVAR,UNIFY):- \+ leave_as_is_logically(NONVAR),  NONVAR=UNIFY.
 1253
 1254%=%
 1255%=% Disjunctive Normal Form (DNF) : assumes Fml in NNF
 1256%=%
 1257% Usage: dnf(KB, +NNF, ?DNF )
 1258
 1259%=
 dnf(?KB, ?A, ?B) is det
Disjunctive Normal Form.
 1265dnf(KB,A,B):- convertAndCall(as_dlog,dnf(KB,A,B)).
 1266dnf(_KB,AS_IS,       AS_IS):-leave_as_is_logically(AS_IS),!.
 1267dnf(KB, v(P,Q),  v(P1,Q1) ):- !, dnf(KB,P, P1), dnf(KB,Q, Q1).
 1268dnf(KB, &(P,Q), DNF):- !, dnf(KB,P, P1), dnf(KB,Q, Q1), dnf1(KB,&(P1,Q1), DNF).
 1269dnf(_KB,DNF,       DNF).
 1270
 1271
 1272%=
 dnf1(?KB, ?DNF, ?DNF) is det
Disjunctive Normal Form Secondary Helper.
 1278dnf1(KB,&(P, v(Q,R)),  v(P1,Q1) ):- !, dnf1(KB,&(P,Q), P1), dnf1(KB,&(P,R), Q1).
 1279dnf1(KB,&(v(P,Q), R), v(P1,Q1) ):- !, dnf1(KB,&(P,R), P1), dnf1(KB,&(Q,R), Q1).
 1280dnf1(_KB,DNF,                  DNF ).
 1281
 1282
 1283
 1284%=
 simplify_cheap(:TermIN, ?IN) is det
Simplify Cheap.
 1290simplify_cheap(IN,OUT):-nonvar(OUT),!,simplify_cheap(IN,M),!,OUT=M.
 1291simplify_cheap(IN,IN):- leave_as_is_logically(IN),!.
 1292simplify_cheap(IN,IN):- var_or_atomic(IN),!.
 1293% simplify_cheap(nesc(BDT,OUT),OUT):- !,nonvar(OUT),is_modal(OUT,BDT),!.
 1294% simplify_cheap(poss(BDT, poss(BDT, F)),  poss(BDT, F)):-nonvar(F),!.
 1295
 1296simplify_cheap( ~( poss(BDT,  ~(  F))), OUT):-nonvar(F),!, simplify_cheap_must(nesc(BDT,F),OUT).
 1297simplify_cheap( ~( nesc(BDT,  ~(  F))), OUT):-nonvar(F),!, simplify_cheap_must(poss(BDT,F),OUT).
 1298simplify_cheap( ~( poss(BDT,  (  F))), OUT):-nonvar(F),!, simplify_cheap_must(nesc(BDT,~(F)),OUT).
 1299simplify_cheap( ~( nesc(BDT,  (  F))), OUT):-nonvar(F),!, simplify_cheap_must(poss(BDT,~(F)),OUT).
 1300simplify_cheap(poss(BDT,IN),OUT):- var_or_atomic(IN),!,poss(BDT,IN)=OUT.
 1301simplify_cheap(nesc(BDT,IN),OUT):- var_or_atomic(IN),!,nesc(BDT,IN)=OUT.
 1302
 1303simplify_cheap(poss(BDT,nesc(BDT,IN)),OUT):- simplify_cheap_must(poss(BDT,IN),OUT).
 1304simplify_cheap(poss(BDT,poss(BDT,IN)),OUT):- simplify_cheap_must(poss(BDT,IN),OUT).
 1305simplify_cheap(nesc(BDT,poss(BDT,IN)),OUT):- simplify_cheap_must(poss(BDT,IN),OUT).
 1306simplify_cheap(nesc(BDT,nesc(BDT,IN)),OUT):- simplify_cheap_must(nesc(BDT,IN),OUT).
 1307%simplify_cheap( ~(  ~( IN)),OUT):- simplify_cheap_must(IN,OUT).
 1308%simplify_cheap( ~(  poss(BDT, poss(BDT, F))),  ~( F)):-nonvar(F),!.
 1309%simplify_cheap(poss(BDT, poss(BDT, F)),  poss(BDT, F)):-nonvar(F),!.
 1310%simplify_cheap( ~( poss(_,  ~(  F))), F):-nonvar(F),!.
 1311%simplify_cheap(IN,-OUT):- IN =  ~( poss(BDT,OUT)), is_modal(OUT,BDT),!.
 1312%simplify_cheap(IN,-OUT):- IN =  ~( nesc(BDT,OUT)), \+is_modal(OUT,BDT),!.
 1313simplify_cheap(INOUT,INOUT).
 1314 
 1315%=
 simplify_cheap_must(?IN, ?IN) is det
Simplify Cheap Must Be Successfull.
 1321simplify_cheap_must(IN,IN):- var_or_atomic(IN),!.
 1322simplify_cheap_must(IN,IN):- leave_as_is_logically(IN),!.
 1323simplify_cheap_must(IN,OUT):- simplify_cheap(IN,OUT),!.
 1324simplify_cheap_must(IN,IN).
 1325
 1326
 1327%=
 1328%=  Prenex Normal Form (PNF)
 1329%=
 1330
 1331% Usage: pfn4(+KB, +Fml, ?PNF ) : assumes Fml in NNF
 1332
 1333
 1334
 1335%=
 pfn4(?KB, ?F, ?PNF) is det
Pnf.
 1341pfn4(KB, F,PNF):- pfn4(KB,F,[],PNF),!.
 1342
 1343% pfn4(+KB, +Fml, +Vars, ?PNF)
 1344
 1345
 1346%=
 pfn4(?A, ?B, ?C, ?D) is det
Pnf.
 1352pfn4(A,B,C,D):- convertAndCall(as_dlog,pfn4(A,B,C,D)),!.
 1353
 1354pfn4(_,Var,_ ,Var):- leave_as_is_logically(Var),!.
 1355
 1356pfn4(_, [],  _,           []):- !.
 1357
 1358pfn4(KB, IN,  _,              OUT):- is_list(IN),!, must_maplist_det(pfn4(KB),IN,OUT).
 1359
 1360%pfn4(KB, IN, FreeV,              OUT):- once(mnf(IN,MID)),IN\=@=MID, pfn4(KB,MID,FreeV,OUT).
 1361%pfn4(KB, IN, FreeV,              OUT):- simplify_cheap(IN,MID), pfn4(KB,MID,FreeV,OUT).
 1362
 1363pfn4(KB,   nesc(BDT,F),Vs,   nesc(BDT,PNF)):- !, pfn4(KB,F,Vs, PNF),!.
 1364
 1365pfn4(KB,   poss(BDT,F),Vs,   poss(BDT,PNF)):- !, pfn4(KB,F,Vs, PNF),!.
 1366
 1367pfn4(KB,   all(X,F),Vs,   all(X,PNF)):- list_to_set([X|Vs],VVs), !, pfn4(KB,F, VVs, PNF),!.
 1368
 1369pfn4(KB,  exists(X,F),Vs,exists(X,PNF)):- list_to_set([X|Vs],VVs), !, pfn4(KB,F, VVs, PNF),!.
 1370
 1371pfn4(KB,  (&(exists(X,A) , B)),Vs,  exists(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pfn4(KB,&(Ay,B),[Y|Vs], PNF),!.
 1372
 1373pfn4(KB,   ( v(exists(X,A)), B),Vs,  exists(Y,PNF)):- !, copy_term((X+A+Vs),(Y+Ay+Vs)), pfn4(KB,(v(Ay,B)),[Y|Vs], PNF).!.
 1374
 1375pfn4(KB, &(all(X,A), B),Vs, all(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pfn4(KB,&(Ay , B),[Y|Vs], PNF),!.
 1376
 1377pfn4(KB, v(all(X,A), B),Vs, all(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pfn4(KB,v(Ay,B),[Y|Vs], PNF),!.
 1378
 1379pfn4(KB, &(A,exists(X,B)),Vs,  exists(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
 1380                                        pfn4(KB,&(A, By),[Y|Vs], PNF),!.
 1381pfn4(KB, v(A,exists(X,B)),Vs,  exists(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
 1382                                        pfn4(KB,v(A,By),[Y|Vs], PNF),!.
 1383pfn4(KB, &(A,all(X,B)),Vs, all(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
 1384                                        pfn4(KB,&(A,By),[Y|Vs], PNF),!.
 1385pfn4(KB, v(A,all(X,B)),Vs, all(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
 1386                                        pfn4(KB,v(A,By),[Y|Vs], PNF),!.
 1387
 1388pfn4(KB, &(A, B),Vs,       PNF ):- pfn4(KB,A,Vs,Ap), pfn4(KB,B,Vs,Bp), 
 1389                                     (A\=Ap; B\=Bp), pfn4(KB,&(Ap,Bp),Vs,PNF),!.
 1390
 1391pfn4(KB, v(A, B),Vs,       PNF ):- pfn4(KB,A,Vs,Ap), pfn4(KB,B,Vs,Bp), 
 1392                                     (A\=Ap; B\=Bp), pfn4(KB,v(Ap,Bp),Vs,PNF),!.
 1393
 1394
 1395pfn4(KB, [A|B], Vs,       PNF ):- !, pfn4(KB,A,Vs,Ap), pfn4(KB,B,Vs,Bp), 
 1396                                     (A\=Ap; B\=Bp), pfn4(KB,[Ap|Bp],Vs,PNF),!.
 1397
 1398
 1399% disabled
 1400pfn4(KB, H,Vars,FOO ):- fail,  compound(H),H=..[F|ARGS], is_sentence_functor(F), !, pfn4(KB, [F|ARGS],Vars,FOOL ),FOO=..FOOL.
 1401
 1402pfn4(_KB,          PNF, _,       PNF ).
 1403
 1404
 1405:- meta_predicate if_debugging2(*,0). 1406% if_debugging2(_,_):- !.
 1407if_debugging2(_,G):- call(G).
 1408%=%  Clausal Form (CF) : assumes Fml in PNF and
 1409%                                 each quantified variable is unique
 1410
 1411% cf(+Why,+KB,+Fml, -Cs)
 1412% Cs is a list of the form: [cl(Head,Body), ...]
 1413% Head and Body are lists.
 1414
 1415% cf(Why,KB,A,B,C):- convertAndCall(as_dlog,cf(Why,KB,A,B,C)).
 cf(?Why, ?KB, ?Original, ?PNF, ?CLAUSESET) is det
Convert to Clausal Form
 1423cf(_Why,KB,_Original,PNF, FlattenedOUT):- fail,   
 1424  check_kif_varnames(PNF),
 1425  removeQ(KB,PNF,[], UnQ),
 1426  cnf(KB,UnQ,CNF0),!,
 1427  nnf(KB,CNF0,[],CNF,_),
 1428  as_prolog_hook(CNF,PROLOG),
 1429  tlog_nnf(PROLOG,even,RULIFY),  
 1430  rulify(constraint,RULIFY,FlattenedOUT),!.
 1431
 1432cf(Why,KB,_Original,PNF, FlattenedOUT):- 
 1433 must_det_l((
 1434  check_kif_varnames(PNF),
 1435  removeQ(KB,PNF,[], UnQ),
 1436  cnf(KB,UnQ,CNF0),!,
 1437  nnf(KB,CNF0,[],CNF,_), 
 1438  % wdmsg(cnf:-CNF),
 1439 call(( conjuncts_to_list_det(CNF,Conj), make_clause_set([infer_by(Why)],Conj,EachClause),
 1440  sanity(is_list(EachClause)),
 1441  must_maplist_det(correct_cls(KB),EachClause,SOO),
 1442  expand_cl(KB,SOO,SOOO))),
 1443  predsort(sort_by_pred_class,SOOO,SET),
 1444  cf_to_flattened_clauses(KB,Why,SET,Flattened),
 1445  list_to_set(Flattened,FlattenedM),!,
 1446  correct_boxlog(FlattenedM,KB,Why,FlattenedOOO),
 1447  demodal_clauses(KB,FlattenedOOO,FlattenedO),  
 1448  defunctionalize_each(FlattenedO,FlattenedOUT),
 1449  nop((((pfc_for_print_left(FlattenedOOO,PrintPFC),wdmsg(boxlog:-PrintPFC),
 1450  maybe_notrace(boxlog_to_pfc(FlattenedO,PFCPreview)),
 1451  pfc_for_print_right(PFCPreview,PrintPFCPreview),wdmsg(preview:-PrintPFCPreview))),!,
 1452  extract_conditions(PFCPreview,Conds), dmsg(conds= (Conds=>PFCPreview)))))).
 1453
 1454check_kif_varnames(KIF):-check_varnames(KIF),fail.
 1455check_kif_varnames(KIF):-ground(KIF),!.
 1456%check_kif_varnames(KIF):-show_call(term_attvars(KIF,Vs)),Vs\==[].
 1457check_kif_varnames(_KIF):-!.
 1458      
 1459
 1460
 1461conjuncts_to_list_det(I,O):- conjuncts_to_list(I,O),!.
 1462list_to_conjuncts_det(C,I,O):- list_to_conjuncts(C,I,O),!.
 1463list_to_conjuncts_det(I,O):- list_to_conjuncts(I,O),!.
 1464
 1465%= 	 	 
 1466
 1467%% clean_repeats_d( ?PTTP, ?PTTP) is det.
 1468%
 1469% Clean Repeats (debug).
 1470%
 1471clean_repeats_d((PTT,P0),PTTP):-!, conjuncts_to_list_det((PTT,P0),DLIST),list_to_set(DLIST,DSET),must_maplist_det(clean_repeats_d,DSET,CSET),list_to_conjuncts_det((,),CSET,PTTP),!.
 1472clean_repeats_d((PTT;P0),PTTP):-!, disjuncts_to_list((PTT;P0),DLIST),list_to_set(DLIST,DSET),must_maplist_det(clean_repeats_d,DSET,CSET),list_to_conjuncts_det((;),CSET,PTTP),!.
 1473clean_repeats_d(PTTP,PTTP).
 1474
 1475
 1476
 1477%=
 invert_modal(+KB, +A, -B) is det
Invert Modal.
 1484invert_modal(_KB,nesc(BD,A),poss(BD,A)):-set_is_lit(A),!.
 1485invert_modal(_KB,poss(BD,A),nesc(BD,A)):-set_is_lit(A),!.
 1486invert_modal(KB,A,OUT):- must(adjust_kif0(KB,poss(A),OUT)).
 1487
 1488% invert_modal(KB,A,poss(b_d(KB,nesc,poss),A)):- is_using_feature(default_nesc),set_is_lit(A),!.
 1489% invert_modal(KB,A,A):-!.
 1490
 1491
 1492
 1493% double_neg(_KB,In,_):- is_ftVar(In),!,fail.
 1494double_neg(KB,I,O):- invert_modal(KB,I,O)->I\=O,!.
 1495double_neg(_,IO,IO):-!.
 1496% double_neg(_KB,I,O):- weaken_to_poss(I,O).
 1497% double_neg(KB,I, \+ ~(O)):-!.
 1498
 1499
 1500%=
 removeQ(?KB, ?F, ?HH) is det
Remove Q.
 1506removeQ(KB, F,  HH):- removeQ(KB, F, _, RQ0),!,RQ0=HH.
 1507
 1508% removes quantifiers (also pushes modal operators inside the negations) 
 1509
 1510
 1511%=
 removeQ_LC(?KB, ?MID, ?FreeV, ?OUT) is det
Remove Q Lc.
 1517removeQ_LC(KB, MID,FreeV,OUT):-loop_check(removeQ(KB, MID,FreeV,OUT)).
 1518
 1519
 1520%=
 removeQ(?VALUE1, :TermVar, ?VALUE3, :TermVar) is det
Remove Q.
 1526removeQ(_,Var,_ ,Var):- leave_as_is_logically(Var),!.
 1527
 1528% removeQ(KB, H, Vars, HH ):- convertAndCall(as_dlog,removeQ(KB,H, Vars, HH )).
 1529removeQ(KB, IN,FreeV,OUT):-  once(simplify_cheap(IN,MID)), IN\=@=MID, removeQ_LC(KB, MID,FreeV,OUT),!.
 1530
 1531removeQ(KB,  ~( NN),Vars, XF):- nonvar(NN),NN= ~( F), invert_modal(KB,F,FI),!, removeQ(KB,  FI,Vars, XF) .
 1532removeQ(KB, all(X,F),Vars, HH):- !,  removeQ(KB,F,[X|Vars], RQ0),RQ0=HH.
 1533
 1534/*
 1535removeQ(KB,  ~( nesc(BDT,  ~( F))),Vars, XF):- !,removeQ_LC(KB, poss(BDT, F),Vars, XF).
 1536removeQ(KB,  ~( poss(BDT,  ~( F))),Vars, XF):- !,removeQ_LC(KB, nesc(BDT, F),Vars, XF).
 1537
 1538removeQ(KB,  ~( nesc(BDT, (F))),Vars, XF):- !,removeQ(KB, poss(BDT,  ~( F)),Vars, XF).
 1539removeQ(KB,  ~( poss(BDT, (F))),Vars, XF):- !,removeQ(KB, nesc(BDT,  ~( F)),Vars, XF).
 1540*/
 1541
 1542% removeQ(KB, nesc(BDT,  ~( F)),Vars, XF):- !,removeQ(KB,  ~( poss(BDT, F)),Vars, XF).
 1543% removeQ(KB, poss(BDT,  ~( F)),Vars, XF):- !,removeQ(KB,  ~( nesc(BDT, F)),Vars, XF).
 1544
 1545removeQ(KB,  exists(X,F),Vars, HH):- is_skolem_setting(removeQ),!,wdmsg(removeQ(skolemizing(exists(X,F)))),
 1546	mk_skolem(KB,F,X,Vars,Fsk),
 1547	removeQ(KB,Fsk,Vars, HH).
 1548
 1549removeQ(KB, exists(X,F),Vars, HH):-   must(removeQ(KB,F,[X|Vars], RQ0)),RQ0=HH.
 1550
 1551removeQ(KB, ':-'(H,B), Vars, ':-'(HH,BB ) ):- !, removeQ(KB,H, Vars, HH ),removeQ(KB,B, Vars, BB).
 1552removeQ(KB, cl(H,B), _, O ):- !,correct_cls(KB,cl(H,B),O).
 1553removeQ(KB,     [ H|B ],Vars, [ HH|BB ] ):- !,removeQ(KB,H, Vars, HH ),removeQ(KB,B, Vars, BB).
 1554
 1555%removeQ(KB, H, Vars, HH ):- functor(H,F,1),adjust_kif(KB,H,MM),H\=@=MM,!, removeQ(KB, MM, Vars, HH ).
 1556
 1557%removeQ(KB, H, Vars,HH ):- functor(H,F,1),kb_nlit(KB,F),once(nnf(KB,H,MM)),H\=@=MM,  removeQ_LC(KB, MM, Vars, HH ).
 1558removeQ(KB, H,  Vars,HH ):- H =  ~(  _), once(nnf(KB,H,MM)),H\=@=MM,  removeQ_LC(KB, MM, Vars, HH ).
 1559
 1560removeQ(KB, H, Vars, HH ):- convertAndCall(as_dlog,removeQ(KB,H, Vars, HH )).
 1561
 1562removeQ(KB, H,Vars,HH ):- compound(H),H=..[F|ARGS],!,removeQ(KB, ARGS,Vars,ARGSO ),HH=..[F|ARGSO].
 1563
 1564removeQ(KB, F,Vars,OUT ):- nnf(KB,F,Vars,F0,_),(F0 =@=F -> F0=OUT; removeQ(KB, F0,Vars,OUT )),!.
 1565
 1566
 1567
 1568
 1569
 1570%=
 nowrap_one(?Wrap, ?MORE, ?OUT) is det
Nowrap One.
 1576nowrap_one(_,[One],One).
 1577nowrap_one(Wrap,MORE,OUT):- OUT=..[Wrap,MORE].
 1578
 1579
 1580
 1581%=
 demodal_sents(?KB, ?I, ?O) is det
Demodal Sentences.
 1587demodal_sents(KB,I,O):- must(to_modal1(KB,I,M)),must(modal2sent(M,O)).
 1588
 1589
 1590%=
 to_modal1(?KB, :TermIn, ?Prolog) is det
Demodal.
 1597% to_modal1(KB,In,Prolog):- call_last_is_var(to_modal1(KB,In,Prolog)),!.
 1598
 1599to_modal1(KB,Var, NonVar):-  nonvar(NonVar),!,to_modal1(KB,Var, NewVar),!, NewVar=NonVar.
 1600
 1601to_modal1(_KB,Var, Var):- quietly(var_or_atomic(Var)),!.
 1602
 1603to_modal1(KB,[H|T],[HH|TT]):- !, to_modal1(KB,H,HH),to_modal1(KB,T,TT).
 1604
 1605to_modal1(KB, nesc(b_d(KB2,X,_),F), HH):- atom(X),KB\==KB2,XF =..[X,KB2,F],!,to_modal1(KB2,XF, HH).
 1606to_modal1(KB, poss(b_d(KB2,_,X),F), HH):- atom(X),KB\==KB2,XF =..[X,KB2,F],!,to_modal1(KB2,XF, HH).
 1607
 1608to_modal1(KB, nesc(b_d(KB,X,_),F),   HH):- atom(X), XF =..[X,F], !,to_modal1(KB,XF, HH).
 1609to_modal1(KB, poss(b_d(KB,_,X),F),   HH):- atom(X), XF =..[X,F], !,to_modal1(KB,XF, HH).
 1610
 1611to_modal1(KB, -XF,   ~(HH)):- !,to_modal1(KB,XF, HH).
 1612
 1613to_modal1(KB, nesc(_,F),   HH):- XF =..[nesc,F], !,to_modal1(KB,XF, HH).
 1614to_modal1(KB, poss(_,F),   HH):- XF =..[poss,F], !,to_modal1(KB,XF, HH).
 1615
 1616to_modal1(KB,H,HH ):- H=..[F|ARGS],!,must_maplist_det(to_modal1(KB),ARGS,ARGSO),!,HH=..[F|ARGSO].
 1617
 1618
 1619%=
 is_sent_op_modality(?VALUE1) is det
If Is A Sentence Oper. Modality.
 1625is_sent_op_modality(not).
 1626is_sent_op_modality(poss).
 1627is_sent_op_modality(nesc).
 1628
 1629has_modals(P):- quietly((sub_term(A,P),compound(A),(functor(A,poss,_);functor(A,nesc,_)))),!.
 1630
 1631%=
 atom_compat(?F, ?HF, ?HHF) is det
Atom Compat.
 1637 /* disabled */
 1638atom_compat(F,HF,HHF):- fail,F\=HF, is_sent_op_modality(F),is_sent_op_modality(HF), format(atom(HHF),'~w_~w',[F,HF]).
 1639
 1640remove_unused_clauses([],[]):- !.
 1641remove_unused_clauses([Unused|FlattenedO4],FlattenedO):- 
 1642   unused_clause(Unused) -> remove_unused_clauses(FlattenedO4,FlattenedO);
 1643     (remove_unused_clauses(FlattenedO4,FlattenedM),FlattenedO=[Unused|FlattenedM]).
 1644
 1645unusual_body :- clause_b(feature_setting(use_unusual_body,true)),!,dmsg(used(unusual_body)).
 1646unusual_body :- dmsg(skipped(unusual_body)),!,fail.
 1647
 1648unused_clause('$unused'(C):-_):-nonvar(C),!.
 1649%unused_clause((C v _):-_):-nonvar(C),!.
 1650unused_clause(naf(C):- ~(_)):-nonvar(C),!.
 1651
 1652
 1653poss_or_skolem(Var):- \+ compound(Var),!,fail.
 1654poss_or_skolem(poss(_)).
 1655poss_or_skolem(dif_objs(_,_)).
 1656poss_or_skolem(nesc(X)):-!,poss_or_skolem(X).
 1657poss_or_skolem(falsify(X)):-!,poss_or_skolem(X).
 1658% MAYBE? poss_or_skolem(needs(_)).
 1659poss_or_skolem(skolem(_,_)).
 1660% poss_or_skolem(P):-arg(_,P,E),is_list(E).
 1661
 1662%%% ***
 1663%%% ****if* PTTP/disjoin
 1664%%% SOURCE
 1665
 1666disjoin(A,B,C) :-
 1667	A == true ->
 1668		C = true;
 1669	B == true ->
 1670		C = true;
 1671	A == false ->
 1672		C = B;
 1673	B == false ->
 1674		C = A;
 1675	%true ->
 1676		C = (A ; B).
 1677
 1678
 1679pos_or_isa(isa(_,_)).
 1680pos_or_isa(poss(_)).
 1681
 1682pred_of(Head, Head):- is_ftVar(Head),!.
 1683pred_of(~(Head), Head).
 1684pred_of(Head, Head).
 1685
 1686
 1687reverse_conj((A,B),Body):- !, reverse_conj(B,RB),conjoin(RB,A,Body).
 1688reverse_conj(Body,Body).
 1689
 1690
 1691%=
 modal2sent(:TermVar, :TermVar) is det
Modal2sent.
 1697modal2sent(Var, Var):- !.
 1698modal2sent(Var, Var):- quietly(var_or_atomic(Var)),!.
 1699% modal2sent(G,O):- G=..[F,H], \+ leave_as_is(H), H=..[HF,HH], atom_compat(F,HF,HHF),!, GG=..[HHF,HH], modal2sent(GG,O).
 1700modal2sent([H|T],[HH|TT]):- !, must(( modal2sent(H,HH),modal2sent(T,TT))),!.
 1701modal2sent(poss([infer_by(_)],G), \+ ~(G)):- G \= ~(_).
 1702modal2sent(nesc([infer_by(_)],G),G):- G \= ~(_).
 1703%modal2sent(naf(~(poss(~(G)))), G):- nonvar(G),!.
 1704%modal2sent(naf(~(skolem(A,B))),skolem(A,B)):- nonvar(B),!.
 1705modal2sent(H,HH ):- H=..[F|ARGS],!,must_maplist_det(modal2sent,ARGS,ARGSO),!,HH=..[F|ARGSO].
 1706
 1707
 1708var_or_atomic(Var):- is_ftVar(Var),!.
 1709var_or_atomic([]):-!.
 1710var_or_atomic(Var):- atomic(Var),!.
 1711
 1712%=
 clausify(?KB, ?P, ?C, ?C) is det
Clausify.
 1718clausify(KB, &(P,Q), C1, C2 ):- 
 1719	!,
 1720	clausify(KB, P, C1, C3 ),
 1721	clausify(KB, Q, C3, C2 ).
 1722clausify(KB, P, [cl(A,B)|Cs], Cs ):- 
 1723	inclause(KB, P, A, [], B, [] ),
 1724	!.
 1725clausify(_KB, _, C, C ).
 1726
 1727
 1728%=
 inclause(?KB, ?P, ?A1, ?A, ?B, ?B) is det
Inclause.
 1734inclause(KB, v(P,Q), A, A1, B, B1 ):- 
 1735	!,
 1736	inclause(KB, P, A2, A1, B2, B1 ),
 1737	inclause(KB, Q, A,  A2, B,  B2 ).
 1738inclause(KB,  ~(  PP) , A,  A, B1, B ):- 
 1739        negate(KB,  ~(  PP),P),
 1740	!,
 1741	notin(P, A ),
 1742	putin(P, B, B1 ).
 1743inclause(_KB, P,  A1, A, B,  B ):- 
 1744	!,
 1745	notin(P, B ),
 1746	putin(P, A, A1 ).
 1747
 1748
 1749%=
 notin(?X, ?Y) is det
Notin.
 1755notin(X,[Y|_]):- X==Y, !, fail.
 1756notin(X,[_|Y]):- !,notin(X,Y).
 1757notin(_,[]).
 1758
 1759
 1760%=
 putin(?X, :TermARG2, :TermX) is det
Putin.
 1766putin(X,[],   [X]   ):- !.
 1767putin(X,[Y|L],[Y|L] ):- X == Y,!.
 1768putin(X,[Y|L],[Y|L1]):- putin(X,L,L1).
 1769
 1770
 1771%=
 simplify_atom(?H, ?SH) is det
Simplify Atom.
 1777simplify_atom(H,SH):-simplify_cheap(H,SH),!.
 1778simplify_atom(H,H).
 1779
 1780
 1781%= 	 	 
 1782
 1783%% to_regular_cl( ?KB, ?H1, ?Has, ?H1) is det.
 1784%
 1785% Converted To Regular Clause.
 1786%
 1787to_regular_cl(KB,[(H1 & H2)],[Has],[cl([H1],H1P),cl([H2],H2P)]):- cnf(KB,Has,HasC),  append([HasC],[poss(H2)],H1P), append([HasC],[poss(H1)],H2P),!.
 1788to_regular_cl(_KB,[(H1 & H2)],Has,[cl([H1],H1P),cl([H2],H2P)]):-  append(Has,[poss(H2)],H1P), append(Has,[poss(H1)],H2P),!.
 1789to_regular_cl(_KB,[H],[],[cl([SH],[])]):-is_lit_atom(H),simplify_atom(H,SH).
 1790to_regular_cl(_KB,HL,BL,[cl(HL,BL)]).
 1791
 1792
 1793
 1794%=
 expand_cl(?KB, :TermARG2, ?VALUE3) is det
Expand Clause.
 1800expand_cl(_KB,[],[]):-!.
 1801expand_cl(KB,[cl(H,B)|O],OOut):- 
 1802      to_regular_cl(KB,H,B,More),!,
 1803      expand_cl(KB,O,OO),
 1804      append(More,OO,OOut).
 1805
 1806
 1807%=
 make_clause_set(?Extras, :TermARG2, ?VALUE3) is det
Make Clause SET.
 1813make_clause_set(_Extras ,[],[]).
 1814make_clause_set(Extras,[CJ|Conj],CLAUSES):-
 1815   make_clauses(Extras,CJ,CLS),
 1816   make_clause_set(Extras,Conj,CLAUS),
 1817   append(CLS,CLAUS,CLAUSES).
 1818
 1819% make_clauses(Extras,_,[CJ],cl([CJ],[])):-is_lit_atom(CJ),!.
 1820
 1821%=
 make_clauses(?Extras, ?CJ, ?OOut) is det
Make Clauses.
 1827make_clauses(Extras,CJ,OOut):- disjuncts_to_list(CJ,Conj),make_clause_from_set(Extras,Conj,OOut).
 1828
 1829
 1830%=
 negate_one_maybe(?Extras, ?One, ?Z) is det
Negate One Maybe.
 1836negate_one_maybe(Extras,One,Z):-negate_one(Extras,One,Z).
 1837   
 1838
 1839%=
 make_clause_from_set(?Extras, ?Conj, ?Out) is det
Make Clause Converted From SET.
 1845make_clause_from_set(Extras,Conj,Out):- findall(E,make_each(Extras,Conj,E),Out).
 1846
 1847
 1848%=
 make_each(?Extras, ?Conj, ?E) is det
Make Each.
 1854make_each(Extras,Conj,E):- member(One,Conj), make_1_cl(Extras,One,Conj,E).
 1855
 1856
 1857%=
 make_1_cl(?Extras, ?One, ?Conj, :TermOne) is det
make Secondary Helper Clause.
 1863make_1_cl(Extras,One,Conj,cl([One],NewBodyListO)):- 
 1864  negate_one_maybe(Extras,One,NHead),!,
 1865  One\={_}, NHead\={_},
 1866  delete_eq(Conj,One,Rest0),delete_eq(Rest0,NHead,Rest),
 1867  must_maplist_det(negate_one_maybe(Extras),Rest,NewBodyList),!,
 1868  flattenConjs(Extras,NewBodyList,NewBodyListM),
 1869  Pred= baseKB:as_prolog_hook, must_maplist_det(Pred,NewBodyListM,NewBodyListO).
 1870
 1871
 1872%=
 flattenConjs(?Extras, ?I, ?O) is det
Flatten Conjs.
 1878flattenConjs(_Extras,I,O):- conjuncts_to_list_det(I,M),must_maplist_det(conjuncts_to_list_det,M,L),flatten(L,O).
 1879
 1880
 1881:- was_export(logical_pos/3). 1882:- was_export(logical_neg/3). 1883
 1884%=
 logical_neg(?KB, ?Wff, ?WffO) is det
Logical Negated.
 1890logical_neg(KB,Wff,WffO):- 
 1891  must(nonegate(KB,Wff,Wff1)),nnf(KB, ~( Wff1),Wff2),must(nonegate(KB,Wff2,WffO)),!.
 1892
 1893%=
 logical_pos(?KB, ?Wff, ?WffO) is det
Logical Pos.
 1899logical_pos(KB,Wff,WffO):- 
 1900  must(nonegate(KB,Wff,Wff1)),nnf(KB,Wff1,Wff2),must(nonegate(KB,Wff2,WffO)),!.
 1901
 1902
 1903
 1904%=
 negate_one(?KB, ?Wff, ?WffO) is det
Negate One.
 1910negate_one(KB,Wff,WffO):- logical_neg(KB,Wff,WffO).
 1911
 1912
 1913
 1914%=
 negate(?KB, ?X, ?Z) is det
Negate.
 1920negate(KB,X,Z):- must(defunctionalize(X,Y)), must_det(negate0(KB,Y,Z)).
 1921
 1922%=
 negate0(?VALUE1, ?X, ?X) is det
Negate Primary Helper.
 1928negate0(_, ~( X),X).
 1929negate0(_,X, ~( X)).
 1930
 1931
 1932
 1933
 1934%=
 mpred_quf(?In, ?Out) is det
Managed Predicate Quf.
 1940mpred_quf(In,Out):- transitive(mpred_quf_0,In,Out).
 1941
 1942
 1943%=
 mpred_quf_0(?InOut, ?InOut) is det
Managed Predicate quf Primary Helper.
 1949mpred_quf_0(InOut,InOut):- not_ftCompound(InOut),!.
 1950% mpred_quf_0(In,Out):- current_predicate(db_quf/4),db_quf(clause(assert,_Must),In,U,C),conjoin(U,C,Out).
 1951mpred_quf_0(In,In).
 1952
 1953:- was_export(nonegate/3). 1954
 1955%=
 nonegate(?KB, ?IO, ?IO) is det
Nonegate.
 1961nonegate(_KB,IO,IO):-!.
 1962nonegate(KB,List,OutZ):- is_list(List),must_maplist_det(nonegate(KB),List,OutZ),!.
 1963nonegate(KB,Fml,OutZ):- simplify_cheap(Fml,Fml2)-> Fml \=@= Fml2,nonegate(KB,Fml2,OutZ),!.
 1964nonegate(KB,Fml,OutZ):- must((unbuiltin_negate(KB,Fml,Out),!,defunctionalize(Out,OutY),!,must(mpred_quf(OutY,OutZ)))),!.
 1965
 1966
 1967%=
 unbuiltin_negate(?Z, ?VALUE2, ?Fml, ?Fml) is det
Unbuiltin Negate.
 1973unbuiltin_negate(_Neg,_, Fml,Fml):- is_ftVar(Fml),!.
 1974unbuiltin_negate(_Neg,_, Fml,Out):- get_functor(Fml,F,A),find_and_call(pttp_builtin(F,A)),!,must(Out=Fml).
 1975
 1976%=
 unbuiltin_negate(?KB, ?Fml, ?Out) is det
Unbuiltin Negate.
 1982unbuiltin_negate(_KB,Fml,Out):- once(negate(KB,Fml,Z)),negate(KB,Z,Out),!.
 1983
 1984
 1985
 1986/*
 1987
 1988
 1989%=% Substitution
 1990
 1991% Usage: subst_except(+Fml,+X,+Sk,?FmlSk)
 1992subst_except(Fml,X,Sk,FmlSkO):- pred_subst(==,Fml,X,Sk,FmlSk),!,must(FmlSkO=FmlSk).
 1993
 1994
 1995% Usage: pred_subst(+Pred,+Fml,+X,+Sk,?FmlSk)
 1996pred_subst(Pred,   all(Y,P), X,Sk,   all(Y,P1) ):- !, pred_subst(Pred, P,X,Sk,P1 ).
 1997pred_subst(Pred,exists(Y,P), X,Sk,exists(Y,P1) ):- !, pred_subst(Pred, P,X,Sk,P1 ).
 1998pred_subst(Pred, &(P,Q), X,Sk,&(P1,Q1) ):- !, pred_subst(Pred, P,X,Sk,P1 ), pred_subst(Pred, Q,X,Sk,Q1 ).
 1999pred_subst(Pred,  v(P,Q), X,Sk, v(P1,Q1) ):- !, pred_subst(Pred, P,X,Sk,P1 ), pred_subst(Pred, Q,X,Sk,Q1 ).
 2000
 2001pred_subst(Pred,       P,    X,Sk,       P1    ):- call(Pred,P,X), Sk=P1,!.
 2002pred_subst(_Pred,       P,    _,_,       P1    ):- is_ftVar(P), P1=P,!.
 2003pred_subst(Pred,       P,    X,Sk,       P1    ):- compound(P),
 2004                             P =..Args, 
 2005                               pred_subst2(Pred, X, Sk, Args, ArgS ),!,
 2006                             P1 =..ArgS.
 2007pred_subst(_  ,        P,    _, _,       P     ).
 2008
 2009pred_subst2(_   , _,  _, [], [] ).
 2010pred_subst2(Pred, X, Sk, [A|As], [Sk|AS] ):- call(Pred, X, A), !, pred_subst2(Pred, X, Sk, As, AS).
 2011pred_subst2(Pred, X, Sk, [A|As], [A|AS]  ):- is_ftVar(A), !, pred_subst2(Pred, X, Sk, As, AS).
 2012pred_subst2(Pred, X, Sk, [A|As], [Ap|AS] ):- pred_subst(Pred, A,X,Sk,Ap ), pred_subst2(Pred, X, Sk, As, AS).
 2013*/
 2014
 2015
 2016%= 	 	 
 2017
 2018
 2019
 2020%=
 removes_literal(:TermX, :TermX) is det
Removes Literal.
 2026removes_literal(true_t(X),possible_t(X)).
 2027removes_literal(true_t(X,Y),possible_t(X,Y)).
 2028removes_literal(true_t(X,Y,Z),possible_t(X,Y,Z)).
 2029removes_literal(true_t(X,Y,Z,A),possible_t(X,Y,Z,A)).
 2030
 2031removes_literal(not_true_t(X),possible_t(X)).
 2032removes_literal(not_true_t(X,Y),possible_t(X,Y)).
 2033removes_literal(not_true_t(X,Y,Z),possible_t(X,Y,Z)).
 2034removes_literal(not_true_t(X,Y,Z,A),possible_t(X,Y,Z,A)).
 2035
 2036
 2037
 2038
 2039%=
 delete_sublits(?H0, ?B, ?HH) is det
Delete Sublits.
 2045delete_sublits(H0,B,HH):- delete_eq(H0,B,H1),delete_eq(H1,B,H2),delete_eq(H2,B,HH),!.
 2046
 2047% cl([-nesc(p)], [-poss(p), nesc(q), -poss(q)]).
 2048
 2049
 2050
 2051%=
 flatten_clauses(?H, ?HHTT) is det
Flatten Clauses.
 2057flatten_clauses([H|T],HHTT):-!,flatten_clauses(H,HH),flatten_clauses(T,TT),append(HH,TT,HHTT).
 2058flatten_clauses(poss(~(~(H))),poss(HH)):- !,flatten_clauses(H,HH),!.
 2059flatten_clauses(nesc(~(~(H))),HH):- !,flatten_clauses(H,HH),!.
 2060flatten_clauses((H,T),HHTT):-!,flatten_clauses(H,HH),flatten_clauses(T,TT),append(HH,TT,HHTT).
 2061flatten_clauses([H],[H]):-!.
 2062
 2063
 2064%=
 correct_cls(?KB, ?H, ?HH) is det
Correct Clauses.
 2070correct_cls(KB,H,HH):-loop_check(correct_cls0(KB,H,HH),H=HH),!.
 2071
 2072
 2073%=
 correct_cls0(?KB, :TermCL0, ?CL1) is det
Correct Clauses Primary Helper.
 2079correct_cls0(_KB,CL0,CL0):- is_ftVar(CL0),!.
 2080correct_cls0(KB,CL0,CL1):- is_list(CL0),!,must_maplist_det(correct_cls(KB),CL0,CL1).
 2081correct_cls0(KB,(H,T),HHTT):-!,correct_cls(KB,H,HH),correct_cls(KB,T,TT),append(HH,TT,HHTT).
 2082correct_cls0(KB,(H:-B),O):-!,conjuncts_to_list_det(H,HH),conjuncts_to_list_det(B,BB),correct_cls0(KB,cl(HH,BB),O).
 2083
 2084correct_cls0(KB,CL,O):- demodal_sents(KB,CL,CLM),CL\=@=CLM,!,correct_cls(KB,CLM,O).
 2085correct_cls0(KB,cl(H,B),O):-flatten_clauses(B,BB),B\=@=BB,correct_cls0(KB,cl(H,BB),O).
 2086correct_cls0(KB,cl(H,B),O):-removeQ(KB,H,HH),removeQ(KB,B,BB),(H\=@=HH ; B\=@=BB),!, correct_cls(KB,cl(HH,BB),O).
 2087
 2088correct_cls0(KB,cl(H,B),O):- member(E,B),removes_literal(E,R),delete_sublits(B,R,BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2089
 2090
 2091
 2092correct_cls0(KB,cl(H,B),O):- list_to_set(H,HH),HH\=@=H,!,correct_cls(KB,cl(HH,B),O).
 2093correct_cls0(KB,cl(H,B),O):- list_to_set(B,BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2094
 2095/*
 2096correct_cls0(_,cl([ ~( poss(H))],B),cl([z_unused(~(poss(H:-B)))],[])):-member( ~( H),B),!.
 2097correct_cls0(KB,cl([ ~( poss(H))],B),O):- correct_cls0(KB,cl([ ~( (H))],B),O).
 2098correct_cls0(KB,cl([ ~( H)],B),O):- delete_sublits(B,poss(H),BB),BB\=@=B,!,correct_cls(KB,cl([ ~( H)],BB),O).
 2099correct_cls0(KB,cl([ ~( H)],B),O):- delete_sublits(B,(H),BB),BB\=@=B,!,correct_cls(KB,cl([ ~( H)],BB),O).
 2100correct_cls0(KB,cl([H],B),O):- delete_sublits(B,H,BB),BB\=@=B,!,correct_cls(KB,cl([H],BB),O).
 2101correct_cls0(KB,cl([H],B),O):- delete_sublits(B, ~( H),BB),BB\=@=B,!,correct_cls(KB,cl([H],BB),O).
 2102
 2103correct_cls0(KB,cl(H,B),O):- member(E,B),E=poss( ~( _)),delete_sublits(B,E,BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2104correct_cls0(KB,cl(H,B),O):- member(E,B),E=nesc( ~( P)),delete_sublits(B,E,BB),BB\=@=B,!,correct_cls(KB,cl(H,[ ~( P)|BB]),O).
 2105correct_cls0(KB,cl(H,B),O):- member(E,B),delete_sublits(B,poss(E),BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2106correct_cls0(KB,cl(H,B),O):- member( ~( E),B),delete_sublits(B,poss(E),BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2107correct_cls0(KB,cl(H,B),O):- member( ~( E),B),delete_sublits(B,E,BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2108correct_cls0(KB,cl(H,B),O):- member(nesc( ~( E)),B),delete_sublits(B,poss(E),BB),BB\=@=B,!,correct_cls(KB,cl(H,BB),O).
 2109
 2110% correct_cls0(KB,cl([(poss(H))],B),O):- correct_cls0(KB,cl([((H))],B),O).
 2111
 2112correct_cls0(_,cl(H,B),O):- member(E,B),member( ~( E),B),!,incorrect_cl(cl(H,B),O).
 2113
 2114correct_cls0(_,cl([nesc((H))],B),cl([z_unused(nesc(H:-B))],[])):-member((H),B),!.
 2115correct_cls0(KB,cl([nesc((H))],B),O):- delete_sublits(B, ~( H),BB),BB\=@=B,!,correct_cls(KB,cl([(H)],BB),O).
 2116correct_cls0(KB,cl([ ~( (H))],B),O):- correct_cls(KB,cl([ ~( poss(H))],B),O).
 2117*/
 2118
 2119correct_cls0(_KB,cl(H,B),O):- !,O=cl(H,B).
 2120correct_cls0(KB,H,O):-correct_cls0(KB,(H:-true),O).
 2121
 2122
 2123%=
 incorrect_cl(:TermH, ?H) is det
Incorrect Clause.
 2129incorrect_cl(cl(H,B),cl([z_unused(H:-B)],[])).
 2130
 2131
 2132
 2133:- was_export(correct_boxlog/4). 2134
 2135%=
 correct_boxlog(?CLAUSES, ?KB, ?Why, ?FlattenedO) is det
Correct Datalog.
 2141interface_to_correct_boxlog(KB,WHY,IN,OUT):- correct_boxlog(IN,KB,WHY,OUT).
 2142
 2143correct_boxlog((CLAU,SES),KB,Why,FlattenedO):- nonvar(SES),conjuncts_to_list_det((CLAU,SES),CLAUSES),!,correct_boxlog_0(CLAUSES,KB,Why,FlattenedO),!.
 2144correct_boxlog(CLAUSES,KB,Why,FlattenedO):- (\+ is_list(CLAUSES)),!,correct_boxlog_0([CLAUSES],KB,Why,FlattenedO),!.
 2145correct_boxlog(BOXLOG,KB,Why,FlattenedS):-correct_boxlog_0(BOXLOG,KB,Why,FlattenedS),!.
 2146
 2147
 2148%=
 correct_boxlog_0(?BOXLOG, ?KB, ?Why, ?FlattenedS) is det
correct Datalog Primary Helper.
 2154correct_boxlog_0(BOXLOG,KB,Why,FlattenedS):-
 2155  must_det_l((  
 2156   must_maplist_det(adjust_kif(KB),BOXLOG,MODAL),
 2157   %sdmsg(modal=(MODAL)),   
 2158   must_maplist_det(to_modal1(KB),MODAL,CLAUSES),
 2159   must_maplist_det(correct_cls(KB),CLAUSES,NCFs),
 2160   must_maplist_det(clauses_to_boxlog(KB,Why),NCFs,ListOfLists),
 2161   flatten([ListOfLists],Flattened),
 2162   must_maplist_det(removeQ(KB),Flattened,FlattenedM),
 2163   must_maplist_det(to_modal1(KB),FlattenedM,FlattenedO),
 2164   predsort(variants_are_equal,FlattenedO,FlattenedS),
 2165   nop(sdmsg(horn=(FlattenedS))))),!.
 2166
 2167
 2168%=
 variants_are_equal(?Order, ?A, ?B) is det
Variants Are Equal.
 2174variants_are_equal( =, A,B):- unnumbervars(A+B,AA+BB),AA=@=BB,!.
 2175variants_are_equal( Order, A,B):- compare(Order,A,B).
 variants_are_equal(?Order, ?A, ?B) is det
Variants Are Equal.
 2182sort_by_pred_class( <, '$unused'(_),B):- B\='$unused'(_),!.
 2183sort_by_pred_class( >, B, '$unused'(_)):- B\='$unused'(_),!.
 2184sort_by_pred_class( <, proven_neg(_),B):- B\=proven_neg(_),!.
 2185sort_by_pred_class( >, B, proven_neg(_)):- B\=proven_neg(_),!.
 2186sort_by_pred_class( =, A,B):- unnumbervars(A+B,AA+BB),AA=@=BB,!.
 2187sort_by_pred_class( Op, (A:-_), B):-sort_by_pred_class( Op, A,B), Op \== (=),!.
 2188sort_by_pred_class( Op, A, (B:-_)):-!,sort_by_pred_class( Op, A,B), Op \== (=),!.
 2189sort_by_pred_class( Order, A,B):- compare(Order,A,B).
 2190
 2191
 2192%=
 cf_to_flattened_clauses(?KB, ?Why, ?NCFsI, ?FlattenedO) is det
Cf Converted To Flattened Clauses.
 2198cf_to_flattened_clauses(KB,Why,NCFsI,FlattenedO):-
 2199  loop_check(cf_to_flattened_clauses_0(KB,Why,NCFsI,FlattenedO),NCFsI=FlattenedO),!.
 2200
 2201
 2202%=
 cf_to_flattened_clauses_0(?KB, ?Why, ?NCFsI, ?FlattenedO) is det
cf Converted To flattened clauses Primary Helper.
 2208cf_to_flattened_clauses_0(KB,Why,NCFsI,FlattenedO):- 
 2209 must_det_l((
 2210   must_maplist_det(correct_cls(KB),NCFsI,NCFs),
 2211   % sdmsg(cf=(NCFs)),
 2212   must_maplist_det(clauses_to_boxlog(KB,Why),NCFs,ListOfLists),
 2213   flatten([ListOfLists],Flattened),
 2214   baseKB:as_prolog_hook(Flattened,FlattenedL),
 2215   list_to_set(FlattenedL,FlattenedS),
 2216   must_maplist_det(demodal_sents(KB),FlattenedS,FlattenedO))),!.
 2217  
 2218% :- autoload([verbose(false)]).
 2219
 2220:- fixup_exports.