1% File: /opt/PrologMUD/pack/logicmoo_base/prolog/common_logic/snark/common_logic_snark.pl 2% :- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )). 3:- module(common_logic_snark, 4 [ 5 6 % op(300,fx,'-'), 7 /*op(1150,xfx,'=>'), 8 op(1150,xfx,'<=>'), 9 op(350,xfx,'xor'), 10 op(400,yfx,'&'), 11 op(500,yfx,'v')*/ 12 % if/2,iif/2, 13 is_not_entailed/1]).
25:- meta_predicate call_l2r(,,). 26 27 28:- reexport(library('logicmoo/common_logic/common_logic_boxlog.pl')). 29:- user:reexport(library('logicmoo_pttp')). 30 31 32 33 34:- include(library('logicmoo/common_logic/common_header.pi')). 35%:- endif. 36 37:- 38 op(1150,fx,(was_dynamic)), 39 op(1150,fx,(was_multifile)), 40 op(1150,fy,(was_module_transparent)). 41 42:- load_library_system(library(logicmoo_typesystem)). 43 44:- set_how_virtualize_file(bodies). 45 46:- system:(( 47 op(1199,fx,('==>')), 48 op(1190,xfx,('::::')), 49 op(1180,xfx,('==>')), 50 op(1170,xfx,'<==>'), 51 op(1160,xfx,('<-')), 52 op(1150,xfx,'=>'), 53 op(1140,xfx,'<='), 54 op(1130,xfx,'<=>'), 55 op(600,yfx,'&'), 56 op(600,yfx,'v'), 57 op(350,xfx,'xor'), 58 op(300,fx,'~'), 59 op(300,fx,'-'))). 60 61 62:- module_transparent(( are_clauses_entailed/1, 63 is_prolog_entailed/1, 64 delistify_last_arg/3)). 65 66:- meta_predicate 67 % common_logic_snark 68 convertAndCall(,), 69 kif_add_boxes3(,,), 70 % common_logic_snark 71 ain_h(,,), 72 map_each_clause(,), 73 map_each_clause(,,), 74 75 % common_logic_snark 76 to_nonvars(,,). 77 78%:- meta_predicate '__aux_maplist/2_map_each_clause+1'(*,1). 79%:- meta_predicate '__aux_maplist/3_map_each_clause+1'(*,*,2). 80 81 82 83:- thread_local(t_l:kif_option/2). 84:- thread_local(t_l:kif_option_list/1). 85 86kif_value_false(Value):- Value == none ; Value == fail; Value == []; Value == false; Value == no ; Value=todo. 87 88kif_option(never,_Jiggler):-!,fail. 89kif_option(always,_Jiggler):-!. 90kif_option(_Default,Jiggler):- foption_to_name(Jiggler,Name), kif_option_value(Name,Value),!, \+ kif_value_false(Value), 91 (compound(Jiggler) -> arg(1,Jiggler,Value) ; true). 92 93kif_option(Default,_Jiggler):- \+ kif_value_false(Default). 94 95as_local_kv(-Key,Key,false):-!. 96as_local_kv(+Key,Key,true):-!. 97as_local_kv(Key,Key,true):- atom(Key),!. 98as_local_kv(KeyValue,_Key,_):- \+ compound(KeyValue),!,fail. 99as_local_kv(KeyValue,Key,Value):- KeyValue=..[Key,Value]. 100as_local_kv(KeyValue,Key,Value):- KeyValue=..[_,Key,Value]. 101 102set_kif_option(Name+Name2):- !,set_kif_option(Name),set_kif_option(+Name2). 103set_kif_option(Name-Name2):- !,set_kif_option(Name),set_kif_option(-Name2). 104set_kif_option(+Name):- !, set_kif_option(Name,true). 105set_kif_option(-Name):- !, set_kif_option(Name,false). 106set_kif_option(List):- is_list(List),!,maplist(set_kif_option,List). 107set_kif_option(N=V):- !, set_kif_option(N,V). 108set_kif_option(N:V):- !, set_kif_option(N,V). 109set_kif_option(Name,Value):- assert_setting01(t_l:kif_option(Name,Value)),!. 110 111kif_option_value(Name,Value):- zotrace(kif_option_value0(Name,Value)). 112kif_option_value0(Name,Value):- Value==none,!,(kif_option_value(Name,ValueReally)->ValueReally==Value;true). 113kif_option_value0(Name,Value):- t_l:kif_option_list(Dict),atom(Name), 114 (is_dict(Dict) -> (get_dict(Key,Dict,Value),atom(Name),atom(Key),atom_concat(Key,_,Name)); 115 true -> ((member(KeyValue,Dict),as_local_kv(KeyValue,Key,Value),(atom_concat(Key,_,Name);atom_concat(_,Key,Name))))),!. 116kif_option_value0(Name,Value):- t_l:kif_option(Name,Value),!. 117kif_option_value0(Name,Value):- atom(Name),current_prolog_flag(Name,Value),!. 118kif_option_value0(Name,Value):- clause_b(feature_setting(Name,Value)),!. 119 120foption_to_name(Name,Name):- \+ compound(Name),!. 121foption_to_name(_:Jiggler,Name):- !,foption_to_name(Jiggler,Name). 122foption_to_name(adapt_to_arity_2(Jiggler),Name):-!,foption_to_name(Jiggler,Name). 123foption_to_name(Jiggler,Name):-functor(Jiggler,Name,_). 124 125:- meta_predicate adapt_to_arity_2(,,). 126adapt_to_arity_2(Pred1,A,O):- call(Pred1,A),A=O. 127 128:- meta_predicate kif_optionally(,,). 129kif_optionally(YN,Pred1,Arg):- kif_optionally(YN,adapt_to_arity_2(Pred1),Arg,_). 130 131:- meta_predicate kif_optionally(,,,). 132kif_optionally(_,_,JIGGLED,JIGGLED):- JIGGLED==[],!. 133kif_optionally(Default,Jiggler,KIF,JIGGLED):- \+ is_list(KIF),!,kif_optionally_e(Default,Jiggler,KIF,JIGGLED). 134kif_optionally(never,_,JIGGLED,JIGGLED):-!. 135kif_optionally(always,Jiggler,KIF,JIGGLED):- must_maplist_det(Jiggler,KIF,JIGGLED),!. 136kif_optionally(Default,Jiggler,KIF,JIGGLED):- must_maplist_det(kif_optionally_e(Default,Jiggler),KIF,JIGGLED),!. 137 138:- meta_predicate kif_optionally_e(,,). 139kif_optionally_e(YN,Pred1,Arg):- kif_optionally_e(YN,adapt_to_arity_2(Pred1),Arg,_). 140 141:- meta_predicate kif_optionally_e(,,,). 142kif_optionally_e(Default,Jiggler,KIF,JIGGLED):- 143 foption_to_name(Jiggler,Name), !, 144 kif_optionally_e(Default,Name,Jiggler,KIF,JIGGLED). 145 146kif_optionally_e( never ,_ ,_,JIGGLED,JIGGLED):-!. 147kif_optionally_e(Default,Name,Jiggler,KIF,JIGGLED):- 148 (kif_option_value(Name,Value)-> true ; Value = Default), 149 ((kif_value_false(Value), \+ Default==always) -> KIF=JIGGLED ; 150 ((locally_tl(kif_option(Name,Value), 151 must(call(Jiggler,KIF,JIGGLED))), 152 if_debugging2(Name,(KIF \=@= JIGGLED) -> (sdmsg(Name=JIGGLED)); true)))),!. 153 154:- fixup_exports. 155 156/* 157:- was_dynamic 158 baseKB:as_prolog_hook/2, 159 elInverse/2, 160 161 not_mudEquals/2. 162 163*/ 164 165% :- dynamic(baseKB:(if/2,iif/2)). 166 167:- export(kw_to_vars/2). 168kw_to_vars(KW,VARS):-subsT_each(KW,[':ARG1'=_ARG1,':ARG2'=_ARG2,':ARG3'=_ARG3,':ARG4'=_ARG4,':ARG5'=_ARG5,':ARG6'=_ARG6],VARS).
177is_gaf(Gaf):-when(nonvar(Gaf), \+ (is_kif_clause(Gaf))). 178 179%= %= :- was_export(is_kif_clause/1).
187are_clauses_entailed(E):-var(E),!,fail. 188are_clauses_entailed(B):- unnumbervars(B,A),map_each_clause(is_prolog_entailed,A). 189 190 191is_pfc_entailed(B):- unnumbervars(B,A),map_each_clause(mpred_supported(local),A).
199is_prolog_entailed(UCL):-clause_asserted_u(UCL),!. 200is_prolog_entailed(UCL):-show_success(clause_asserted(UCL)),!. 201is_prolog_entailed(UCL):-show_success(clause_asserted_i(UCL)),!. 202is_prolog_entailed(UCL):-boxlog_to_pfc(UCL,PFC),show_failure(is_pfc_entailed(PFC)),!. 203is_prolog_entailed(PFC):-show_failure(is_pfc_entailed(PFC)),!. 204is_prolog_entailed(UCL):-clause(UCL,B),split_attrs(B,A,BB),must(A),. 205is_prolog_entailed(UCL):-clause(UCL,B,Ref),(B\==true->must(B);(dtrace,clause(HH,BB,Ref),dmsg(BB:-(UCL,HH)))),!. 206is_prolog_entailed(UCL):-dmsg(warn(not_is_prolog_entailed(UCL))),!,fail.
214member_ele(E,E):- is_ftVar(E),!. 215member_ele([],_):-!,fail. 216member_ele(E,E):- ( \+ (compound(E))),!. 217member_ele([L|List],E):- must(is_list([L|List])),!,member(EE,[L|List]),member_ele(EE,E). 218member_ele((H,T),E):- nonvar(H),nonvar(T),!, (member_ele(H,E);member_ele(T,E)). 219member_ele(E,E). 220 221 222 223% sanity that mpreds (manage prolog prodicate) are abily to transform 224 225% cwc "code-wise chaining" is always true in Prolog but will throw programming error if evalled in LogicMOO Prover. 226% Use this to mark code and not axiomatic prolog 227 228 229map_each_clause(P,CLIF,Prolog):- is_list(CLIF),!,must_maplist_det(map_each_clause(P),CLIF,Prolog). 230map_each_clause(P,(H,CLIF),(T,Prolog)):- sanity(nonvar(H)),!,map_each_clause(P,H,T),map_each_clause(P,CLIF,Prolog). 231map_each_clause(P,A,B):- call(P,A,B). 232 233map_each_clause(P,CLIF):- is_list(CLIF),!,must_maplist_det(map_each_clause(P),CLIF). 234map_each_clause(P,(H,CLIF)):- sanity(nonvar(H)),!,map_each_clause(P,H),map_each_clause(P,CLIF). 235map_each_clause(P,A):- call(P,A).
241any_to_pfc(B,A):- sumo_to_pdkb(B,B0),must(map_each_clause(any_to_pfc0,B0,A)). 242 243any_to_pfc0(B,A):- is_kif_clause(B),!,maybe_notrace(kif_to_pfc0(B,A)). 244any_to_pfc0(B,A):- is_pfc_clause(B),!,maybe_notrace(fully_expand(clause(any_to_pfc,any_to_pfc),B,A)). 245any_to_pfc0(B,A):- is_prolog_clause(B),!,maybe_notrace(boxlog_to_pfc(B,A)). 246any_to_pfc0(B,A):- maybe_notrace(boxlog_to_pfc(B,A)),!. 247% any_to_pfc0(B,A):- \+ \+ lookup_u(B),!,A=B. 248any_to_pfc0(B,A):- !, trace_or_throw(should_never_be_here(any_to_pfc0(B,A))). 249any_to_pfc0((H:-B),PrologO):- must((show_failure(why,boxlog_to_pfc((H:-B),Prolog)),!,=(Prolog,PrologO))),!.
256kif_to_pfc(B,A):- must(map_each_clause(kif_to_pfc0,B,A)). 257 258kif_to_pfc0(CLIF,Prolog):- 259 sanity(is_kif_clause(CLIF)), 260 % somehow integrate why_to_id(tell,Wff,Why), 261 must_det_l(( 262 kif_to_boxlog(CLIF,BOXLOG), 263 boxlog_to_pfc(BOXLOG,Prolog), 264 (BOXLOG=@=Prolog -> true; (pfc_for_print_left(Prolog,PrintPFC),wdmsg(-PrintPFC))))),!.
272pfc_for_print_left(Prolog,PrintPFC):-is_list(Prolog),!,must_maplist_det(pfc_for_print_left,Prolog,PrintPFC). 273%pfc_for_print_left(==>(P,if_missing(R,Q)),(Q :- (fwc, naf(R), P))):-!. 274%pfc_for_print_left(if_missing(R,Q),(Q :- (fwc, naf(R)))):-!. 275pfc_for_print_left(==>(P,Q),(Q:-fwc, P)):-!. 276pfc_for_print_left(Prolog,PrintPFC):- =(Prolog,PrintPFC).
282pfc_for_print_right(Prolog,PrintPFC):-is_list(Prolog),!,must_maplist_det(pfc_for_print_right,Prolog,PrintPFC). 283pfc_for_print_right('<-'(Q,P),'->'(P, Q)):-!. 284pfc_for_print_right(Prolog,PrintPFC):- =(Prolog,PrintPFC).
294is_entailed_u(CLIF):-
295 mpred_run,
296 mpred_nochaining((
297 must_det(any_to_pfc(CLIF,Prolog)),!,
298 \+ \+ are_clauses_entailed(Prolog))),!.306is_not_entailed(CLIF):- mpred_nochaining((kif_to_boxlog(CLIF,Prolog), 307 \+ are_clauses_entailed(Prolog))). 308 309:- op(1190,xfx,(:-)). 310:- op(1200,fy,(is_entailed_u)). 311 312% this defines a recogniser for clif syntax (well stuff that might be safe to send in thru kif_to_boxlog)
320is_clif(all(_,X)):-compound(X),!. 321is_clif(forall(_,X)):-compound(X),!,is_clif(X). 322is_clif(CLIF):- 323 VVs = v(if,iff,clif_forall,all,exists), % but not: implies,equiv,forall 324 (var(CLIF)-> (arg(_,VVs,F),functor(CLIF,F,2)); 325 compound(CLIF),functor(CLIF,F,2),arg(_,VVs,F)). 326 327 328:- style_check(+singleton).
337correct_arities([],Fml,Fml):-!. 338correct_arities(_,Fml,Fml):- \+ compound(Fml),!. 339correct_arities(_,FmlO,FmlO):-leave_as_is_logically(FmlO),!. 340correct_arities([H|B],Fml,FmlO):-!,correct_arities(H,Fml,FmlM),correct_arities(B,FmlM,FmlO). 341correct_arities(H,Fml,FmlO):- Fml=..[H,A|ARGS], ARGS\=[_], 342 (ARGS==[] -> 343 correct_arities(H,A,FmlO); 344 (correct_arities(H,A,CA), FmlM=..[H|ARGS],correct_arities(H,FmlM,FmlMC),FmlO=..[H,CA,FmlMC])),!. 345correct_arities(H,Fml,FmlM):- Fml=..[F|ARGS],must_maplist_det(correct_arities(H),ARGS,ARGSM),FmlM =.. [F|ARGSM]. 346 347 348:- public(subsT_each/3).
356subsT_each(In,[],In):- !. 357% subsT_each(In,[KV|TODO],Out):- !,get_kv(KV,X,Y),subst_except(In,X,Y,Mid),!,subsT_each(Mid,TODO,Out),!. 358subsT_each(In,[KV|TODO],Out):- quietly(subst_except_l(In,[KV|TODO],Out)),!.
367subst_except_l( Var, List, NVar ) :- nonvar(NVar),!,subst_except_l( Var, List, MVar ),!,must(MVar=NVar). 368subst_except_l( Var, _,Var ) :- is_ftVar(Var),!. 369% subst_except_l( Var, _,Var ) :- leave_as_is_logically(Var),!. 370subst_except_l( N, List,V ) :- memberchk(N=V,List),!. 371subst_except_l( N, List,V ) :- memberchk(N-V,List),!. 372subst_except_l([H|T],List,[HH|TT]):- !, subst_except_l(H,List,HH), subst_except_l(T,List,TT). 373subst_except_l( [], _,[] ) :-!. 374subst_except_l(HT,List,HHTT):- compound(HT), 375 compound_name_arguments(HT,F,ARGS0), 376 subst_except_l([F|ARGS0],List,[FM|MARGS]),!, 377 (atom(FM)->HHTT=..[FM|MARGS];append_termlist(FM,MARGS,HHTT)),!. 378subst_except_l(HT,_List,HT).
388skolem_in_code(X,Y):- ignore(X=Y).396skolem_in_code(X,_,Fml):- when('?='(X,_),skolem_in_code(X,Fml)). 397 398:- public(not_mudEquals/2). 399:- was_dynamic(not_mudEquals/2).
407not_mudEquals(X,Y):- dif:dif(X,Y). 408 409:- public(type_of_var/3).
417type_of_var(Fml,Var,Type):- contains_type_lits(Fml,Var,Lits),!,(member(Type,Lits)*->true;Type='Unk'). 418:- style_check(+singleton).
428to_dlog_ops([
429 '~'='~',
430 'theExists'='exists',
431 'thereExists'='exists',
432 'ex'='exists',
433 'forAll'='all',
434 'forall'='all',
435 ';'='v',
436 ','='&',
437 'neg'='~',
438 % '-'='~',
439
440 'not'='~',
441 '\\+'='~',
442 % '\\+'='naf',
443 'and'='&',
444 '^'='&',
445 '/\\'='&',
446 'or'='v',
447 '\\/'='v',
448 'V'='v',
449 ':-'=':-',
450 'implies'='=>',
451 'if'='=>',
452 'iff'='<=>',
453 'implies_fc'='==>',
454 'implies_bc'='->',
455 'equiv'='<=>',
456 '=>'='=>',
457 '<=>'='<=>']).
466to_symlog_ops([
467 ';'='v',
468 ','='&'
469 %'=>'='=>',
470 %'<=>'='<=>',
471 %'not'='~',
472 %':-'=':-'
473 ]).
482to_prolog_ops([
483 'v'=';',
484 '&'=(',')
485 %'=>'='=>',
486 %'<=>'='<=>',
487 %'~'='~',
488 %'naf'='not',
489 %'naf'='not',
490 %':-'=':-'
491 ]).501to_nonvars(_Type,IN,IN):- is_ftVar(IN),!. 502to_nonvars(_,Fml,Fml):- leave_as_is_logically(Fml),!. 503to_nonvars(Type,IN,OUT):- is_list(IN),!,must_maplist_det(to_nonvars(Type),IN,OUT),!. 504to_nonvars(Type,IN,OUT):- call(Type,IN,OUT),!.
512convertAndCall(Type,Call):- fail,Call=..[F|IN],must_maplist_det(to_nonvars(Type),IN,OUT), IN \=@= OUT, !, must(apply(F,OUT)). 513convertAndCall(_Type,Call):-call_last_is_var(Call).
522as_dlog(Fml,Fml):- leave_as_is_logically(Fml),!. 523as_dlog(Fml,FmlO):- to_dlog_ops(OPS),subsT_each(Fml,OPS,FmlM),!,correct_arities(['v','&'],FmlM,FmlO).
535as_symlog(Fml,Fml):- leave_as_is_logically(Fml),!. 536as_symlog(Fml,FmlO):- quietly((as_dlog(Fml,FmlM),!,to_symlog_ops(OPS),!, 537 subsT_each(FmlM,OPS,FmlM),!,correct_arities(['v','&'],FmlM,FmlO))),!.
546baseKBas_prolog_hook(Fml,Fml):- is_ftVar(Fml),!. 547baseKBas_prolog_hook(Fml,FmlO):- as_symlog(Fml,FmlM), 548 to_prolog_ops(OPS),subsT_each(FmlM,OPS,FmlO).
560adjust_kif(KB,Kif,KifO):- as_dlog(Kif,KifM),maybe_notrace(adjust_kif0(KB,KifM,KifO)),!. 561 562% Converts to syntax that NNF/DNF/CNF/removeQ like
573adjust_kif0(KB,I,O):-nonvar(O),!,adjust_kif0(KB,I,M),!,M=O. 574 575adjust_kif0(_,V,V):- is_ftVar(V),!. 576adjust_kif0(_,A,A):- \+ compound(A),!. 577adjust_kif0(_,A,A):- leave_as_is_logically(A),!. 578 579adjust_kif0(KB,not(Kif),(KifO)):- !,adjust_kif0(KB, ~(Kif),KifO). 580% adjust_kif0(KB,\+(Kif),(KifO)):- !,adjust_kif0(KB, naf(Kif),KifO). 581adjust_kif0(KB,nesc(N,Kif),nesc(N,KifO)):- !,adjust_kif0(KB,Kif,KifO). 582adjust_kif0(KB,poss(N,Kif),poss(N,KifO)):- !,adjust_kif0(KB,Kif,KifO). 583adjust_kif0(KB, ~(Kif), ~(KifO)):- !,adjust_kif0(KB,Kif,KifO). 584adjust_kif0(KB, ~(KB2,Kif), KifO):- KB2==KB,!,adjust_kif0(KB,~(Kif),KifO). 585adjust_kif0(KB,t(Kif),t(KifO)):- !,adjust_kif0(KB,Kif,KifO). 586adjust_kif0(KB,poss(Kif), poss(b_d(KB,nesc,poss),KifO)):- !,adjust_kif0(KB,Kif,KifO). 587adjust_kif0(KB,nesc(Kif), nesc(b_d(KB,nesc,poss),KifO)):- !,adjust_kif0(KB,Kif,KifO). 588 589adjust_kif0(KB,exists(L,Expr), ExprO):-L==[],!,adjust_kif0(KB,Expr,ExprO). 590adjust_kif0(KB,exists(V,Expr), ExprO):-atom(V),svar_fixvarname(V,L),subst(Expr,V,'$VAR'(L),ExprM),!,adjust_kif0(KB,exists('$VAR'(L),ExprM),ExprO). 591% adjust_kif0(KB,exists([L|List],Expr), ExprO):-is_list(List),!,adjust_kif0(KB,exists(L,exists(List,Expr)),ExprO). 592% adjust_kif0(KB,exists(L,Expr), ExprO):- is_ftVar(L), \+ contains_var(L,Expr),!,adjust_kif0(KB,Expr,ExprO). 593adjust_kif0(KB,exists(L,Expr),exists(L,ExprO)):-!,adjust_kif0(KB,Expr,ExprO). 594 595 596adjust_kif0(KB,all(L,Expr), ExprO):-L==[],!,adjust_kif0(KB,Expr,ExprO). 597adjust_kif0(KB,all(V,Expr), ExprO):-atom(V),svar_fixvarname(V,L),subst(Expr,V,'$VAR'(L),ExprM),!,adjust_kif0(KB,all('$VAR'(L),ExprM),ExprO). 598adjust_kif0(KB,all([L|List],Expr),all(L,ExprO)):-is_list(List),!,adjust_kif0(KB,all(List,Expr),ExprO). 599% adjust_kif0(KB,all(L,Expr), ExprO):- \+ contains_var(L,Expr),!,adjust_kif0(KB,Expr,ExprO). 600adjust_kif0(KB,all(L,Expr),all(L,ExprO)):-!,adjust_kif0(KB,Expr,ExprO). 601 602adjust_kif0(KB,(H & B),(HH & ConjO)):- !, adjust_kif(KB,H,HH),adjust_kif(KB,B,ConjO). 603adjust_kif0(KB,(H v B),(HH v ConjO)):- !, adjust_kif(KB,H,HH),adjust_kif(KB,B,ConjO). 604adjust_kif0(KB,'&'([L|Ist]),ConjO):- is_list([L|Ist]),list_to_conjuncts_det('&',[L|Ist],Conj),adjust_kif0(KB,Conj,ConjO). 605adjust_kif0(KB,'v'([L|Ist]),ConjO):- is_list([L|Ist]),list_to_conjuncts_det('v',[L|Ist],Conj),adjust_kif0(KB,Conj,ConjO). 606 607adjust_kif0(KB,[L|Ist],ConjO):- is_list([L|Ist]),!,must_maplist_det(adjust_kif0(KB),[L|Ist],ConjO),!. 608adjust_kif0(KB,(H:-[L|Ist]),(HH:-ConjO)):- nonvar(Ist), adjust_kif(KB,H,HH),is_list([L|Ist]),adjust_kif0(KB,'&'([L|Ist]),ConjO). 609adjust_kif0(KB,(H:-B),(HH:-ConjO)):- !, adjust_kif(KB,H,HH),adjust_kif(KB,B,ConjO). 610 611adjust_kif0(KB,PAB,KifO):- PAB=..[F|AB],must_maplist_det(adjust_kif0(KB),AB,ABO),maybe_notrace(adjust_kif4(KB,F,ABO,KifO)).
620adjust_kif4(KB,call_builtin,ARGS,O):-!,PARGS=..ARGS,adjust_kif0(KB,PARGS,O),!. 621 622adjust_kif4(KB,'v',[F|LIST],O3):- !, adjust_kif0(KB,'v'([F|LIST]),O3). 623adjust_kif4(KB,'&',[F|LIST],O3):- !, adjust_kif0(KB,'&'([F|LIST]),O3). 624 625adjust_kif4(KB,true_t,[F|LIST],O3):-atom(F),!,PARGS=..[F|LIST],adjust_kif0(KB,(PARGS),O3),!. 626adjust_kif4(KB,not_true_t,[F|LIST],O3):-atom(F),!,PARGS=..[F|LIST],adjust_kif0(KB, ~(PARGS),O3),!. 627adjust_kif4(KB,~,[F|LIST],O3):-atom(F),!,PARGS=..[F|LIST],adjust_kif0(KB, ~(PARGS),O3),!. 628 629/* 630adjust_kif4(KB,possible_t,[A],O):-!,adjust_kif0(KB,poss(A),O),!. 631adjust_kif4(KB,possible_t,ARGS,O):-!,PARGS=..ARGS,adjust_kif0(KB,poss(PARGS),O). 632 633% adjust_kif0(KB,asserted_t,[A],O):-!,adjust_kif0(KB,t(A),O),!. 634% adjust_kif0(KB,asserted_t,[A|RGS],O):- atom(A),PARGS=..[A|RGS],!,adjust_kif0(KB,t(PARGS),O). 635 636adjust_kif4(KB,true_t,[A|RGS],O):- atom(A),PARGS=..[A|RGS],adjust_kif0(KB,PARGS,O),!. 637adjust_kif4(KB,Not_P,ARGS,O):-atom_concat('not_',P,Not_P),!,PARGS=..[P|ARGS],adjust_kif0(KB, ~(PARGS),O). 638adjust_kif4(KB,Int_P,ARGS,O):-atom_concat('int_',P,Int_P),!,append(LARGS,[_, _, _, _, _, _, _ ],ARGS), 639 PLARGS=..[P|LARGS],adjust_kif0(KB,PLARGS,O). 640 641adjust_kif4(KB,P,ARGS,O):- fail, atom_concat(_,'_t',P),!,append(LARGS,[_, _, _, _, _, _],ARGS), 642 PARGS=..[P|LARGS],adjust_kif0(KB,PARGS,O). 643*/ 644 645adjust_kif4(KB,W,[P,A,R|GS],O):- call(clause_b(is_wrapper_pred(W))),PARGS=..[P,A,R|GS],adjust_kif0(KB,t(PARGS),O). 646 647adjust_kif4(KB,F,ARGS,O):-KIF=..[F|ARGS],length(ARGS,L),L>2,adjust_kif0(KB,KIF,F,ARGS,Conj),KIF\=@=Conj,!,adjust_kif0(KB,Conj,O). 648% adjust_kif0(KB,W,[A],O):-is_wrapper_pred(W),adjust_kif(KB,A,O),!. 649 650adjust_kif4(_, F,ARGS,P):- P=..[F|ARGS],!.
658adjust_kif0(KB,KIF,OP,ARGS,Conj):-must_maplist_det(adjust_kif(KB),ARGS,ABO),adjust_kif5(KB,KIF,OP,ABO,Conj).667adjust_kif5(_KB,_KIF,',',ARGS,Conj):- list_to_conjuncts_det('&',ARGS,Conj). 668adjust_kif5( _,_,';',ARGS,Conj):-list_to_conjuncts_det('v',ARGS,Conj). 669adjust_kif5( _,_,'v',ARGS,Conj):-list_to_conjuncts_det('v',ARGS,Conj). 670adjust_kif5( _,_,'&',ARGS,Conj):-list_to_conjuncts_det('&',ARGS,Conj).
680local_pterm_to_sterm(P,['$VAR'(S)]):- if_defined(mpred_sexp_reader:svar(P,S),fail),!. 681local_pterm_to_sterm(P,['$VAR'(S)]):- if_defined(mpred_sexp_reader:lvar(P,S),fail),!. 682local_pterm_to_sterm(P,[P]):- leave_as_is_logically(P),!. 683local_pterm_to_sterm((H:-P),(H:-S)):-!,local_pterm_to_sterm(P,S),!. 684local_pterm_to_sterm((P=>Q),[implies,PP,=>,QQ]):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ). 685local_pterm_to_sterm((P<=>Q),[equiv,PP,QQ]):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ). 686local_pterm_to_sterm(all(P,Q),[all(PP),QQ]):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ). 687local_pterm_to_sterm(exists(P,Q),[ex(PP),QQ]):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ). 688local_pterm_to_sterm( ~(Q),[not,QQ]):-local_pterm_to_sterm(Q,QQ). 689local_pterm_to_sterm(poss(Q),[poss(QQ)]):-local_pterm_to_sterm(Q,QQ). 690local_pterm_to_sterm('&'(P,Q),PPQQ):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ),flatten([PP,QQ],PPQQ0),list_to_set(PPQQ0,PPQQ). 691local_pterm_to_sterm(','(P,Q),PPQQ):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ),flatten([PP,QQ],PPQQ0),list_to_set(PPQQ0,PPQQ). 692local_pterm_to_sterm('v'(P,Q),[or,[PP],[QQ]]):-local_pterm_to_sterm(P,PP),local_pterm_to_sterm(Q,QQ),!. 693local_pterm_to_sterm('beliefs'(P,Q),[beliefs(PP),QQ]):-local_pterm_to_sterm2(P,PP),local_pterm_to_sterm(Q,QQ),!. 694local_pterm_to_sterm(P,S):-subst_except(P,'&',',',Q),P\=@=Q,!,local_pterm_to_sterm(Q,S),!. 695local_pterm_to_sterm(P,S):-subst_except(P,'v',';',Q),P\=@=Q,!,local_pterm_to_sterm(Q,S),!. 696local_pterm_to_sterm(P,[Q]):-P=..[F|ARGS],must_maplist_det(local_pterm_to_sterm2,ARGS,QARGS),Q=..[F|QARGS]. 697local_pterm_to_sterm(P,[P]).
706local_pterm_to_sterm2(P,Q):-local_pterm_to_sterm(P,PP),([Q]=PP;Q=PP),!. 707 708 709 710 711 712 713%====== make a sequence out of a disjunction =====
721flatten_or_list(A,B,C):- convertAndCall(as_symlog,flatten_or_list(A,B,C)). 722flatten_or_list(KB,v(X , Y), F):- !, 723 flatten_or_list(KB,X,A), 724 flatten_or_list(KB,Y,B), 725 flatten([A,B],F). 726flatten_or_list(_KB,X,[X]).
737fmtl(X):- baseKB:as_prolog_hook(X,XX), fmt(XX).746write_list([F|R]):- write(F), write('.'), nl, write_list(R). 747write_list([]).
757% unnumbervars_with_names(X,X):-!. 758% unnumbervars_with_names(Term,CTerm):- ground(Term),!,dupe_term(Term,CTerm). 759unnumbervars_with_names(Term,CTerm):- show_failure(quietly(unnumbervars(Term,CTerm))),!. 760 761unnumbervars_with_names(Term,CTerm):- break, 762 must_det_l(( 763 source_variables_l(NamedVars), 764 copy_term(Term:NamedVars,CTerm:CNamedVars), 765 b_implode_varnames0(CNamedVars))),!. 766 767 768unnumbervars_with_names(Term,CTerm):- 769 must_det_l(( 770 source_variables_l(NamedVars), 771 copy_term(Term:NamedVars,CTerm:CNamedVars), 772 term_variables(CTerm,Vars), 773 call((dtrace,get_var_names(Vars,CNamedVars,Names))), 774 b_implode_varnames0(Names), 775 % numbervars(CTerm,91,_,[attvar(skip),singletons(false)]), 776 append(CNamedVars,NamedVars,NewCNamedVars), 777 list_to_set(NewCNamedVars,NewCNamedVarsS), 778 remove_grounds(NewCNamedVarsS,NewCNamedVarsSG), 779 put_variable_names(NewCNamedVarsSG))),!. 780 781 782unnumbervars_with_names_best2(Term,CTerm):- 783 must_det_l(( 784 source_variables_l(NamedVars),!, 785 copy_term(Term:NamedVars,CTerm:CNamedVars), 786 term_variables(CTerm,Vars), 787 get_var_names(Vars,CNamedVars,Names), 788 b_implode_varnames0(Names), 789 % numbervars(CTerm,91,_,[attvar(skip),singletons(false)]), 790 append(CNamedVars,NamedVars,NewCNamedVars), 791 list_to_set(NewCNamedVars,NewCNamedVarsS), 792 remove_grounds(NewCNamedVarsS,NewCNamedVarsSG), 793 put_variable_names(NewCNamedVarsSG))),!.
802get_var_names([],_,[]). 803get_var_names([V|Vars],NamedVars,[S|SNames]):- 804 get_1_var_name(V,NamedVars,S), 805 get_var_names(Vars,NamedVars,SNames).
814get_1_var_name(_V,[],_S). 815 816get_1_var_name(Var,NamedVars,Name):- compound(Var),arg(1,Var,NV),!,get_1_var_name(NV,NamedVars,Name). 817get_1_var_name(Var,NamedVars,Var=NV):-atom(Var),NamedVars=[_|T],nb_setarg(2,NamedVars,[Var=NV|T]),!. 818get_1_var_name(Var,[N=V|_NamedVars],Name=V):- 819 (Var == V -> Name = N ; (Var==Name -> Name=Var ; fail )),!. 820get_1_var_name(Var,[_|NamedVars],Name):- get_1_var_name(Var,NamedVars,Name). 821 822 823 824call_l2r(P,X,Y):- var(X) -> freeze(X,call_l2r(P,X,Y)) ; (call(P,X,Z),Y=Z).
====== kif_to_boxlog(+Wff,-NormalClauses):-
832:- public(kif_to_boxlog/2).838kif_to_boxlog(Wff,Out):- Wff\=(_:-_), why_to_id(rule,Wff,Why),!,must(kif_to_boxlog(Wff,Out,Why)),!. 839% kif_to_boxlog(Wff,Out):- loop_check(kif_to_boxlog(Wff,Out),Out=looped_kb(Wff)). % kif_to_boxlog('=>'(WffIn,enables(Rule)),'$VAR'('MT2'),complete,Out1), % kif_to_boxlog('=>'(enabled(Rule),WffIn),'$VAR'('KB'),complete,Out).
845:- export(kif_to_boxlog/3). 846kif_to_boxlog(Wff,Out,Why):- Wff\=(_:-_), kif_to_boxlog(Wff,'$VAR'('KB'),Why,Out),!.
853:- export(kif_to_boxlog/4). 854kif_to_boxlog(I,KB,Why,Datalog):- % trace, 855 convert_if_kif_string( I, PTerm), 856 kif_to_boxlog(PTerm,KB,Why,Datalog), !. 857 858kif_to_boxlog(HB,KB,Why,FlattenedO):- 859 sumo_to_pdkb(HB,HB00)-> 860 sumo_to_pdkb(KB,KB00)-> 861 sumo_to_pdkb(Why,Why00)-> 862 unnumbervars_with_names((HB00,KB00,Why00),(HB0,KB0,Why0)),!, 863 with_no_kif_var_coroutines(must(kif_to_boxlog_attvars(HB0,KB0,Why0,FlattenedO))),!. 864 865:- meta_predicate(unless_ignore(,)). 866unless_ignore(A,B):- call(A)->;true. 867 868kif_to_boxlog_attvars(kif(HB),KB,Why,FlattenedO):-!,kif_to_boxlog_attvars(HB,KB,Why,FlattenedO). 869kif_to_boxlog_attvars(clif(HB),KB,Why,FlattenedO):-!,kif_to_boxlog_attvars(HB,KB,Why,FlattenedO). 870 871kif_to_boxlog_attvars(HB,KB,Why,FlattenedO):- compound(HB),HB=(HEAD:- BODY),!, 872 must_det_l(( 873 check_is_kb(KB), 874 conjuncts_to_list_det(HEAD,HEADL), 875 conjuncts_to_list_det(BODY,BODYL), 876 finish_clausify([cl(HEADL,BODYL)],KB,Why,FlattenedO))),!. 877 878kif_to_boxlog_attvars(WffIn0,KB0,Why0,RealOUT):- 879 flag(skolem_count,_,0), 880 must_maplist_det(must_det,[ 881 must_be_unqualified(WffIn0), 882 unnumbervars_with_names(WffIn0:KB0:Why0,WffIn:KB:Why), 883 check_is_kb(KB), 884 as_dlog(WffIn,DLOGKIF),!, 885 guess_varnames(DLOGKIF), 886 sdmsg(kif=(DLOGKIF)), 887 kif_optionally_e(false,existentialize_objs,DLOGKIF,EXTOBJ), 888 kif_optionally_e(false,existentialize_rels,EXTOBJ,EXT), 889 kif_optionally_e(true,ensure_quantifiers,EXT,OuterQuantKIF), 890 un_quant3(KB,OuterQuantKIF,NormalOuterQuantKIF), 891 kif_optionally_e(false,rejiggle_quants(KB),NormalOuterQuantKIF,FullQuant), 892 kif_optionally_e(todo,qualify_modality,FullQuant,ModalKIF), 893 adjust_kif(KB,ModalKIF,ModalKBKIF), 894 b_setval('$nnf_outermost',FullQuant), 895 kif_optionally_e(true,nnf(KB),ModalKBKIF,NNF), 896 term_attvars(NNF,NNFVs), maplist(del_attr_type(skv),NNFVs), 897 sanity(NNF \== poss(~t)), 898 % sdmsg(nnf=(NNF)), 899 % save_wid(Why,kif,DLOGKIF), 900 % save_wid(Why,pkif,FullQuant), 901 removeQ(KB,NNF,[], UnQ), 902 unless_ignore(NNF\==UnQ, sdmsg(unq=UnQ)), 903 must(kif_to_boxlog_theorist(FullQuant,UnQ,KB,Why,RealOUT))]),!. 904 905kif_to_boxlog_theorist2(Original,THIN,KB,Why,RealOUT):- 906 demodal_clauses(KB,THIN,THIN2), 907 as_prolog_hook(THIN2,THIN3), 908 must(cf(Why,KB,Original,THIN3,RealOUT)),!. 909 910kif_to_boxlog_theorist(_Wff666,UnQ,KB,Why,RealOUT):- 911 must_maplist_det(call,[ 912 current_outer_modal_t(HOLDS_T), 913 % true cause poss loss 914 kif_optionally_e(false,to_tlog(HOLDS_T,KB),UnQ,UnQ666), 915 as_prolog_hook(UnQ666,THIN0), 916 with_no_dmsg(kif_optionally_e(always,to_tnot,THIN0,THIN)), 917 must_be_unqualified(THIN), 918 % unless_ignore(THIN\==UnQ, sdmsg(tlog_nnf_in=THIN)), 919 with_no_dmsg(kif_optionally_e(always,tlog_nnf(even),THIN,RULIFY)), 920 unless_ignore(THIN\== ~ RULIFY,((as_dlog(RULIFY,DRULIFY), sdmsg(tlog_nnf_out_negated= DRULIFY)))), 921 % trace, 922 once((rulify(constraint,RULIFY,SideEffectsList),SideEffectsList\==[])), 923 list_to_set(SideEffectsList,SetList), 924 finish_clausify(KB,Why,SetList,RealOUT)]). 925 926tlog_nnf(Even,THIN,RULIFY):- th_nnf(THIN,Even,RULIFY). 927 928 929/* 930finish_clausify(KB,Why,Datalog,FlattenedO):- 931 set_prolog_flag(gc,true), 932 (current_prolog_flag(runtime_breaks,3)-> 933 zotrace(kif_optionally_e(true,interface_to_correct_boxlog(KB,Why),Datalog,DatalogT)); 934 kif_optionally_e(true,interface_to_correct_boxlog(KB,Why),Datalog,DatalogT)), 935 demodal_clauses(KB,DatalogT,FlattenedO),!. 936*/ 937 938finish_clausify(KB,Why,Datalog,RealOUT):- 939 locally(set_prolog_flag(dmsg_level,never), 940 ((must_maplist_det(call,[ 941 kif_optionally_e(true,from_tlog,Datalog,Datalog11), 942 kif_optionally_e(false,interface_to_correct_boxlog(KB,Why),Datalog11,Datalog1), 943 kif_optionally_e(true,demodal_clauses(KB),Datalog1,Datalog12), 944 kif_optionally_e(true,remove_unused_clauses,Datalog12,Datalog2), 945 kif_optionally(false,defunctionalize_each,Datalog2,Datalog3), 946 predsort(sort_by_pred_class,Datalog3,Datalog4), 947 kif_optionally(false,vbody_sort,Datalog4,Datalog5), 948 kif_optionally(false,demodal_clauses(KB),Datalog5,Datalog6), 949 kif_optionally_e(true,combine_clauses_with_disjuncts,Datalog6,Datalog7), 950 kif_optionally_e(true,demodal_clauses(KB),Datalog7,Datalog8), 951 kif_optionally(false,kb_ify(KB),Datalog8,RealOUT)])))),!. 952 953 954 955 956is_4th_order(F):- atom_concat('never_',_,F). 957is_4th_order(F):- atom_concat('prove',_,F). 958is_4th_order(F):- atom_concat('call_',_,F). 959is_4th_order(F):- atom_concat('with_',_,F). 960is_4th_order(F):- atom_concat('fals',_,F). 961is_4th_order(F):- atom_concat(_,'neg',F). 962is_4th_order(F):- atom_concat(_,'nesc',F). 963is_4th_order(F):- atom_concat(_,'dom',F). 964is_4th_order(F):- atom_concat(_,'xdoms',F). 965is_4th_order(F):- atom_concat(_,'serted',F). 966is_4th_order(F):- atom_concat(_,'_mu',F). 967is_4th_order(F):- atom_concat(_,'_i',F). 968is_4th_order(F):- atom_concat(_,'_u',F). 969is_4th_order(make_existential). 970is_4th_order(ist). 971is_4th_order(F):-is_2nd_order_holds(F). 972 973 974:- fixup_exports. 975 976kb_ify(_,FlattenedOUT,FlattenedOUT):- \+ compound(FlattenedOUT),!. 977kb_ify(_,ist(KB,H),ist(KB,H)):-!. 978kb_ify(_KB,skolem(X,SK),skolem(X,SK)). 979kb_ify(_KB,make_existential(X,SK),make_existential(X,SK)). 980 981kb_ify(KB,H,HH):- H=..[F,ARG1,ARG2|ARGS],is_4th_order(F),HH=..[F,ARG1,ARG2,KB|ARGS],!. 982kb_ify(KB,H,HH):- H=..[F,ARG1],is_4th_order(F),HH=..[F,KB,ARG1],!. 983 984kb_ify(KB,H,HH ):- H=..[F|ARGS],tlog_is_sentence_functor(F),!,must_maplist_det(kb_ify(KB),ARGS,ARGSO),!,HH=..[F|ARGSO]. 985kb_ify(KB,FlattenedOUT,FlattenedOUT):- contains_var(KB,FlattenedOUT),!. 986 987kb_ify(KB,H,ist(KB,HH)):- H=..[F|ARGS],!,must_maplist_det(kb_ify(KB),ARGS,ARGSO),!,HH=..[F|ARGSO]. 988kb_ify(_KB, (G), (G)):- !. 989 990 991:- meta_predicate(to_tlog(,,,)). 992:- meta_predicate(to_tlog_lit(,,,,)). 993 994to_tlog(args,_KB,Var, Var):-!. % for now 995to_tlog(_,_KB,Var, Var):- quietly(leave_as_is_logically(Var)),!. 996to_tlog(MD,KB,M:H,M:HH):- !, to_tlog(MD,KB,H,HH). 997to_tlog(MD,KB,[H|T],[HH|TT]):- !, to_tlog(MD,KB,H,HH),to_tlog(MD,KB,T,TT). 998 999 1000to_tlog(MD,KB, quant(Q,X,F1), quant(Q,X,F2)):- !, to_tlog(MD,KB,F1,F2). 1001to_tlog(MD,KB, nesc(b_d(KB2,X,_),F), HH):- atom(X),KB\=KB2,XF =..[X,KB2,F],!,to_tlog(MD,KB2,XF, HH). 1002to_tlog(MD,KB, poss(b_d(KB2,_,X),F), HH):- atom(X),KB\=KB2,XF =..[X,KB2,F],!,to_tlog(MD,KB2,XF, HH). 1003to_tlog(MD,KB, nesc(b_d(KB,X,_),F), HH):- atom(X), XF =..[X,F], !,to_tlog(MD,KB,XF, HH). 1004to_tlog(MD,KB, poss(b_d(KB,_,X),F), HH):- atom(X), XF =..[X,F], !,to_tlog(MD,KB,XF, HH). 1005to_tlog(MD,KB, nesc(_,F), HH):- XF =..[nesc,F], !,to_tlog(MD,KB,XF, HH). 1006to_tlog(MD,KB, poss(_,F), HH):- XF =..[poss,F], !,to_tlog(MD,KB,XF, HH). 1007 1008 1009to_tlog(_,KB, poss(F), poss( HH)):-!, to_tlog(poss,KB,F, HH). 1010 1011to_tlog(MD,KB,(X ; Y),(Xp v Yp)) :- to_tlog(MD,KB,X,Xp), to_tlog(MD,KB,Y,Yp). 1012to_tlog(MD,KB,(X v Y),(Xp v Yp)) :- to_tlog(MD,KB,X,Xp), to_tlog(MD,KB,Y,Yp). 1013to_tlog(MD,KB,H,HH ):- H=..[F|ARGS],tlog_is_sentence_functor(F),!,must_maplist_det(to_tlog(MD,KB),ARGS,ARGSO),!,HH=..[F|ARGSO]. 1014to_tlog(MD,KB, ~(XF), n(HH)):- !,to_tlog(MD,KB,XF, HH). 1015to_tlog(MD,KB, n(XF), n(HH)):- !,to_tlog(MD,KB,XF, HH). 1016to_tlog(MD,KB, neg(XF), n(HH)):- !,to_tlog(MD,KB,XF, HH). 1017to_tlog(MD,KB, nesc(_,XF),(HH)):- !,to_tlog(MD,KB,XF, HH). 1018to_tlog(MD,KB, nesc(XF),(HH)):- !,to_tlog(MD,KB,XF, HH). 1019 1020to_tlog(MD,KB,H,HH ):- H=..[F|ARGS],is_quantifier(F),!, 1021 append(Left,[XF],ARGS), to_tlog(MD,KB, XF, XFF), 1022 append(Left,[XFF],ARGSO), HH=..[XFF|ARGSO]. 1023 1024to_tlog(_,KB,H,HH ):- H=..[F,ARG],is_holds_functor(F),!,(is_ftVar(ARG)->HH=H;to_tlog(F,KB,ARG,HH)). 1025to_tlog(_,KB, poss(XF), HH):- !, to_tlog(poss_t,KB, XF, HH). 1026to_tlog(_,KB,H,HH):- H=..[F,ARG],to_tlog(args,KB,ARG,ARGO),HH=..[F,ARGO],!. 1027to_tlog(MD,KB,H,HH):- H=..[F|ARGS],must_maplist_det(to_tlog(args,KB),ARGS,ARGSO),to_tlog_lit(MD,KB,F,ARGSO,HH). 1028 1029tlog_is_sentence_functor(F):- \+ atom(F),!,fail. 1030tlog_is_sentence_functor(F):- upcase_atom(F,F). 1031tlog_is_sentence_functor(F):- is_sentence_functor(F), \+ is_holds_functor(F). 1032 1033to_tlog_lit(MD,KB,F,[ARG],HH):- (clause_b(ttExpressionType(F));atom_concat(ft,_,F)),!,to_tlog(MD,KB,quotedIsa(ARG,F ),HH). 1034to_tlog_lit(MD,KB,F,[ARG],HH):- (clause_b(tSet(F));(atom_concat(t,_,F), \+ atom_concat(_,'_t',F))),!,to_tlog(MD,KB,isa(ARG,F ),HH). 1035to_tlog_lit(MD,_ ,F,ARGSO,HHH):- is_holds_functor(F),!,HH=..[F|ARGSO],maybe_wrap_modal(MD,HH,HHH). 1036to_tlog_lit(MD,_ ,F,ARGSO,HHH):- get_holds_wrapper(F,W),(W==h;W==c),!,HH=..[F|ARGSO],maybe_wrap_modal(MD,HH,HHH). 1037to_tlog_lit(MD,_ ,F,ARGSO,HHH):- get_holds_wrapper(F,W),!,XF=..[F|ARGSO],into_ff(W,XF,HH),maybe_wrap_modal(MD,HH,HHH). 1038to_tlog_lit(MD,_ ,F,ARGSO,HHH):- XF=..[F|ARGSO],into_ff(MD,XF,HHH). 1039 1040into_ff(MD,XF,HHH):-into_functor_form(MD,XF,HHH). 1041 1042current_outer_modal_t(t). 1043 1044maybe_wrap_modal(MD,HH,HH):- current_outer_modal_t(H_T),MD==H_T,!. 1045maybe_wrap_modal(MD,HH,HHH):- var_or_atomic(HH),HHH=..[MD,HH],!. 1046maybe_wrap_modal(MD,M:HH,M:HHH):-!,maybe_wrap_modal(MD,HH,HHH). 1047maybe_wrap_modal(MD,HH,HH):- functor(HH,MD,_). 1048maybe_wrap_modal(MD,HH,HHH):- HH=..[F|_],get_holds_wrapper(F,W),W==h,HHH=..[MD,HH]. 1049maybe_wrap_modal(MD,HH,HHH):- HH=..[F|ARGS],get_holds_wrapper(F,W),W==c,atomic_list_concat([F,'_',MD],MF),HHH=..[MF|ARGS]. 1050maybe_wrap_modal(MD,HH,HHH):- HH=..[F|ARGS],is_holds_functor(F),atom_concat(MD,F,MF),HHH=..[MF|ARGS]. 1051maybe_wrap_modal(MD,HH,HHH):-HHH=..[MD,HH]. 1052 1053 1054% get_holds_wrapper(isa,c). 1055get_holds_wrapper(isa,c). 1056get_holds_wrapper(arity,c). 1057get_holds_wrapper(reify,c). 1058get_holds_wrapper(skolem,c). 1059get_holds_wrapper(quotedIsa,c). 1060get_holds_wrapper(resultIsa,c). 1061get_holds_wrapper(quotedArgIsa,c). 1062get_holds_wrapper(ISA,c):- if_defined(tinyKB(isa(ISA,_)),fail). 1063get_holds_wrapper(IST,c):- atom_contains(IST,ist). % relationAllExists ist etc 1064get_holds_wrapper(IST,c):- atom_contains(IST,ist). 1065get_holds_wrapper(genls,c). 1066get_holds_wrapper(admittedArgument,c). 1067get_holds_wrapper(argIsa,c). 1068get_holds_wrapper(disjointWith,c). 1069%get_holds_wrapper(_,_):-!,fail. 1070%get_holds_wrapper(_P,t). 1071 1072to_tnot(THIN,THIN):- \+ compound(THIN),!. 1073to_tnot(~ THIN0,NTHIN):- to_tnot( THIN0, THIN),!,to_neg(THIN,NTHIN). 1074to_tnot(poss_t(C,I),POSCI):- atom(C),CI=..[C,I],!,to_poss(CI,POSCI). 1075to_tnot(poss(THIN0),NTHIN):- to_poss( THIN0, NTHIN),!. 1076to_tnot(nesc(THIN0),(NTHIN)):- to_tnot( THIN0, NTHIN),!. 1077to_tnot((X ; Y),(Xp ; Yp)) :- to_tnot(X,Xp), to_tnot(Y,Yp). 1078to_tnot((X :- Y),(Xp :- Yp)) :- to_tnot(X,Xp), to_tnot(Y,Yp). 1079to_tnot((X , Y),(Xp , Yp)) :- to_tnot(X,Xp), to_tnot(Y,Yp). 1080to_tnot(THIN0,nesc(THIN)):- into_mpred_form(THIN0,THIN). 1081 1082to_neg(THIN,THIN):- \+ compound(THIN),!. 1083to_neg(neg(THIN),THIN). 1084to_neg(nesc(THIN),neg(THIN)). 1085to_neg(THIN,neg(THIN)). 1086 1087to_poss(THIN,poss(THIN)):- \+ compound(THIN),!. 1088to_poss(poss(THIN),poss(THIN)). 1089to_poss(nesc(THIN),poss(THIN)). 1090to_poss(neg(THIN),poss(neg(THIN))). 1091to_poss(THIN,poss(THIN)).
1099baseKBno_rewrites :- fail. 1100 1101 1102 1103 1104from_tlog(Var, NVar):- \+ compound(Var),!,Var=NVar. 1105from_tlog(Var, Var):- quietly(leave_as_is_logically(Var)),!. 1106from_tlog(M:H,M:HH):- !, from_tlog(H,HH). 1107from_tlog([H|T],[HH|TT]):- !, from_tlog(H,HH),from_tlog(T,TT). 1108from_tlog( t(XF), (HH)):- !,from_tlog(XF, HH). 1109from_tlog( proven_not_holds_t(XF), ~(HH)):- !,from_tlog(XF, HH). 1110from_tlog( proven_not_holds_t(F,A,B), ~(t(F,A,B))):- var(F),!. 1111from_tlog( proven_not_t(XF), ~(HH)):- !,from_tlog(XF, HH). 1112from_tlog( proven_not_t(F,A,B), ~(t(F,A,B))):- var(F),!. 1113from_tlog( proven_t(XF), (HH)):- !,from_tlog(XF, HH). 1114from_tlog( proven_t(F,A,B), (t(F,A,B))):- var(F),!. 1115from_tlog(H,HH):- H=..[F,ARG],is_holds_functor(F),is_ftVar(ARG)->HH=H,!. 1116% from_tlog(H,HH):- H=..[F|ARGS],tlog_is_sentence_functor(F),!,must_maplist_det(from_tlog,ARGS,ARGSO),!,HH=..[F|ARGSO]. 1117% from_tlog(H,HH):- H=..[F|ARGS],must_maplist_det(from_tlog,ARGS,ARGSO),must(from_tlog_lit(F,ARGSO,HH)). 1118from_tlog(H,HH):- H=..[F|ARGS],from_tlog_lit(F,ARGS,HH),!. 1119 1120add_modal(t,HH,HH). 1121add_modal(MD,HH,HHH):- HHH=..[MD,HH]. 1122 1123from_tlog_lit(F,ARGSO,HHH):- F==u,HHH=..[F|ARGSO],!. 1124from_tlog_lit(F,ARGSO,HHH):- \+ is_holds_functor(F),!,HHH=..[F|ARGSO],!. 1125from_tlog_lit(F,ARGSO,HHH):- get_holds_unwrapper(F,MD,W),!,XF=..[W|ARGSO],into_mpred_form(XF,HH),from_tlog(HH,HHHH),add_modal(MD,HHHH,HHH). 1126from_tlog_lit(F,ARGSO,HHH):- XF=..[F|ARGSO],into_mpred_form(XF,HHH). 1127 1128get_holds_unwrapper(F,t,t):- current_outer_modal_t(F). 1129get_holds_unwrapper(FIn,MD,F):- modal_prefix(MDF,MD),atom_concat(MDF,F,FIn). 1130 1131 1132modal_prefix(proven_,t). 1133modal_prefix(holds_,t). 1134modal_prefix(not_,~). 1135modal_prefix(possible_,poss). 1136modal_prefix(poss_,poss). 1137modal_prefix(unknown_,unknown). 1138modal_prefix(false_,~). 1139 1140% PrologMUD is created to correct the mistakes we made in the projects i worked on that we forgot the funding was to create the platform/OS to run Roger Schank''s outlined software and not Doug Lenat''s software. 1141% Additionally to allow it to be taken for granted by current scientists whom were unaware of the breakthroughs we made in those projects due to the fact we where affaid competetors would take our future grant money.
1148check_is_kb(KB):-attvar(KB),!. 1149check_is_kb(KB):-ignore('$VAR'('KB')=KB).
1158add_preconds(X,X):- baseKB:no_rewrites,!. 1159add_preconds(X,Z):- 1160 locally(leave_as_is_db('CollectionS666666666666666ubsetFn'(_,_)), 1161 locally_tl(dont_use_mudEquals,must(defunctionalize('=>',X,Y)))),must(add_preconds2(Y,Z)).
1170add_preconds2(Wff6667,PreCondPOS):-
1171 must_det_l((get_lits(Wff6667,PreCond),list_to_set(PreCond,PreCondS),
1172 add_poss_to(PreCondS,Wff6667, PreCondPOS))).1181get_lits(PQ,[]):- var(PQ),!. 1182get_lits(PQ,QQ):- PQ=..[F,_Vs,Q],is_quantifier(F),get_lits(Q,QQ). 1183get_lits(OuterQuantKIF,[OuterQuantKIF]):-leave_as_is_logically(OuterQuantKIF),!. 1184get_lits( ~(IN),NOUT):-get_lits(IN,OUT),must_maplist_det(simple_negate_literal(not),OUT,NOUT). 1185get_lits(knows(WHO,IN),NOUT):-get_lits(IN,OUT),must_maplist_det(simple_negate_literal(knows(WHO)),OUT,NOUT). 1186get_lits(beliefs(WHO,IN),NOUT):-get_lits(IN,OUT),must_maplist_det(simple_negate_literal(beliefs(WHO)),OUT,NOUT). 1187get_lits(IN,OUTLF):-IN=..[F|INL],logical_functor_pttp(F),!,must_maplist_det(get_lits,INL,OUTL),flatten(OUTL,OUTLF). 1188get_lits(IN,[IN]).
1197simple_negate_literal(F,FX,X):-FX=..FXL,F=..FL,append(FL,[X],FXL),!. 1198simple_negate_literal(F,X,FX):-append_term(F,X,FX).
1206should_be_poss(argInst). 1207 1208% :- was_dynamic(elInverse/2).
1217clauses_to_boxlog(KB,Why,In,Prolog):- clauses_to_boxlog_0(KB,Why,In,Prolog),!.1227clauses_to_boxlog_0(KB,Why,In,Prolog):- 1228 loop_check(clauses_to_boxlog_1(KB,Why,In,Prolog), 1229 show_call(why,(clauses_to_boxlog_5(KB,Why,In,Prolog)))),!. 1230clauses_to_boxlog_0(KB,Why,In,Prolog):-correct_cls(KB,In,Mid),!,clauses_to_boxlog_1(KB,Why,Mid,PrologM),!,Prolog=PrologM.
1239clauses_to_boxlog_1(KB, Why,In,Prolog):- clauses_to_boxlog_2(KB,Why,In,PrologM),!,must(Prolog=PrologM).1248clauses_to_boxlog_2(KB, Why,In,Prolog):- is_list(In),!,must_maplist_det(clauses_to_boxlog_1(KB,Why),In,Prolog). 1249clauses_to_boxlog_2(KB, Why,cl([],BodyIn), Prolog):- !, (is_lit_atom(BodyIn) -> clauses_to_boxlog_1(KB,Why,cl([inconsistentKB(KB)],BodyIn),Prolog); (dtrace,kif_to_boxlog( ~(BodyIn),KB,Why,Prolog))). 1250clauses_to_boxlog_2(KB, Why,cl([HeadIn],[]),Prolog):- !, (is_lit_atom(HeadIn) -> Prolog=HeadIn ; (kif_to_boxlog(HeadIn,KB,Why,Prolog))). 1251clauses_to_boxlog_2(KB,_Why,cl([HeadIn],BodyIn),(HeadIn:- BodyOut)):-!, must_maplist_det(logical_pos(KB),BodyIn,Body), list_to_conjuncts_det(Body,BodyOut),!. 1252 1253clauses_to_boxlog_2(KB, Why,cl([H,Head|List],BodyIn),Prolog):- 1254 findall(Answer,((member(E,[H,Head|List]),delete_eq([H,Head|List],E,RestHead), 1255 must_maplist_det(logical_neg(KB),RestHead,RestHeadS),append(RestHeadS,BodyIn,Body), 1256 clauses_to_boxlog_1(KB,Why,cl([E],Body),Answer))),Prolog),!. 1257 1258clauses_to_boxlog_2(_KB,_Why,(H:-B),(H:-B)):- !.
1267clauses_to_boxlog_5(KB, Why,In,Prolog):- is_list(In),!,must_maplist_det(clauses_to_boxlog_5(KB,Why),In,Prolog). 1268clauses_to_boxlog_5(_KB,_Why,(H:-B),(H:-B)):-!. 1269clauses_to_boxlog_5(_KB,_Why,cl([HeadIn],[]),HeadIn):-!. 1270clauses_to_boxlog_5(_KB,_Why,In,Prolog):-dtrace,In=Prolog.
1281mpred_t_tell_kif(OP2,RULE):- 1282 locally_tl(current_pttp_db_oper(mud_call_store_op(OP2)), 1283 (show_call(why,call((must(kif_add(RULE))))))). 1284 1285 1286:- public(why_to_id/3). 1287 1288 1289 1290:- kb_shared(baseKB:wid/3).
1296why_to_id(Term,Wff,IDWhy):- \+ atom(Term),term_to_atom(Term,Atom),!,why_to_id(Atom,Wff,IDWhy),!. 1297why_to_id(Atom,Wff,IDWhy):- clause_asserted(wid(IDWhy,Atom,Wff)),!. 1298why_to_id(Atom,Wff,IDWhy):- must(atomic(Atom)),gensym(Atom,IDWhyI),kb_incr(IDWhyI,IDWhy), 1299 mpred_ain(wid(IDWhy,Atom,Wff)),!.
1307:- public(kif_ask_sent/1). 1308kif_ask_sent(Wff):- 1309 why_to_id(ask,Wff,Why), 1310 term_variables(Wff,Vars), 1311 gensym(z_q,ZQ), 1312 Query=..[ZQ,666|Vars], 1313 why_to_id(rule,'=>'(Wff,Query),Why), 1314 kif_to_boxlog('=>'(Wff,Query),Why,QueryAsserts),!, 1315 kif_add_boxes1(Why,QueryAsserts),!, 1316 call_cleanup( 1317 kif_ask(Query), 1318 find_and_call(retractall_wid(Why))). 1319 1320 1321:- public(kif_ask/1).
1328kif_ask(Goal0):- call_unwrap(Goal0,Goal),!,kif_ask(Goal). 1329%kif_ask(P <=> Q):- kif_ask_sent(P <=> Q). 1330%kif_ask(P => Q):- kif_ask_sent(P => Q). 1331%kif_ask((P v Q)):- kif_ask_sent(((P v Q))). 1332%kif_ask((P & Q)):- kif_ask_sent((P & Q)). 1333kif_ask((PQ)):- kif_hook_skel(PQ),kif_ask_sent((PQ)). 1334kif_ask(Goal0):- logical_pos(_KB,Goal0,Goal), 1335 no_repeats(baseKB:( 1336 if_defined(add_args(Goal0,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],_ProofOut1,Goal1,_)),!, 1337 call(call,search(Goal1,60,0,1,3,DepthIn,DepthOut)))). 1338 1339:- public(kif_ask/2).
1347kif_ask(Goal0,ProofOut):- logical_pos(_KB,Goal0,Goal), 1348 no_repeats(baseKB:( 1349 if_defined(add_args(Goal0,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],ProofOut1,Goal1,_)),!, 1350 call(call,search(Goal1,60,0,1,3,DepthIn,DepthOut)), 1351 call(call,contract_output_proof(ProofOut1,ProofOut)))). 1352 1353 1354 1355 1356 1357call_unwrap(WffIn,OUT):- call_unwrap0(WffIn,OUT),!,WffIn\==OUT. 1358 1359call_unwrap0(WffIn,WffIn):- is_ftVar(WffIn),!. 1360call_unwrap0(==>WffIn,OUT):-!,call_unwrap0(WffIn,OUT). 1361call_unwrap0(clif(WffIn),OUT):-!,call_unwrap0(WffIn,OUT). 1362call_unwrap0(WffIn,WffIn).
1371local_sterm_to_pterm(Wff,WffO):- sexpr_sterm_to_pterm(Wff,WffO),!. 1372 1373 1374 1375:- op(1000,fy,(kif_add)).
1380kif_add(InS):- 1381 sanity( \+ is_ftVar(InS)), 1382 string(InS),!, 1383 must_det_l(( 1384 input_to_forms(string(InS),Wff,Vs), 1385 nop(b_implode_varnames0(Vs)), 1386 local_sterm_to_pterm(Wff,Wff0))), 1387 InS \== Wff0, 1388 kif_add(Wff0),!. 1389kif_add(Goal0):- call_unwrap(Goal0,Goal),!,kif_add(Goal). 1390kif_add([]). 1391kif_add([H|T]):- !,kif_add(H),kif_add(T). 1392%kif_add((H <- B)):- !, ain((H <- B)). 1393%kif_add((H :- B)):- !, ain((H :- B)). 1394%kif_add((P ==> Q)):- !, ain((P ==> Q)). 1395 1396kif_add(WffIn):- kif_hook(WffIn),!, 1397 test_boxlog(WffIn), 1398 show_call(ain(clif(WffIn))). 1399 1400kif_add(WffIn):- show_call(ain(WffIn)),!. 1401% unnumbervars_with_names(WffIn,Wff), 1402%kif_add(WffIn):- show_call(ain(clif(WffIn))),!. 1403 1404kif_ain(InS):-kif_add(InS). 1405kif_assert(InS):-kif_add(InS). 1406 1407/* 1408:- public((kif_add)/2). 1409 1410kif_add(_,[]). 1411kif_add(Why,[H|T]):- !,must_det_l((kif_add(Why,H),kb_incr(Why,Why2),kif_add(Why2,T))). 1412kif_add(Why,P):- !, mpred_ain(P,Why). 1413kif_add(Why,(H <- B)):- !, mpred_ain((H <- B),Why). 1414%kif_add(Why,(P ==> Q)):- !, ain((P ==> Q),Why). 1415 1416 1417kif_add(Why,Wff):- 1418 must_det_l((kif_to_boxlog(Wff,Why,Asserts), 1419 kif_add_boxes(assert_wfs_def,Why,Wff,Asserts))),!. 1420 1421 1422:- thread_local(t_l:assert_wfs/2). 1423assert_wfs_def(HBINFO,HB):-if_defined(t_l:assert_wfs(HBINFO,HB)),!. 1424assert_wfs_def(Why,H):-assert_wfs_fallback(Why,H). 1425 1426assert_wfs_fallback(Why, HB):- subst(HB,(~),(-),HB2),subst(HB2,(not_proven_t),(not_true_t),HB1),subst(HB1,(poss),(possible_t),HBO),assert_wfs_fallback0(Why, HBO). 1427assert_wfs_fallback0(Why,(H:-B)):- adjust_kif('$VAR'(KB),B,HBK),to_modal1('$VAR'(KB),HBK,HBKD), 1428 wdmsg((H:-w_infer_by(Why),HBKD)),pttp_assert_wid(Why,pttp_in,(H:-B)),!. 1429assert_wfs_fallback0(Why, HB):- adjust_kif('$VAR'(KB),HB,HBK),to_modal1('$VAR'(KB),HBK,HBKD), 1430 wdmsg((HBKD:-w_infer_by(Why))),pttp_assert_wid(Why,pttp_in,(HB)),!. 1431 1432*/ 1433 1434:- public(kb_incr/2).
1442kb_incr(WffNum1 ,WffNum2):-is_ftVar(WffNum1),trace_or_throw(kb_incr(WffNum1 ,WffNum2)). 1443kb_incr(WffNum1 ,WffNum2):-number(WffNum1),WffNum2 is WffNum1 + 1,!. 1444%kb_incr(WffNum1 ,WffNum2):-atom(WffNum1),WffNum2=..[WffNum1,0],!. 1445kb_incr(WffNum1 ,WffNum2):-atomic(WffNum1),WffNum2 = WffNum1:0,!. 1446kb_incr(WffNum1 ,WffNum2):-WffNum1=..[F,P,A|REST],kb_incr(A ,AA),!,WffNum2=..[F,P,AA|REST]. 1447kb_incr(WffNum1 ,WffNum2):-trace_or_throw(kb_incr(WffNum1 ,WffNum2)). 1448/* 1449kif_add_boxes(How,Why,Wff0,Asserts0):- 1450 must_det_l(( 1451 show_failure(why,kif_unnumbervars(Asserts0+Wff0,Asserts+Wff)), 1452 %fully_expand(Get1,Get), 1453 get_constraints(Wff,Isas), 1454 kif_add_adding_constraints(Why,Isas,Asserts))), 1455 findall(HB-WhyHB,retract(t_l:in_code_Buffer(HB,WhyHB,_)),List), 1456 list_to_set(List,Set), 1457 forall(member(HB-WhyHB,Set), 1458 call(How,WhyHB,HB)). 1459*/
1468kif_add_adding_constraints(Why,Isas,Get1Get2):- var(Get1Get2),!,trace_or_throw(var_kif_add_isa_boxes(Why,Isas,Get1Get2)). 1469kif_add_adding_constraints(Why,Isas,(Get1,Get2)):- !,kif_add_adding_constraints(Why,Isas,Get1),kb_incr(Why,Why2),kif_add_adding_constraints(Why2,Isas,Get2). 1470kif_add_adding_constraints(Why,Isas,[Get1|Get2]):- !,kif_add_adding_constraints(Why,Isas,Get1),kb_incr(Why,Why2),kif_add_adding_constraints(Why2,Isas,Get2). 1471kif_add_adding_constraints(_,_,[]). 1472kif_add_adding_constraints(_,_,z_unused(_)):-!. 1473kif_add_adding_constraints(Why,Isas,((H:- B))):- conjoin(Isas,B,BB), kif_add_boxes1(Why,(H:- BB)). 1474kif_add_adding_constraints(Why,Isas,((H))):- kif_add_boxes1(Why,(H:- Isas)).
1483kif_add_boxes1(_,[]). 1484kif_add_boxes1(Why,List):- is_list(List),!,list_to_set(List,[H|T]),must_det_l((kif_add_boxes1(Why,H),kb_incr(Why,Why2),kif_add_boxes1(Why2,T))). 1485kif_add_boxes1(_,z_unused(_)):-!. 1486kif_add_boxes1(Why,AssertI):- must_det_l((simplify_bodies(AssertI,AssertO),kif_add_boxes3(save_wfs,Why,AssertO))). 1487 1488:- thread_local(t_l:in_code_Buffer/3).
1498kif_add_boxes3(How,Why,Assert):-
1499 must_det_l((
1500 boxlog_to_pfc(Assert,Prolog1),
1501 defunctionalize(Prolog1,Prolog2),
1502 kif_unnumbervars(Prolog2,PTTP),
1503 call(How,Why,PTTP))).1512kif_unnumbervars(X,YY):-unnumbervars(X,YY),!. 1513kif_unnumbervars(X,YY):- 1514 must_det_l(( 1515 with_output_to(string(A),write_term(X,[character_escapes(true),ignore_ops(true),quoted(true)])), 1516 atom_to_term(A,Y,NamedVars), 1517 YY=Y, 1518 add_newvars(NamedVars))).
1528simplify_bodies((H:- B),(H:- BC)):- must_det_l((conjuncts_to_list_det(B,RB),simplify_list(_KB,RB,BB),list_to_conjuncts_det(BB,BC))). 1529simplify_bodies((B),(BC)):- must_det_l((conjuncts_to_list_det(B,RB),simplify_list(_KB,RB,BB),list_to_conjuncts_det(BB,BC))).
1539simplify_list(KB,RB,BBS):- list_to_set(RB,BB),must_maplist_det(removeQ(KB),BB,BBO),list_to_set(BBO,BBS).
1548save_wfs(Why,PrologI):-
1549 must_det_l((baseKB:as_prolog_hook(PrologI,Prolog),
1550 \+ \+
1551 ( b_setval('$current_why',wp(Why,Prolog)),
1552 ain_h(save_in_code_buffer,Why,Prolog)))).
1561nots_to(H,To,HH):-subst_except(H,not,To,HH),subst_except(H,-,To,HH),subst_except(H,~,To,HH),subst_except(H, \+ ,To,HH),!.
1569neg_h_if_neg(H,HH):-nots_to(H,'~',HH).
1577neg_b_if_neg(HBINFO,B,BBB):-nots_to(B,'~',BB),sort_body(HBINFO,BB,BBB),!.1584simp_code(HB,(H:-BS)):-expand_to_hb(HB,H,B),conjuncts_to_list_det(B,BL),sort(BL,BS),!. 1585simp_code(A,A).
1595var_count_num(Term,SharedTest,SharedCount,UnsharedCount):- term_slots(Term,Slots),term_slots(SharedTest,TestSlots),
1596 subtract(Slots,TestSlots,UnsharedSlots),
1597 subtract(Slots,UnsharedSlots,SharedSlots),
1598 length(SharedSlots,SharedCount),
1599 length(UnsharedSlots,UnsharedCount).1608ain_h(How,Why,(H:- B)):- neg_h_if_neg(H,HH), neg_b_if_neg((HH:- B),B,BB),!,call(How,Why,(HH:-BB)). 1609ain_h(How,Why,(H)):- neg_h_if_neg(H,HH), call(How,Why,(HH)).
1618save_in_code_buffer(_ ,HB):- simp_code(HB,SIMP),t_l:in_code_Buffer(HB,_,SIMP),!. 1619save_in_code_buffer(Why,HB):- simp_code(HB,SIMP),assert(t_l:in_code_Buffer(HB,Why,SIMP)).
1628use_was_isa_h(_,ftTerm,true):- !. 1629use_was_isa_h(_,argi(mudEquals,_),true):- !. 1630use_was_isa_h(_,argi(skolem,_),true):- !. 1631use_was_isa_h(I,T,ISA):- to_isa_form0(I,T,ISA),!.
1637to_isa_form0(I,C,isa(I,C)). 1638to_isa_form0(I,C,t(C,I)). 1639to_isa_form0(I,C,OUT):- atom(C)->OUT=..[C,I].
1647generate_ante([],[],InOut,InOut). 1648generate_ante([I|VarsA],[T|VarsB],In,Isas):- use_was_isa_h(I,T,ISA), conjoin(In,ISA,Mid),generate_ante(VarsA,VarsB,Mid,Isas).
1657get_constraints(T,true):- T==true. 1658get_constraints(_,true):- !. 1659get_constraints(ListA,Isas):- 1660 must_det_l((copy_term(ListA,ListB), 1661 term_variables(ListA,VarsA), 1662 term_variables(ListB,VarsB), 1663 attempt_attribute_args(isAnd,ftAskable,ListB), 1664 attribs_to_atoms(VarsB,VarsB), 1665 generate_ante(VarsA,VarsB,true,Isas))). 1666 1667 1668 1669:- source_location(S,_),forall((source_file(H,S),once((clause(H,B),B\=true))),(functor(H,F,A),module_transparent(F/A))). 1670 1671 1672:- fixup_exports.
common_logic_snark
% Provides a specific compilation API for KIF axioms %
% Logicmoo Project PrologMUD: A MUD server written in Prolog % Maintainer: Douglas Miles % Dec 13, 2035 % */