API tools faq
paste
Advertisement
logicmoo

Untitled

logicmoo
Jun 10th, 2015
482
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
ZXBasic 53.02 KB | None | 0 0
raw download clone embed print report
  1. /** <module> logicmoo_i_mpred_pttp
  2. % Provides a prolog database replacement that uses an interpretation of SNARK
  3. %
  4. %  t/N
  5. %  hybridRule/2
  6. %  
  7. %
  8. % Logicmoo Project PrologMUD: A MUD server written in Prolog
  9. % Maintainer: Douglas Miles
  10. % Dec 13, 2035
  11. %
  12. */
  13. %= Compute normal forms FOR SHOIQ formulae.
  14. %= Skolemize SHOI<Q> formula.
  15. %=
  16. %= Copyright (C) 1999 Anthony A. Aaby <aabyan@wwc.edu>
  17. %= Copyright (C) 2006-2007 Stasinos Konstantopoulos <stasinos@users.sourceforge.net>
  18. %= Douglas R. Miles <logicmoo@gmail.com>
  19. %=
  20. %= This program is free software; you can redistribute it AND/OR modify
  21. %= it under the terms of the GNU General Public License AS published by
  22. %= the Free Software Foundation; either version 2 of the License, OR
  23. %= (AT your option) any later version.
  24. %=
  25. %= This program is distributed in the hope that it will be useful,
  26. %= but WITHOUT ANY WARRANTY; without even the implied warranty of
  27. %= MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.  See the
  28. %= GNU General Public License FOR more details.
  29. %=
  30. %= You should have received a copy of the GNU General Public License along
  31. %= with this program; IF NOT, write TO the Free Software Foundation, Inc.,
  32. %= 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  33. %=
  34. %= FORMULA SYNTAX
  35. %=
  36. %= n(Neg,A)
  37. %= &(F, F)
  38. %= v(F, F)
  39. %= '=>'(F, F)
  40. %= '<=>'(F, F)
  41. %=    all(X,A)
  42. %=    exists(X,A)
  43. %=    atleast(X,N,A)
  44. %=    atmost(X,N,A)
  45. /*
  46. :- module(logicmoo_i_snark,
  47.           [
  48.            nnf/4,
  49.            pnf/3, pnf/2, cf/4,
  50.           tsn/0,
  51.           op(300,fx,'-'),
  52.           op(600,xfx,'=>'),
  53.           op(600,xfx,'<=>'),
  54.           op(350,xfx,'xor'),
  55.           op(400,yfx,'&'),  
  56.           op(500,yfx,'v')
  57.         ]).
  58. */
  59. :- nodebug(_).
  60.  
  61. %=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%
  62. %=%
  63. %=%   snark_in_prolog.P
  64. %=%      SWI-Prolog version
  65. %=%   Convert wffs TO list of normal logic clauses
  66. %=%
  67. %=%   AND       &  
  68. %=%   OR        v
  69. %=%   NOT       ~
  70. %=%   XOR       XOR
  71. %=%   implies   =>  
  72. %=%   iff       <=>  
  73. %=%   all       all(X,0)
  74. %=%   some      exists(Y,0)
  75. %=%
  76. %=%    all(X,p(X) => exists(Y, r(Y) & q(X,Y)))
  77. %=%  ===============
  78. %=%    p(X) => r(sk1(X)) & q(X,sk1(X))
  79. %=%  ===============
  80. %=%    r(sk1(X)):- p(X).
  81. %=%    q(X,sk1(X)):- p(X).
  82.  
  83.  
  84. :- op(300,fx,'~').
  85. :- op(300,fx,'-').
  86. :- op(400,yfx,'&').  
  87. :- op(500,yfx,'v').
  88. :- op(1075,xfx,'=>').
  89. :- op(1075,xfx,'<=>').
  90. :- op(350,xfx,'xor').
  91.  
  92. :- op(300,fx,user:'~').
  93. :- op(300,fx,user:'-').
  94. :- op(400,yfx,user:'&').  
  95. :- op(500,yfx,user:'v').
  96. :- op(1075,xfx,user:'=>').
  97. :- op(1075,xfx,user:'<=>').
  98. :- op(350,xfx,user:'xor').
  99.  
  100. % SWI Prolog modules DO NOT export operators by default
  101. % so they must be explicitly placed in the user namespace
  102.  
  103. :- dynamic   user:file_search_path/2.
  104. :- multifile user:file_search_path/2.
  105. :- prolog_load_context(directory,Dir),asserta(user:file_search_path(logicmoo,Dir)).
  106. :- dynamic(user:isa_pred_now_locked/0).
  107. :- multifile(user:isa_pred_now_locked/0).
  108.  
  109. :- ensure_loaded(logicmoo(mpred/logicmoo_i_header)).
  110. :- ensure_loaded(library(pttp/dbase_i_mpred_pttp)).
  111.  
  112. %  all(R, room(R) => exists(D, (door(D) & has(R,D))))
  113. % FOR any arbitrary R, IF R is a room THEN there exists some object D that is a door, AND R has a D.
  114. % door(sk6(_G180)):- room(_G180)
  115. % has(_G180,sk6(_G180)):- room(_G180)
  116. %  R is NOT a room IF D is a door AND R doesn't have D
  117. % IF there are no doors anywhere THEN there must NOT be rooms
  118. % - room(R):- - has(R,_).
  119.  
  120. :- %(current_prolog_flag(argv,[pl|_]) -> )
  121.      %op(400, fy, user:(nesc) ),    % Necessity, Always
  122.      %op(400, fy, user:(poss) ),    % Possibly, Eventually
  123.      op(400, fy, user:(cir) ),  % NEXT time
  124.      op(1075,xfx,user:'<-'),
  125.  
  126.  
  127.      %op(400,fy,nesc),      % Necessity, Always
  128.      %op(400,fy,poss),      % Possibly, Eventually
  129.      op(400,fy,cir),        % NEXT time
  130.  
  131.      op(300,fx,'-'),
  132.      op(300,fx,'~'),
  133.      op(1075,xfx,'=>'),
  134.      op(1075,xfx,'<-'),
  135.      op(1075,xfx,'<=>'),
  136.      op(350,xfx,'xor'),
  137.      op(400,yfx,'&'),  
  138.      op(500,yfx,'v')
  139.      ,!.
  140.  
  141. leave_as_is(V):- \+ compound(V),!.
  142. leave_as_is('$VAR'(_)).
  143. leave_as_is(ignore(_)).
  144. leave_as_is(kbMark(_)).
  145.  
  146. kb_nlit(_KB,Neg):-member(Neg,[-,~,neg,NOT]).
  147.  
  148. non_compound(InOut):- once(NOT(compound(InOut));is_ftVar(InOut)).
  149.  
  150. is_gaf(Gaf):- NOT(is_snark_rule(Gaf)).
  151.  
  152. :- export(is_snark_rule/1).
  153. is_snark_rule(Var):- is_ftVar(Var),!,fail.
  154. % is_snark_rule(_:- _):- !.
  155. is_snark_rule(R):- get_functor(R,F,A),functor(P,F,A),snark_hook(P),!.
  156.  
  157. snark_hook(0=>0).
  158. snark_hook(0<=>0).
  159. snark_hook((0 & 0)).
  160. snark_hook((0 v 0)).
  161. snark_hook(0 <- 0).
  162. snark_hook(~(0)).
  163. snark_hook(-(0)).
  164. snark_hook(n(?,0)).
  165. snark_hook(all(+,0)).
  166. snark_hook(exists(+,0)).
  167. snark_hook(C):- non_compound(C),!,fail.
  168. snark_hook(H:- _):- !,nonvar(H),!,snark_hook(H).
  169.  
  170.  
  171. :- style_check(+singleton).
  172.  
  173.  
  174. :- export(term_singletons/2).
  175. term_singletons(A,Vs):- term_singletons(A,[],_,[],Vs).
  176. :- export(term_singletons/5).
  177. term_singletons(Fml, NS,NS, S,S):- atomic(Fml),!.
  178. term_singletons(Fml, NS,NS, S,S):- identical_member(Fml,NS),!.
  179. term_singletons(Fml, NS, [Fml|NS], S, NSV):- is_ftVar(Fml),identical_member(Fml,S),!,delete_eq(S,Fml,NSV),!.
  180. term_singletons(Fml, NS, NS, S, [Fml|S]):- is_ftVar(Fml),!.
  181. term_singletons([H|T],NS,NSO,S,NSV):- !, term_singletons(H,NS,NSM,S,M),term_singletons(T,NSM,NSO,M,NSV).
  182. term_singletons(Fml, NS,NSO, S,NSV):- compound(Fml),Fml=..[_,H|T],!, term_singletons(H,NS,NSM,S,M),term_singletons(T,NSM,NSO, M,NSV).
  183.  
  184. subst_eq(A,B,C,D):- subst(A,B,C,D).
  185.  
  186. get_kv(X=Y,X,Y):- !.
  187. get_kv(KV,X,Y):- functor(KV,_,1),KV=..[X,Y],!.
  188. get_kv(KV,X,Y):- arg(1,KV,X),arg(2,KV,Y),!.
  189.  
  190. :- export(subsT_each/4).
  191. subsT_each(_,In,[],In):- !.
  192. subsT_each(each,In,[KV|TODO],Out):- !,get_kv(KV,X,Y),subst_eq(In,X,Y,Mid),subsT_each(each,Mid,TODO,Out),!.
  193. subsT_each(REV,In,[KV|TODO],Out):- !,get_kv(KV,X,Y),subst_eq(In,Y,X,Mid),subsT_each(REV,Mid,TODO,Out),!.
  194.  
  195. contains_var_lits(Fml,Var,Lits):- findall(Lit,contains_t_var(Fml,Var,Lit),Lits).
  196.  
  197. get_isa(Lit,I,TT):- compound(Lit),get_isa0(Lit,I,TT).
  198. get_isa0(isa(I,T),I,TT):- to_iname(T,TT),!.
  199. get_isa0(IT,I,TT):- IT=..[T,I],is_colection_name(IT,T,TT),!.
  200.  
  201. is_colection_name(_,-,_):- !,fail.
  202. is_colection_name(IT,T,TT):- atom_length(T,TL),TL>2,NOT(atom_contains(T,'_')),not(predicate_property(IT,_)),to_iname(T,TT).
  203.  
  204. :- dynamic(mudEquals/2).
  205. :- export(mudEquals/2).
  206. mudEquals(X,Y):- X=Y.
  207.  
  208. :- export(not_mudEquals/2).
  209. :- dynamic(not_mudEquals/2).
  210. not_mudEquals(X,Y):- X \= Y.
  211.  
  212. contains_type_lits(Fml,Var,Lits):- findall(T,(contains_t_var(Fml,Var,Lit),get_isa(Lit,O,T),same_var(O,Var)),Lits).
  213. contains_t_var(Fml,Var,Term):- each_subterm(Fml,Term),compound(Term),arg(_,Term,O),same_var(O,Var).
  214.  
  215. :- export(type_of_var/3).
  216. type_of_var(Fml,Var,Type):- contains_type_lits(Fml,Var,Lits),!,(member(Type,Lits)*->true;Type='Unk').
  217.  
  218. to_dlog_ops([
  219.        'theExists'='exists',
  220.        'ex'='exists',
  221.        'forAll'='all',
  222.        'forall'='all',
  223.        ';'='v',
  224.        ','='&',
  225.        '~'='-',
  226.      'not'='-',      
  227.      'neg'='-',
  228.      'naf'='-',
  229.      'and'='&',
  230.       'or'='v',
  231.       ':-'=':-',
  232.       '<='=':-',
  233.  'implies'='=>',
  234.  'implies_fc'='=>',
  235.  'implies_bc'=':-',
  236.    'equiv'='<=>',
  237.       '=>'='=>',
  238.      '<=>'='<=>']).
  239.  
  240. to_symlog_ops([
  241.    ';'='v',
  242.    ','='&',
  243.    '=>'='=>',
  244.    '<=>'='<=>',
  245.    '~'='-',
  246.    ':-'=':-']).
  247.  
  248. to_prolog_ops([
  249.    'v'=';',
  250.    '&'=',',  
  251.    '=>'='=>',
  252.    '<=>'='<=>',
  253.    '-'='not',
  254.    ':-'=':-']).
  255.  
  256.  
  257. to_nonvars(_Type,IN,IN):- is_ftVar(IN),!.
  258. to_nonvars(Type,IN,OUT):- is_list(IN),!,maplist(to_nonvars(Type),IN,OUT),!.
  259. to_nonvars(Type,IN,OUT):- call(Type,IN,OUT),!.
  260.  
  261. convertAndCall(Type,Call):- fail, Call=..[F|IN],maplist(to_nonvars(Type),IN,OUT), IN \=@= OUT, !, must(apply(F,OUT)).
  262.  
  263. as_dlog(Fml,Fml):- leave_as_is(Fml),!.
  264. as_dlog(OR(X,Y,Z),FmlO):- !,as_dlog(v(X,v(Y,Z)),FmlO),!.
  265. as_dlog(AND(X,Y,Z),FmlO):- !,as_dlog(&(X,&(Y,Z)),FmlO),!.
  266. as_dlog(Fml,FmlO):- to_dlog_ops(OPS),subsT_each(each,Fml,OPS,FmlO),!.
  267.  
  268. as_symlog(Fml,Fml):- is_ftVar(Fml),!.
  269. as_symlog(Fml,FmlO):- as_dlog(Fml,FmlM),to_symlog_ops(OPS),subsT_each(each,FmlM,OPS,FmlO).
  270.  
  271. :- dynamic(thglobal:as_prolog/2).
  272. thglobal:as_prolog(Fml,Fml):- is_ftVar(Fml),!.
  273. thglobal:as_prolog(Fml,FmlO):- as_symlog(Fml,FmlM),
  274.   to_prolog_ops(OPS),subsT_each(each,FmlM,OPS,FmlO).
  275.  
  276.  
  277. is_modal(n(_Neg,MODAL),BDT):- !, compound(MODAL),is_modal(MODAL,BDT),nonvar(BDT).
  278. is_modal(MODAL,BDT):- compound(MODAL), (MODAL = nesc(BDT,_) ; MODAL = poss(BDT,_)),!,nonvar(BDT).
  279.  
  280. %=% Negation Normal Form
  281.  
  282. % Usage: nnf(Neg,+KB,+Orig,+Fml, ?NNF)
  283.  
  284. nnf(Neg,Fml,NNF):- copy_term(Fml,Orig),
  285.   nnf(Neg,_KB,Orig,Fml,NNF).
  286.  
  287. nnf(Neg,KB,Orig,Fml,NNF):-  
  288.    nnf(Neg,KB,Orig,Fml,[],NNF,_),!.
  289.  
  290. %skolem_setting(nnf).
  291. skolem_setting(removeQ).
  292. %skolem_setting(eliminate).
  293. %skolem_setting(ignore).
  294. % skolem_setting(label).
  295. %skolem_setting(leavein).
  296.  
  297. % Converts TO syntax that NNF/DNF/CNF/removeQ like
  298. adjust_kif(V,V):- is_ftVar(V),!.
  299. adjust_kif(A,A):- \+ compound(A),!.
  300. adjust_kif(n(N,Kif),n(N,KifO)):- !,adjust_kif(Kif,KifO).
  301. adjust_kif(nesc(N,Kif),nesc(N,KifO)):- !,adjust_kif(Kif,KifO).
  302. adjust_kif(poss(N,Kif),poss(N,KifO)):- !,adjust_kif(Kif,KifO).
  303. adjust_kif(-(Kif),n((-),KifO)):- !,adjust_kif(Kif,KifO).
  304. adjust_kif(NOT(Kif),n((-),KifO)):- !,adjust_kif(Kif,KifO).
  305. adjust_kif(poss_not(Kif),poss(b_d(nesc,poss),n((-),KifO))):- !,adjust_kif(Kif,KifO).
  306. adjust_kif(nesc_not(Kif),nesc(b_d(nesc,poss),n((-),KifO))):- !,adjust_kif(Kif,KifO).
  307. adjust_kif(not_poss(Kif),n(-,poss(KifO))):- !,adjust_kif(Kif,KifO).
  308. adjust_kif(not_nesc(Kif),n(-,nesc(KifO))):- !,adjust_kif(Kif,KifO).
  309. adjust_kif(poss(Kif),poss(b_d(nesc,poss),KifO)):- !,adjust_kif(Kif,KifO).
  310. adjust_kif(nesc(Kif),nesc(b_d(nesc,poss),KifO)):- !,adjust_kif(Kif,KifO).
  311. adjust_kif(exists(L,Expr),               ExprO):-L==[],!,adjust_kif(Expr,ExprO).
  312. adjust_kif(exists([L|List],Expr),exists(L,ExprO)):-is_list(List),!,adjust_kif(exists(List,Expr),ExprO).
  313. adjust_kif(exists(L,Expr),exists(L,ExprO)):-!,adjust_kif(Expr,ExprO).
  314. adjust_kif(all(L,Expr),               ExprO):-L==[],!,adjust_kif(Expr,ExprO).
  315. adjust_kif(all([L|List],Expr),all(L,ExprO)):-is_list(List),!,adjust_kif(exists(List,Expr),ExprO).
  316. adjust_kif(all(L,Expr),all(L,ExprO)):-!,adjust_kif(Expr,ExprO).
  317. adjust_kif('&'([L|Ist]),ConjO):- is_list([L|Ist]),list_to_conjuncts('&',[L|Ist],Conj),adjust_kif(Conj,ConjO).
  318. adjust_kif('v'([L|Ist]),ConjO):- is_list([L|Ist]),list_to_conjuncts('v',[L|Ist],Conj),adjust_kif(Conj,ConjO).
  319. adjust_kif(([L|Ist]),ConjO):- is_list([L|Ist]),list_to_conjuncts('&',[L|Ist],Conj),adjust_kif(Conj,ConjO).
  320. adjust_kif(PAB,PABO):- PAB=..[P|AB],maplist(adjust_kif,AB,ABO),PABO=..[P|ABO].
  321.  
  322.  
  323.  
  324. %====== drive negation inward ===
  325. %  nnf(Neg,KB, Orig,+Fml,+FreeV,-NNF,-Paths)
  326. %
  327. % Fml,NNF:    See above.
  328. % FreeV:      List of free variables in Fml.
  329. % Paths:      Number of disjunctive paths in Fml.
  330.  
  331. nnf(Neg,KB, Orig,Lit,FreeV,POS,Paths):- is_ftVar(Lit),!,nnf(Neg,KB, Orig,proven_t(Lit),FreeV,POS,Paths).
  332.  
  333. nnf(_,_, _,Var, _ ,Var,1):- leave_as_is(Var),!.
  334.  
  335. nnf(Neg,KB, Orig,Lit,FreeV,POS,1):- is_ftVar(Lit),!,wdmsg(warn(nnf(Neg,KB, Orig,Lit,FreeV,POS,1))),POS=proven_t(Lit).
  336.  
  337. nnf(Neg,KB, Orig,Fin,FreeV,NNF,Paths):- Fin\=nesc(_,_),is_b(nesc(BDT),Fin,F),!,nnf(Neg,KB, Orig,nesc(BDT,F),FreeV,NNF,Paths).
  338. nnf(Neg,KB, Orig,Fin,FreeV,NNF,Paths):- Fin\=poss(_,_),is_b(poss(BDT),Fin,F),!,nnf(Neg,KB, Orig,poss(BDT,F),FreeV,NNF,Paths).
  339. nnf(Neg,KB, Orig,-(Fin),FreeV,NNF,Paths):- nnf(Neg,KB, Orig,n(Neg,Fin),FreeV,NNF,Paths).
  340.  
  341. nnf(Neg,KB, Orig,n(NegM,Fin),FreeV,NNF,Paths):- NegM\==Neg,!, nnf(NegM,KB, Orig,n(NegM,Fin),FreeV,NNF,Paths).
  342.  
  343. nnf(Neg,KB, Orig,Fin,FreeV,BOX,Paths):- is_b(nesc(BDT),Fin,F), !,
  344.     nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), cnf(Orig,NNF,CNF), boxRule(Orig,nesc(BDT,CNF), BOX).
  345.  
  346. nnf(Neg,KB, Orig,Fin,FreeV,DIA,Paths):- is_b(poss(BDT),Fin,F), !,
  347.     nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), dnf(Orig,NNF,DNF), diaRule(Orig,poss(BDT,DNF), DIA).
  348.  
  349. nnf(Neg,KB, Orig,Fin,FreeV,CIR,Paths):- is_b(cir(CT),Fin,F), !,
  350.     nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), cirRule(Orig,cir(CT,NNF), CIR).
  351.  
  352. nnf(Neg,KB, Orig,nesc(BDT,F),FreeV,BOX,Paths):- !,trace, show_call(nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), cnf(Orig,NNF,CNF), boxRule(Orig,nesc(BDT,CNF), BOX)).
  353. nnf(Neg,KB, Orig,poss(BDT,F),FreeV,DIA,Paths):- !,trace, show_call(nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), dnf(Orig,NNF,DNF), diaRule(Orig,poss(BDT,DNF), DIA)).
  354. nnf(Neg,KB, Orig,  cir(CT,F),FreeV,CIR,Paths):- !,trace, show_call(nnf(Neg,KB, Orig,F,FreeV,NNF,Paths), cirRule(Orig,cir(CT,NNF), CIR)).
  355.  
  356.  
  357. nnf(Neg,KB, Orig,UNTIL(A,B),FreeV,NNF,Paths):- !,
  358.     nnf(Neg,KB, Orig,A,FreeV,NNF1,Paths1),
  359.     nnf(Neg,KB, Orig,B,FreeV,NNF2,Paths2),
  360.     Paths is Paths1 + Paths2,
  361.     NNF = UNTIL(NNF1, NNF2).
  362.  
  363.  
  364. % ==== quantifiers ========
  365. nnf(Neg,KB, Orig,all(X,NNF),FreeV,all(X,NNF2),Paths):-  
  366.      list_to_set([X|FreeV],NewVars),
  367.       nnf(Neg,KB, Orig,NNF,NewVars,NNF2,Paths).
  368.  
  369. nnf(Neg,KB, Orig,exists(X,Fml),FreeV,NNF,Paths):- skolem_setting(nnf),!, wdmsg(nnf(Neg,skolemizing(exists(X,Fml)))),
  370.    must(skolem(KB,Orig,Fml,X,FreeV,FmlSk)),
  371.    must(nnf(Neg,KB, Orig,FmlSk,FreeV,NNF,Paths)).
  372.  
  373. nnf(Neg,KB, Orig,exists(X,Fml),FreeV,NNF,Paths):- skolem_setting(label),
  374.    list_to_set([X|FreeV],NewVars),
  375.      delete(NewVars,X,NewNewVars),
  376.      subst(Fml,X,theThis,FmlNoSk),
  377.     must(nnf(Neg,KB, Orig,(ignore(X =skF(NewNewVars,FmlNoSk)) => Fml),NewVars,NNF,Paths)).
  378.  
  379. nnf(Neg,KB, Orig,exists(X,Fml),FreeV,NNF,Paths):- skolem_setting(ignore),
  380.    list_to_set([X|FreeV],NewVars),
  381.     nnf(Neg,KB, Orig,Fml,NewVars,NNF,Paths).
  382.  
  383. nnf(Neg,KB, Orig,exists(X,Fml),FreeV,exists(X,NNF),Paths):- (skolem_setting(removeQ);skolem_setting(leave)),
  384.    list_to_set([X|FreeV],NewVars),
  385.     nnf(Neg,KB, Orig,Fml,NewVars,NNF,Paths).
  386.  
  387. nnf(Neg,KB, Orig,atleast(1,X,Fml),FreeV,NNF,Paths):- !,
  388.     nnf(Neg,KB, Orig,exists(X,Fml),FreeV,NNF,Paths).
  389.  
  390. nnf(Neg,KB, Orig,atleast(N,X,Fml),FreeV,NNF,Paths):-
  391.     !,
  392.     NewN is N - 1,
  393.         subst_eq(Fml,X,Y,FmlY),
  394.     nnf(Neg,KB, Orig,&(exists(X,Fml),atleast(NewN,Y,FmlY)),FreeV,NNF,Paths).
  395. nnf(Neg,KB, Orig,atmost(1,X,Fml),FreeV,NNF,Paths):-
  396.     !,
  397.         subst_eq(Fml,X,Y,FmlY),
  398.         subst_eq(Fml,X,Z,FmlZ),
  399.     nnf(Neg,KB, Orig,n(Neg,&(exists(Y,FmlY),exists(Z,FmlZ))),FreeV,NNF,Paths).
  400. nnf(Neg,KB, Orig,atmost(N,X,Fml),FreeV,NNF,Paths):-
  401.     !,
  402.         subst_eq(Fml,X,Y,FmlY),
  403.     NewN is N - 1,
  404.     nnf(Neg,KB, Orig,&(exists(Y,FmlY),atmost(NewN,X,Fml)),FreeV,NNF,Paths).
  405.  
  406. nnf(NegIn,KB, Orig,n(Neg,XOR(X , Y)),FreeV,NNF,Paths):-
  407.    !,
  408.    nnf(NegIn,KB, Orig,v(&(X , Y) , &(n(Neg,X) , n(Neg,Y))),FreeV,NNF,Paths).
  409.    
  410. nnf(Neg,KB, Orig,XOR(X , Y),FreeV,NNF,Paths):-
  411.    !,
  412.    nnf(Neg,KB, Orig,&(v(X , Y) , v(n(Neg,X) , n(Neg,Y))),FreeV,NNF,Paths).
  413.    
  414.  
  415. nnf(Neg,KB, Orig,&(A,B),FreeV,NNF,Paths):- !,
  416.     nnf(Neg,KB, Orig,A,FreeV,NNF1,Paths1),
  417.     nnf(Neg,KB, Orig,B,FreeV,NNF2,Paths2),
  418.     Paths is Paths1 * Paths2,
  419.     (Paths1 > Paths2 -> NNF = &(NNF2,NNF1);
  420.                     NNF = &(NNF1,NNF2)).
  421.  
  422. nnf(Neg,KB, Orig,v(A,B),FreeV,NNF,Paths):- !,
  423.         nnf(Neg,KB, Orig,A,FreeV,NNF1,Paths1),
  424.     nnf(Neg,KB, Orig,B,FreeV,NNF2,Paths2),
  425.     Paths is Paths1 + Paths2,
  426.     (Paths1 > Paths2 -> NNF = v(NNF2,NNF1);
  427.                     NNF = v(NNF1,NNF2)).
  428.  
  429. nnf(Neg,KB, Orig,Fml,FreeV,NNF,Paths):-
  430.     (Fml = n(Neg,n(Neg,A)) -> Fml1 = A;
  431.      Fml = n(Neg,nesc(BDT,F)) -> Fml1 = poss(BDT,n(Neg,F));
  432.      Fml = n(Neg,poss(BDT,F)) -> Fml1 = nesc(BDT,n(Neg,F));
  433.      Fml = n(Neg,cir(CT,F)) -> Fml1 = cir(CT,n(Neg,F));
  434.      Fml = n(Neg,UNTIL(A,B)) -> (nnf(Neg,KB, Orig,n(Neg,A),FreeV,NNA,_), nnf(Neg,KB, Orig,n(Neg,B),FreeV,NNB,_),
  435.                                      Fml1 = v(all(NNB), UNTIL(NNB,&(NNA,NNB))));
  436.      Fml = n(Neg,all(X,F)) -> Fml1 = exists(X,n(Neg,F));
  437.      Fml = n(Neg,exists(X,F)) -> Fml1 = all(X,n(Neg,F));
  438.  
  439.      Fml = n(Neg,atleast(N,X,F)) -> Fml1 = atmost(N,X,F);
  440.      Fml = n(Neg,atmost(N,X,F)) -> Fml1 = atleast(N,X,F);
  441.  
  442.      Fml = n(Neg,v(A,B)) -> Fml1 = &(n(Neg,A), n(Neg,B) );
  443.      Fml = n(Neg,&(A,B)) -> Fml1 = v(n(Neg,A), n(Neg,B) );
  444.      Fml = '=>'(A,B) -> Fml1 = v(n(Neg,A), B );
  445.      Fml = n(Neg,'=>'(A,B)) -> Fml1 = &(A, n(Neg,B) );
  446.          Fml = '<=>'(A,B) -> Fml1 = v('=>'(A, B), '=>'(B, A) );
  447.      Fml = '<=>'(A,B) -> Fml1 = v(&(A, B), &(n(Neg,A), n(Neg,B)) );
  448.      Fml = n(Neg,'<=>'(A,B)) -> Fml1 = v(&(A, n(Neg,B)) , &(n(Neg,A), B) )
  449.     ),!,
  450.     nnf(Neg,KB, Orig,Fml1,FreeV,NNF,Paths).
  451.  
  452. /*
  453. nnf(Neg,KB, _Orig,Fml,_,Fml,1):- Fml=..[F,KB,_],third_order(F),!.
  454. nnf(Neg,KB,  Orig,Fml,FreeV,Out,Path):- Fml=..[F,A],third_order(F),  
  455.   nnf(Neg,KB, Orig,A,FreeV,NNF1,Path1),!,
  456.   Fml2=..[F,KB,NNF1],nnf(Neg,KB, Orig,Fml2,FreeV,Out,Path2),Path is Path1+Path2.
  457. */
  458.  
  459. nnf(Neg,KB, Orig, IN,FreeV,OUT,Paths):- simplify_cheap(IN,MID),IN\=MID,nnf(Neg,KB, Orig, MID,FreeV,OUT,Paths).
  460. nnf(Neg,KB,_Orig,Fml,_,FmlO,1):- nonegate(Neg,KB,Fml,FmlO),!.
  461.  
  462. is_lit_atom(IN):- leave_as_is(IN),!.
  463. is_lit_atom(IN):- subst(IN,'&','*',M),subst(M,'v','*',O),!,O==IN.
  464.  
  465.  
  466. mnf(box(A=>B),Out):- mnf(box(v( - B,A)),Out).
  467. mnf(box(v(A,B)),Out):- !,mnf( - dia(- v(A,B)) ,   - dia(&(-A,-B))    box -
  468. mnf(Fml,Out):-boxRule(_,Fml,M),Fml\=M,mnf(M,Out).
  469. mnf(box(Fml),Out):- mnf(- dia(- Fml),Out).
  470. mnf(Fml,Out):-diaRule(_,Fml,M),Fml\=M,mnf(M,Out).
  471.  
  472.         %  <>  <=>  ¬[]¬
  473. nnf(Neg,KB, Orig,poss(BDT,&(A,B)),FreeV,BOX,Paths):-
  474.  
  475.  
  476. third_order(asserted_t).
  477.  
  478.  
  479. boxRule(Orig,nesc(BDT,&(A,B)), &(BA,BB)):- !, boxRule(Orig,nesc(BDT,A),BA), boxRule(Orig,nesc(BDT,B),BB).
  480. boxRule(_Orig,nesc(BDT, IN), BOX):- \+ is_lit_atom(IN),  nnf(Neg,n(Neg,nesc(BDT, n(Neg,IN))),BOX).
  481. boxRule(_Orig,BOX, BOX).
  482.  
  483.  
  484. diaRule(Orig,poss(BDT,v(A,B)), v(DA,DB)):- !, diaRule(Orig,poss(BDT,A),DA), diaRule(Orig,poss(BDT,B),DB).
  485. diaRule(_Orig,DIA, DIA).
  486.  
  487.  
  488. cirRule(Orig,cir(CT,v(A,B)), v(DA,DB)):- !, cirRule(Orig,cir(CT,A),DA), cirRule(Orig,cir(CT,B),DB).
  489. cirRule(Orig,cir(CT,&(A,B)), &(DA,DB)):- !, cirRule(Orig,cir(CT,A),DA), cirRule(Orig,cir B,DB).
  490. cirRule(_Orig,CIR, CIR).
  491.  
  492.  
  493. is_b(nesc(b_d(B,D)),BF,F):- BF=..[B,F],b_d(B,D).
  494. is_b(poss(b_d(B,D)),DF,F):- DF=..[D,F],b_d(B,D).
  495. is_b(nesc(b_d(B,D)),nesc(b_d(B,D),F),F):- b_d(B,D).
  496. is_b(poss(b_d(B,D)),poss(b_d(B,D),F),F):- b_d(B,D).
  497. is_b(nesc(b_d(B,D)),nesc(B,F),F):- b_d(B,D).
  498. is_b(poss(b_d(B,D)),poss(D,F),F):- b_d(B,D).
  499. is_b(cir(ct(CT)),CF,F):- CF=..[CT,F],ct(CT).
  500. is_b(cir(ct(CT)),cir(CT,F),F):- ct(CT).
  501.  
  502. ct(cir).
  503. ct(asserted_t).
  504.  
  505. b_d(box,dia).
  506. b_d(nesc,poss).
  507. b_d(knows,beliefs).
  508. b_d(always,sometimes).
  509. % b_d(A,I):- genlPreds(I,A).
  510.  
  511. %=%
  512. %=%  Conjunctive Normal Form (CNF) : assumes Fml in NNF
  513. %=%
  514.  
  515. % Usage: cnf(Orig, +NNF, ?CNF )
  516. cnf(A,B):- copy_term(A,Orig),cnf(Orig,A,B).
  517. cnf(Orig,A,B):- convertAndCall(as_dlog,cnf(Orig,A,B)).
  518. cnf(Orig,&(P,Q), &(P1,Q1)):- !, cnf(Orig,P, P1), cnf(Orig,Q, Q1).
  519. cnf(Orig,v(P,Q),     CNF):- !, cnf(Orig,P, P1), cnf(Orig,Q, Q1), cnf1(Orig, v(P1,Q1), CNF ).
  520. cnf(_Orig,CNF,       CNF).
  521.  
  522. cnf1(Orig, v(&(P,Q), R), &(P1,Q1) ):- !, cnf1(Orig, v(P,R), P1), cnf1(Orig, v(Q,R), Q1).
  523. cnf1(Orig, v(P, &(Q,R)), &(P1,Q1) ):- !, cnf1(Orig, v(P,Q), P1), cnf1(Orig, v(P,R), Q1).
  524. cnf1(_Orig, CNF,                 CNF).
  525.  
  526.  
  527. %=%
  528. %=% Disjunctive Normal Form (DNF) : assumes Fml in NNF
  529. %=%
  530. % Usage: dnf(Orig, +NNF, ?DNF )
  531. dnf(A,B):- copy_term(A,Orig),dnf(Orig,A,B).
  532. dnf(Orig,A,B):- convertAndCall(as_dlog,dnf(Orig,A,B)).
  533. dnf(Orig, v(P,Q),  v(P1,Q1) ):- !, dnf(Orig,P, P1), dnf(Orig,Q, Q1).
  534. dnf(Orig, &(P,Q), DNF):- !, dnf(Orig,P, P1), dnf(Orig,Q, Q1), dnf1(Orig,&(P1,Q1), DNF).
  535. dnf(_Orig,DNF,       DNF).
  536.  
  537. dnf1(Orig,&(P, v(Q,R)),  v(P1,Q1) ):- !, dnf1(Orig,&(P,Q), P1), dnf1(Orig,&(P,R), Q1).
  538. dnf1(Orig,&(v(P,Q), R), v(P1,Q1) ):- !, dnf1(Orig,&(P,R), P1), dnf1(Orig,&(Q,R), Q1).
  539. dnf1(_Orig,DNF,                  DNF ).
  540.  
  541.  
  542. simplify_cheap(IN,OUT):- IN = nesc(BDT,OUT),is_modal(OUT,BDT),!.
  543. simplify_cheap(n(Neg,poss(BDT, poss(BDT, F))), n(Neg,F)):-nonvar(F),!.
  544. simplify_cheap((poss(BDT, poss(BDT, F))),  poss(BDT, F)):-nonvar(F),!.
  545. %simplify_cheap(IN,-OUT):- IN = n(Neg,poss(BDT,OUT)), is_modal(OUT,BDT),!.
  546. %simplify_cheap(IN,-OUT):- IN = n(Neg,nesc(BDT,OUT)), \+is_modal(OUT,BDT),!.
  547.  
  548.  
  549. is_sentence_functor(_).
  550.  
  551. %=
  552. %=  Prenex Normal Form (PNF)
  553. %=
  554.  
  555. % Usage: pnf(+Orig, +Fml, ?PNF ) : assumes Fml in NNF
  556.  
  557. pnf(A,B):- copy_term(A,Orig),pnf(Orig,A,B).
  558.  
  559. pnf(Orig, F,PNF):- pnf(Orig,F,[],PNF),!.
  560.  
  561. % pnf(+Orig, +Fml, +Vars, ?PNF)
  562.  
  563. pnf(A,B,C,D):- convertAndCall(as_dlog,pnf(A,B,C,D)),!.
  564.  
  565. pnf(_,Var,_ ,Var):- leave_as_is(Var),!.
  566.  
  567. pnf(_, [],  _,           []):- !.
  568.  
  569. pnf(_, IN,  _,              OUT):- is_list(IN),!, maplist(pnf,IN,OUT).
  570.  
  571. pnf(Orig, IN, FreeV,              OUT):- simplify_cheap(IN,MID), pnf(Orig,MID,FreeV,OUT).
  572.  
  573. pnf(Orig,   all(X,F),Vs,   all(X,PNF)):- list_to_set([X|Vs],VVs), !, pnf(Orig,F, VVs, PNF).
  574.  
  575. pnf(Orig,   nesc(X,F),Vs,   nesc(X,PNF)):- !, pnf(Orig,F,Vs, PNF).
  576.  
  577. pnf(Orig,   poss(X,F),Vs,   poss(X,PNF)):- !, pnf(Orig,F,Vs, PNF).
  578.  
  579. pnf(Orig,  exists(X,F),Vs,exists(X,PNF)):- list_to_set([X|Vs],VVs), !, pnf(Orig,F, VVs, PNF).
  580.  
  581. pnf(Orig,  &(exists(X,A) , B),Vs,  exists(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pnf(Orig,&(Ay,B),[Y|Vs], PNF).
  582.  
  583. pnf(Orig,    v(exists(X,A), B),Vs,  exists(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pnf(Orig,v(Ay,B),[Y|Vs], PNF).
  584.  
  585. pnf(Orig, &(all(X,A), B),Vs, all(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pnf(Orig,&(Ay , B),[Y|Vs], PNF).
  586.  
  587. pnf(Orig, v(all(X,A), B),Vs, all(Y,PNF)):- !, copy_term((X,A,Vs),(Y,Ay,Vs)), pnf(Orig,v(Ay,B),[Y|Vs], PNF).
  588.  
  589. pnf(Orig, &(A,exists(X,B)),Vs,  exists(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
  590.                                         pnf(Orig,&(A, By),[Y|Vs], PNF).
  591. pnf(Orig, v(A,exists(X,B)),Vs,  exists(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
  592.                                         pnf(Orig,v(A,By),[Y|Vs], PNF).
  593. pnf(Orig, &(A,all(X,B)),Vs, all(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
  594.                                         pnf(Orig,&(A,By),[Y|Vs], PNF).
  595. pnf(Orig, v(A,all(X,B)),Vs, all(Y,PNF)):- !, copy_term((X,B,Vs),(Y,By,Vs)),
  596.                                         pnf(Orig,v(A,By),[Y|Vs], PNF).
  597.  
  598. pnf(Orig, &(A, B),Vs,       PNF ):- pnf(Orig,A,Vs,Ap), pnf(Orig,B,Vs,Bp),
  599.                                      (A\=Ap; B\=Bp), pnf(Orig,&(Ap,Bp),Vs,PNF).
  600.  
  601. pnf(Orig, v(A, B),Vs,       PNF ):- pnf(Orig,A,Vs,Ap), pnf(Orig,B,Vs,Bp),
  602.                                      (A\=Ap; B\=Bp), pnf(Orig,v(Ap,Bp),Vs,PNF).
  603.  
  604.  
  605. pnf(Orig, [A|B], Vs,       PNF ):- !, pnf(Orig,A,Vs,Ap), pnf(Orig,B,Vs,Bp),
  606.                                      (A\=Ap; B\=Bp), pnf(Orig,[Ap|Bp],Vs,PNF).
  607.  
  608.  
  609. pnf(Orig, H,Vars,FOO ):-  compound(H),H=..[F|ARGS], is_sentence_functor(F), !, pnf(Orig, [F|ARGS],Vars,FOOL ),FOO=..FOOL.
  610.  
  611. pnf(_Orig,          PNF, _,       PNF ).
  612.  
  613. %=%  Clausal Form (CF) : assumes Fml in PNF AND
  614. %                                 each quantified variable is unique
  615.  
  616. % cf(KB, Orig,+Fml, ?Cs)
  617. % Cs is a list of the form: [cl(Head,Body), ...]
  618. % Head AND Body are lists.
  619.  
  620. % cf(KB,A,B,C):- convertAndCall(as_dlog,cf(KB,A,B,C)).
  621. cf(KB, Orig,PNF, SET):- removeQ(KB, Orig,PNF,[], UnQ),
  622.   cnf(Orig,UnQ,CNF),clausify(KB,CNF,Cla,[]),!,
  623.   dnf(Orig,UnQ,DNF),flatten_or_list(Orig,DNF,Flat),make_clause_Vs_each(KB,Flat,EachClause),!,
  624.   append(Cla,[cl([kbMark(Orig)],[])|EachClause],SO),!,
  625.   maplist(correct_cls,SO,SOO),
  626.   list_to_set(SOO,SET),!.
  627.  
  628. removeQ(F,  HH):- removeQ(_KB, _, F, _, RQ0),!,RQ0=HH.
  629.  
  630. % removes quantifiers (also pushes modal operators inside the negations)
  631.  
  632. removeQ(_,_,Var,_ ,Var):- leave_as_is(Var),!.
  633. removeQ(_KB, _Orig, F,_, RQ0):- is_list(F),!,maplist(removeQ,F,HH),!,HH=RQ0.
  634.  
  635.  
  636. removeQ(KB, Orig, IN,FreeV,OUT):-  simplify_cheap(IN,MID), IN\=@=MID, removeQ(KB, Orig, MID,FreeV,OUT).
  637.  
  638. removeQ(KB, Orig, H, Vars, HH ):- convertAndCall(as_dlog,removeQ(KB, Orig,H, Vars, HH )).
  639. removeQ(KB, Orig, n(Neg,n(Neg,F)),Vars, XF):- !, removeQ(KB, Orig,  F,Vars, XF) .
  640. removeQ(KB, Orig, all(X,F),Vars, HH):- !,  removeQ(KB, Orig,F,[X|Vars], RQ0),RQ0=HH.
  641.  
  642. removeQ(KB, Orig, n(Neg,nesc(b_d(B,X), n(Neg,F))),Vars, XF):- !,removeQ(KB, Orig, poss(b_d(B,X), F),Vars, XF).
  643. removeQ(KB, Orig, n(Neg,poss(b_d(B,X), n(Neg,F))),Vars, XF):- !,removeQ(KB, Orig, nesc(b_d(B,X), F),Vars, XF).
  644.  
  645. %removeQ(KB, Orig, n(Neg,nesc(b_d(B,X), (F))),Vars, XF):- !,removeQ(KB, Orig, poss(b_d(B,X), n(Neg,F)),Vars, XF).
  646. %removeQ(KB, Orig, n(Neg,poss(b_d(B,X), (F))),Vars, XF):- !,removeQ(KB, Orig, nesc(b_d(B,X), n(Neg,F)),Vars, XF).
  647.  
  648. removeQ(KB, Orig, nesc(b_d(B,X), n(Neg,F)),Vars, XF):- !,removeQ(KB, Orig, n(Neg,poss(b_d(B,X), F)),Vars, XF).
  649. removeQ(KB, Orig, poss(b_d(B,X), n(Neg,F)),Vars, XF):- !,removeQ(KB, Orig, n(Neg,nesc(b_d(B,X), F)),Vars, XF).
  650.  
  651. removeQ(KB, Orig,  exists(X,F),Vars, HH):- skolem_setting(removeQ),!,wdmsg(removeQ(skolemizing(exists(X,F)))),
  652.     skolem(KB, Orig,F,X,Vars,Fsk),
  653.     removeQ(KB, Orig,Fsk,Vars, HH).
  654.  
  655. removeQ(KB, Orig, exists(X,F),Vars, HH):- !,  removeQ(KB, Orig,F,[X|Vars], RQ0),RQ0=HH.
  656.  
  657. removeQ(KB, Orig, ':-'(H,B), Vars, ':-'(HH,BB ) ):- !, removeQ(KB, Orig,H, Vars, HH ),removeQ(KB, Orig,B, Vars, BB).
  658. removeQ(_, _, cl(H,B), _, O ):- !,correct_cls(cl(H,B),O).
  659. removeQ(KB, Orig,     [ H|B ],Vars, [ HH|BB ] ):- !,removeQ(KB, Orig,H, Vars, HH ),removeQ(KB, Orig,B, Vars, BB).
  660.  
  661.  
  662. removeQ(KB,_Orig, F,_,FOO ):- kb_nlit(KB,Neg),once(nnf(Neg,F,FO)),F\=@=FO, loop_check(removeQ(KB,_,FO,_,FOO)).
  663.  
  664. removeQ(KB,Orig, H,Vars,HH ):- compound(H),H=..[F|ARGS],!,removeQ(KB,Orig, ARGS,Vars,ARGSO ),HH=..[F|ARGSO].
  665.  
  666. removeQ(_,_Orig, F,_,F0 ):- F=F0.
  667.  
  668. display_form(Form):- demodal_sents(Form,Out),portray_clause(Out).
  669.  
  670. demodal_sents(I,O):-transitive(demodal_sents0,I,O).
  671.  
  672. demodal_sents0(I,O):-demodal(I,M),modal2sent(M,O),!.
  673.  
  674. demodal(Var, Var):- leave_as_is(Var),!.
  675. demodal(n(Neg,H), HHH):- must(atom(Neg)),demodal(H, HH),!,HHH=..[Neg,HH].
  676. demodal(nesc(b_d(X,_),F), XF):- !,demodal(F, HH), XF =..[X,HH].
  677. demodal(poss(b_d(_,X),F), XF):- !,demodal(F, HH), XF =..[X,HH].
  678. demodal(neg(H),NOT(HH)):- nonvar(H),demodal(H,HH).
  679. demodal(-(H),NOT(HH)):- nonvar(H),demodal(H,HH).
  680. demodal([H|T],[HH|TT]):- !, must(( demodal(H,HH),demodal(T,TT))),!.
  681. demodal(H,HH ):- H=..[F|ARGS],!,maplist(demodal,ARGS,ARGSO),!,HH=..[F|ARGSO].
  682.  
  683. is_sent_op_modality(NOT).
  684. is_sent_op_modality(poss).
  685. is_sent_op_modality(nesc).
  686. atom_compat(F,HF,HHF):- F\=HF, is_sent_op_modality(F),is_sent_op_modality(HF), format(atom(HHF),'~w_~w',[F,HF]).
  687.  
  688. modal2sent(Var, Var):- leave_as_is(Var),!.
  689. modal2sent(G,O):- G=..[F,H], \+ leave_as_is(H), H=..[HF,HH], atom_compat(F,HF,HHF),!, GG=..[HHF,HH], modal2sent(GG,O).
  690. modal2sent([H|T],[HH|TT]):- !, must(( modal2sent(H,HH),modal2sent(T,TT))),!.
  691. modal2sent(H,HH ):- H=..[F|ARGS],!,maplist(modal2sent,ARGS,ARGSO),!,HH=..[F|ARGSO].
  692.  
  693.  
  694. clausify(KB, &(P,Q), C1, C2 ):-
  695.     !,
  696.     clausify(KB, P, C1, C3 ),
  697.     clausify(KB, Q, C3, C2 ).
  698. clausify(KB, P, [cl(A,B)|Cs], Cs ):-
  699.     inclause(KB, P, A, [], B, [] ),
  700.     !.
  701. clausify(_KB, _, C, C ).
  702.  
  703. inclause(KB, v(P,Q), A, A1, B, B1 ):-
  704.     !,
  705.     inclause(KB, P, A2, A1, B2, B1 ),
  706.     inclause(KB, Q, A,  A2, B,  B2 ).
  707. inclause(KB, n(Neg, PP) , A,  A, B1, B ):-
  708.         negate(KB, n(Neg, PP),P),
  709.     !,
  710.     notin(P, A ),
  711.     putin(P, B, B1 ).
  712. inclause(_KB, P,  A1, A, B,  B ):-
  713.     !,
  714.     notin(P, B ),
  715.     putin(P, A, A1 ).
  716.  
  717. notin(X,[Y|_]):- X==Y, !, fail.
  718. notin(X,[_|Y]):- !,notin(X,Y).
  719. notin(_,[]).
  720.  
  721. putin(X,[],   [X]   ):- !.
  722. putin(X,[Y|L],[Y|L] ):- X == Y,!.
  723. putin(X,[Y|L],[Y|L1]):- putin(X,L,L1).
  724.  
  725.  
  726. make_clause_Vs_each(KB,List,Out):- must((findall(E,make_each(KB,List,E),Out),Out=[_|_])).
  727. make_each(KB,List,E):- member(One,List),  make_1_cl(KB,One,List,E).
  728.  
  729. make_1_cl(KB,One,List,cl([One],NewBodyListO)):- delete_eq(List,One,Rest),
  730.   maplist(negate_one(KB),Rest,NewBodyList),
  731.   flattenConjs(KB,NewBodyList,NewBodyListM),
  732.   maplist(thglobal:as_prolog,NewBodyListM,NewBodyListO).
  733.  
  734. flattenConjs(_KB,I,O):- conjuncts_to_list(I,M),maplist(conjuncts_to_list,M,L),flatten(L,O).
  735.  
  736. is_neg(n(_Neg,_)).
  737. is_pos(One):- get_functor(One,F),!,NOT(is_log_op(F)).
  738.  
  739. :- export(is_log_sent/1).
  740. is_log_sent(S):- get_functor(S,F,_),is_log_op(F).
  741.  
  742. not_log_op(OP):- NOT(is_log_op(OP)).
  743. :- export(is_log_op/1).
  744. is_log_op(OP):- atomic(OP),to_dlog_ops(OPS),!,(member(OP=_,OPS);member(_=OP,OPS)).
  745.  
  746.  
  747. :- export(logical_pos/3).
  748. :- export(logical_neg/3).
  749. logical_neg(KB,Wff,WffO):-
  750.   must(nonegate(Neg,KB,Wff,Wff1)),nnf(Neg,KB,n(Neg,Wff1),n(Neg,Wff1),Wff2),must(nonegate(Neg,KB,Wff2,WffO)),!.
  751. logical_pos(KB,Wff,WffO):-
  752.   must(nonegate(Neg,KB,Wff,Wff1)),nnf(Neg,KB,Wff1,Wff1,Wff2),must(nonegate(Neg,KB,Wff2,WffO)),!.
  753.  
  754.  
  755. negate_one(KB,Wff,WffO):- logical_neg(KB,Wff,WffO).
  756.  
  757.  
  758. negate(KB,X,Z):- must(defunctionalize(X,Y)), must(negate0(KB,Y,Z)).
  759. negate0(KB,n(Neg,X),X):- kb_nlit(KB,Neg).
  760. negate0(KB,X,n(Neg,X)):- kb_nlit(KB,Neg).
  761.  
  762.  
  763. mpred_quf(In,Out):- transitive(mpred_quf_0,In,Out).
  764.  
  765. mpred_quf_0(InOut,InOut):- non_compound(InOut),!.
  766. % mpred_quf_0(In,Out):- current_predicate(db_quf/4),db_quf(change(assert,_Must),In,U,C),conjoin(U,C,Out).
  767. mpred_quf_0(In,In).
  768.  
  769. :- export(nonegate/4).
  770. nonegate(Neg,KB,List,OutZ):- is_list(List),maplist(nonegate(Neg,KB),List,OutZ),!.
  771. nonegate(Neg,KB,Fml,OutZ):- simplify_cheap(Fml,Fml2), Fml \=@= Fml2,nonegate(Neg,KB,Fml2,OutZ),!.
  772. nonegate(Neg,KB,Fml,OutZ):- must((unbuiltin_negate(Neg,KB,Fml,Out),!,defunctionalize(Out,OutY),!,must(mpred_quf(OutY,OutZ)))),!.
  773.  
  774. unbuiltin_negate(_Neg,_, Fml,Fml):- is_ftVar(Fml),!.
  775. unbuiltin_negate(_Neg,_, Fml,Out):- get_functor(Fml,F,A),pttp_builtin(F,A),!,must(Out=Fml).
  776. unbuiltin_negate(_Neg,KB,Fml,Out):- once(negate(KB,Fml,Neg)),negate(KB,Neg,Out),!.
  777.  
  778. %=%  Skolemizing : method 1
  779.  
  780. % Usage: skolem(+Fml,+X,+FreeV,?FmlSk)
  781. % Replaces existentially quantified variable with the formula
  782. % VARIABLES MUST BE PROLOG VARIABLES
  783. % exists(X,p(X)) ==> p(p(exists))
  784.  
  785. skolem_bad(Fml,X,FreeV,FmlSk):-
  786.     copy_term((X,Fml,FreeV),(Fml,Fml1,FreeV)),
  787.     copy_term((X,Fml1,FreeV),(exists,FmlSk,FreeV)).
  788.  
  789. %=%  Skolemizing : method 2
  790.  
  791. % Usage: skolem(KB, Orig, +Fml, +X, +FreeV, ?FmlSk )
  792. % Replaces existentially quantified variable with a unique FUNCTION
  793. % fN(Vars) N=1,...
  794. % VARIABLES MAYBE EITHER PROLOG VARIABLES OR TERMS
  795.  
  796. skolem(KB, Orig, F, X, FreeV, Out):-  
  797.    must(skolem_f(KB, Orig, F, X, FreeV, Sk)),
  798.    subst(F,X,Sk,Out).
  799.  
  800. skolem(KB, Orig, F, X, FreeV, Out):-  
  801.    must(skolem_f(KB, Orig, F, X, FreeV, Sk)),
  802.    must(Out=('=>'(mudEquals(X,Sk),F))),!.
  803.  
  804. skolem(KB, Orig, F, X, FreeV, FmlSk):-
  805.     must(skolem_f(KB, Orig, F, X, FreeV, Sk)),
  806.     must(subst_eq(F, X, Sk, FmlSk)),!.
  807.  
  808.  
  809. skolem_f(KB, Orig, F, X, FreeVIn, Sk):-
  810.        must_det_l([
  811.          delete_eq(FreeVIn,KB,FreeV),
  812.          list_to_set(FreeV,FreeVSet),
  813.     contains_var_lits(F,X,LitsList),
  814.         mk_skolem_name(Orig,X,LitsList,'',SK),
  815.         concat_atom(['sk',SK,'Fn'],Fun),
  816.     Sk =..[Fun,KB|FreeVSet]]).
  817. /*
  818.  
  819.  
  820. %=% Substitution
  821.  
  822. % Usage: subst_eq(+Fml,+X,+Sk,?FmlSk)
  823. subst_eq(Fml,X,Sk,FmlSkO):- pred_subst(==,Fml,X,Sk,FmlSk),!,must(FmlSkO=FmlSk).
  824.  
  825.  
  826. % Usage: pred_subst(+Pred,+Fml,+X,+Sk,?FmlSk)
  827. pred_subst(Pred,   all(Y,P), X,Sk,   all(Y,P1) ):- !, pred_subst(Pred, P,X,Sk,P1 ).
  828. pred_subst(Pred,exists(Y,P), X,Sk,exists(Y,P1) ):- !, pred_subst(Pred, P,X,Sk,P1 ).
  829. pred_subst(Pred, &(P,Q), X,Sk,&(P1,Q1) ):- !, pred_subst(Pred, P,X,Sk,P1 ), pred_subst(Pred, Q,X,Sk,Q1 ).
  830. pred_subst(Pred,  v(P,Q), X,Sk, v(P1,Q1) ):- !, pred_subst(Pred, P,X,Sk,P1 ), pred_subst(Pred, Q,X,Sk,Q1 ).
  831.  
  832. pred_subst(Pred,       P,    X,Sk,       P1    ):- call(Pred,P,X), Sk=P1,!.
  833. pred_subst(_Pred,       P,    _,_,       P1    ):- is_ftVar(P), P1=P,!.
  834. pred_subst(Pred,       P,    X,Sk,       P1    ):- compound(P),
  835.                              P =..Args,
  836.                                pred_subst2(Pred, X, Sk, Args, ArgS ),!,
  837.                              P1 =..ArgS.
  838. pred_subst(_  ,        P,    _, _,       P     ).
  839.  
  840. pred_subst2(_   , _,  _, [], [] ).
  841. pred_subst2(Pred, X, Sk, [A|AS], [Sk|AS] ):- call(Pred, X, A), !, pred_subst2(Pred, X, Sk, AS, AS).
  842. pred_subst2(Pred, X, Sk, [A|AS], [A|AS]  ):- is_ftVar(A), !, pred_subst2(Pred, X, Sk, AS, AS).
  843. pred_subst2(Pred, X, Sk, [A|AS], [Ap|AS] ):- pred_subst(Pred, A,X,Sk,Ap ), pred_subst2(Pred, X, Sk, AS, AS).
  844. */
  845.  
  846.  
  847.  
  848.  
  849. %=%=%=%=%=%=%=%=%=%=%=
  850. %=% generate a skolem
  851.  
  852. mk_skolem_name(_O,Var,Fml,SIN,SOut):- is_ftVar(Fml), same_var(Var,Fml),!,atom_concat('Is',SIn,SOut).
  853. mk_skolem_name(_O,_V,Fml,SIN,SIN):- is_ftVar(Fml),!.
  854. mk_skolem_name(_O ,_V,[],SIN,SIN):- !.
  855. mk_skolem_name(_O,_V, OP,SIN,SIN):- is_log_op(OP),!.
  856. mk_skolem_name(_O,_V,Fml,SIN,SOut):- atomic(Fml),!,i_name(Fml,N),toPropercase(N,CU),!,(atom_contains(SIN,CU)->SOut=SIN;atom_concat(SIN,CU,SOut)).
  857. mk_skolem_name(Orig,Var,[H|T],SIN,SOut):- !,mk_skolem_name(Orig,Var,H,SIN,M),mk_skolem_name(Orig,Var,T,M,SOut).
  858. mk_skolem_name(Orig,Var,isa(VX,Lit),SIN,SOut):- same_var(Var,VX),not_ftVar(Lit),!,mk_skolem_name(Orig,Var,['Is',Lit,'In'],'',F),atom_concat(F,SIn,SOut).
  859. mk_skolem_name(Orig,Var,Fml,SIN,SOut):- Fml=..[F,VX],same_var(Var,VX),!,mk_skolem_name(Orig,Var,['Is',F,'In'],SIn,SOut).
  860. mk_skolem_name(Orig,Var,Fml,SIN,SOut):- Fml=..[F,Other,VX|_],same_var(Var,VX),!,type_of_var(Orig,Other,OtherType),
  861.    mk_skolem_name(Orig,Var,[OtherType,'Arg2Of',F],SIn,SOut).
  862. mk_skolem_name(Orig,Var,Fml,SIN,SOut):- Fml=..[F,VX|_],same_var(Var,VX),!,mk_skolem_name(Orig,Var,['Arg1Of',F],SIn,SOut).
  863. mk_skolem_name(Orig,Var,Fml,SIN,SOut):- Fml=..[F|_],!,mk_skolem_name(Orig,Var,['ArgNOf',F],SIn,SOut).
  864.  
  865. % same_var(Var,Fml):- NOT(NOT(Var=Fml)),!.
  866. same_var(Var,Fml):- Var==Fml,!.
  867.  
  868.  
  869. %======  make a sequence out of a disjunction =====
  870. flatten_or_list(A,B,C):- convertAndCall(as_symlog,flatten_or_list(A,B,C)).
  871. flatten_or_list(Orig,v(X , Y), F):- !,
  872.    flatten_or_list(Orig,X,A),
  873.    flatten_or_list(Orig,Y,B),
  874.    flatten([A,B],F).
  875. flatten_or_list(_Orig,X,[X]).
  876.  
  877.  
  878.  
  879. fmtl(X):- thglobal:as_prolog(X,XX), fmt(XX).
  880.  
  881. write_list([F|R]):- write(F), write('.'), nl, write_list(R).
  882. write_list([]).
  883.  
  884. numbervars_with_names(Term):-
  885.    term_variables(Term,Vars),name_variables(Vars),!,
  886.    numbervars(Term,91,_,[attvar(skip),singletons(false)]),!.
  887.  
  888. name_variables([]).
  889. name_variables([Var|Vars]):-
  890.    (var_property(Var, name(Name)) -> Var = '$VAR'(Name) ; true),
  891.    name_variables(Vars).
  892.  
  893. wdmsgl(CNF):- compound(CNF),CNF=..[NAME,NF],!,must(wdmsgl_2(NAME,NF)).
  894. wdmsgl(NF):- must((get_functor(NF,NAME),!,must(wdmsgl_2(NAME,NF)))).
  895.  
  896.  
  897. wdmsgl_2(NAME,NF):- functor(NF,_,_),wdmsgl_3(NAME,&,NF).
  898.  
  899. wdmsgl_3(NAME,F,NF):- copy_term(vv(NAME,F,NF),vv(NAME2,F2,NF2)),
  900.    numbervars_with_names(vv(NAME2,F2,NF2)),!,
  901.    wdmsgl_4(NAME2,F2,NF2).
  902.  
  903. wdmsgl_4(NAME,F,NF):- is_list(NF),!,list_to_set(NF,NS),maplist(wdmsgl_4(NAME,F),NS).
  904. wdmsgl_4(NAME,F,NF):- compound(NF),NF=..[FF,A,B],FF=F,not_ftVar(A),not_ftVar(B),!,
  905.   maplist(wdmsgl_4(NAME,F),[A,B]).
  906. wdmsgl_4(NAME,_,NF):- as_symlog(NF,NF2), cyc:pterm_to_sterm(NF2,NF3),with_all_dmsg(display_form(NAME:-NF3)).
  907.  
  908.  
  909.  
  910. put_singles(Wff,_,[],Wff).
  911. put_singles(Wff,Exists,[S|Singles],NewWff):-  
  912.    (((each_subterm(Wff,SubTerm),compound(SubTerm),
  913.     SubTerm=..[OtherExists,SO,_],same_var(SO,S),
  914.      member(OtherExists,[all,exists])))
  915.  -> WffM = Wff ; WffM =..[Exists,S,Wff]),
  916.    put_singles(WffM,Exists,Singles,NewWff),!.
  917.  
  918.  
  919. ensure_quantifiers(Wff:- B,WffO):- B== true,!, ensure_quantifiers(Wff,WffO).
  920. ensure_quantifiers(Wff:- B,Wff:- B):- !.
  921. ensure_quantifiers(Wff,Wff):-!.
  922. ensure_quantifiers(Wff,WffO):-
  923.  must_det_l((show_call(term_singletons(Wff,[],NS,[],Singles)),
  924.   put_singles(Wff,'exists',Singles,WffM),put_singles(WffM,'all',NS,WffO))).
  925.  
  926. :- multifile(function_corisponding_predicate/2).
  927. :- dynamic(function_corisponding_predicate/2).
  928.  
  929. get_pred(Pred,F):- get_functor(Pred,F).
  930. is_function(F):- is_ftVar(F),!,fail.
  931.  
  932.  
  933. is_function(FUNCTION):- compound(FUNCTION),get_functor(FUNCTION,F,A),is_function(FUNCTION,F,A).
  934.  
  935. is_function(_,'SubLQuoteFn',_):- !,fail.
  936. is_function(_,F,_):- atom_concat('sk',_Was,F),!,fail.
  937. is_function(_,F,_):- atom_concat(_Was,'Fn',F).
  938. is_function(_,F,_):- tFunction(F).
  939. is_function(_,F,A):- A2 is A+1,current_predicate(F/A2), NOT(current_predicate(F/A)).
  940.  
  941. %:- pfc_add(isa(I,C)<=(ttPredType(C),user:isa(I,C))).
  942.  
  943. is_ftEquality(Term):- is_ftVar(Term),!,fail.
  944. %is_ftEquality(Term):- get_pred(Term,Pred),is),!,(Pred==mudEquals;genlPreds(Pred,equals);clause_asserted(prologEquality(Pred))),!.
  945. is_ftEquality(mudEquals(_,_)).
  946. is_ftEquality(equals(_,_)).
  947.  
  948. function_to_predicate(FUNCTION,NewVar,PredifiedFunction):-
  949.   FUNCTION=..[F|ARGS],
  950.   function_corisponding_predicate(F,P),
  951.   PredifiedFunction=..[P,NewVar|ARGS].
  952. function_to_predicate(FUNCTION,NewVar,mudEquals(NewVar,FUNCTION)).
  953.  
  954. :- export(defunctionalize/2).
  955. defunctionalize(Wff,WffO):- defunctionalize(',',Wff,WffO).
  956. defunctionalize(_ ,Wff,Wff):- non_compound(Wff),!.
  957. defunctionalize(OP,Wff,WffO):- compound(Wff),
  958.   each_subterm(Wff,SubTerm),
  959.   compound(SubTerm),
  960.   NOT(is_ftEquality(SubTerm)),
  961.   arg(_,SubTerm,FUNCTION),is_function(FUNCTION),
  962.   subst_eq(SubTerm,FUNCTION,NewVar,NewSubTerm),
  963.   must(function_to_predicate(FUNCTION,NewVar,PredifiedFunction)),
  964.   NEW =..[OP,PredifiedFunction,NewSubTerm],
  965.   subst_eq(Wff,SubTerm,NEW,NextWff),!,
  966.   defunctionalize(OP,NextWff,WffO).
  967. defunctionalize(_,Wff,Wff).
  968.  
  969.  
  970. delete_sublits(H0,B,HH):- delete_eq(H0,B,H1),delete_eq(H1,B,H2),delete_eq(H2,B,HH),!.
  971.  
  972. % cl([-nesc(p)], [-poss(p), nesc(q), -poss(q)]).
  973.  
  974. correct_cls(H,HH):-loop_check(correct_cls0(H,HH),H=HH),!.
  975. correct_cls0(CL0,CL1):- is_list(CL0),!,maplist(correct_cls,CL0,CL1).
  976. correct_cls0(cl([POS(BD,v(H1,H2))],B),O):- delete_sublits(B,H,BB),BB\=@=B,!,correct_cls(cl([H],BB),O).
  977. correct_cls0(cl([H],B),O):- delete_sublits(B,H,BB),BB\=@=B,!,correct_cls(cl([H],BB),O).
  978. correct_cls0(cl(H,B),O):- list_to_set(B,BB),BB\=@=B,!,correct_cls(cl(H,BB),O).
  979. correct_cls0(CL,O):- demodal_sents(CL,CLM),CL\=@=CLM,!,correct_cls(CLM,O).
  980. correct_cls0(cl(H,B),O):-removeQ(H,HH),removeQ(B,BB),!,((H\=@=HH ; B\=@=BB) -> correct_cls(cl(HH,BB),O); O=cl(H,B)),!.
  981.  
  982. % kif_to_boxlog('=>'(WffIn,enables(Rule)),'$VAR'('MT2'),complete,Out1), % kif_to_boxlog('=>'(enabled(Rule),WffIn),'$VAR'('KB'),complete,Out).  
  983.  
  984. kif_to_prolog(X,E):- kif_to_boxlog(X,Y),!,list_to_set(Y,S),!,member(E,S).
  985.  
  986. %====== kif_to_boxlog(+Wff,-NormalClauses):-
  987. :- export(kif_to_boxlog/2).
  988. % kif_to_boxlog(Wff,Out):- loop_check(kif_to_boxlog(Wff,Out),Out=looped_kb(Wff)).
  989. kif_to_boxlog(Wff,Out):- why_to_id(rule,Wff,Why), kif_to_boxlog(Wff,Why,Out),!.
  990. kif_to_boxlog(WffIn,Out):-  why_to_id(rule,WffIn,Why), kif_to_boxlog(all('$VAR'('KB'),'=>'(asserted_t('$VAR'('KB'),WffIn),WffIn)),'$VAR'('KB'),Why,Out).
  991. kif_to_boxlog(WffIn,NormalClauses):- why_to_id(rule,WffIn,Why), kif_to_boxlog(WffIn,'$VAR'('KB'),Why,NormalClauses).
  992.  
  993. alt_kif_to_boxlog(n(Neg, Wff),KB,Why,Out):- !, kif_to_boxlog(n(Neg, Wff),KB,Why,Out).
  994. alt_kif_to_boxlog(Wff,KB,Why,Out):- loop_check(kif_to_boxlog((n(Neg,nesc(n(Neg,Wff)))),KB,Why,Out),Out=looped_kb(Wff)).
  995.  
  996. :- export(kif_to_boxlog/3).
  997. kif_to_boxlog(WffIn,Why,Out):-  kif_to_boxlog(WffIn,'$VAR'('KB'),Why,Out),!.
  998.  
  999. kif_to_boxlog(Fml,KB,Why,Flattened):- var(KB),!,kif_to_boxlog(Fml,'$VAR'('KB'),Why,Flattened).
  1000.  
  1001. kif_to_boxlog(Wff,KB,Why,Out):- once(adjust_kif(Wff,M)),Wff \=@= M ,!,kif_to_boxlog(M,KB,Why,Out).
  1002. kif_to_boxlog((Wff:- B),KB,Why,Flattened):- is_true(B),!, kif_to_boxlog(Wff,KB,Why,Flattened),!.
  1003. kif_to_boxlog(WffInIn,KB,Why,FlattenedO):-  as_dlog(WffInIn,WffIn),WffInIn\=@=WffIn,!,kif_to_boxlog(WffIn,KB,Why,FlattenedO),!.
  1004.  
  1005. % kif_to_boxlog(Wff,KB,Why,Out):- loop_check(kif_to_boxlog(Wff,KB,Why,Out),alt_kif_to_boxlog(Wff,KB,Why,Out)),!.
  1006.  
  1007. kif_to_boxlog((HEAD:- BODY),KB,Why,FlattenedO):-  
  1008.   must_det_l((
  1009.    conjuncts_to_list(HEAD,HEADL),conjuncts_to_list(BODY,BODYL),
  1010.    maplist(correct_cls,[cl(HEADL,BODYL)],NCFs),
  1011.    maplist(clauses_to_boxlog(KB,Why),NCFs,ListOfLists),
  1012.    flatten([ListOfLists],Flattened),
  1013.    maplist(removeQ,Flattened,FlattenedO),
  1014.    wdmsgl(horn(FlattenedO)))),!.
  1015.  
  1016. kif_to_boxlog(WffIn,KB,Why,FlattenedO):-    
  1017.   must_det_l((
  1018.    must(numbervars_with_names(WffIn:KB:Why)),  
  1019.    ensure_quantifiers(WffIn,WffQ),
  1020.    Orig = WffQ,
  1021.    defunctionalize('=>',WffQ,Wff),  
  1022.    (WffQ\==Wff-> dmsg(defunctionalize('=>',WffQ,Wff));wdmsgl(kif(Wff))),
  1023.    as_dlog(Wff,Wff666),
  1024.    kb_nlit(KB,Neg),
  1025.    add_nesc(Wff666,Wff6667),
  1026.    transitive(nnf(Neg,KB,Orig),Wff6667,NNF),
  1027.    transitive(pnf,NNF,PNF),
  1028.    %wdmsgl(pnf(PNF)),
  1029.    cf(KB,Orig,PNF,NCFsI),!,
  1030.    cf_to_flattened_clauses(KB,Why,NCFsI,FlattenedO))),!.
  1031.  
  1032. add_nesc(Wff666,Wff666):-leave_as_is(Wff666),!.
  1033. add_nesc(Wff666,Wff666):-is_modal(Wff666,_),!.
  1034. add_nesc(Wff666,nesc(Wff666)).
  1035.  
  1036. cf_to_flattened_clauses(KB,Why,NCFsI,FlattenedO):-
  1037.  must_det_l((
  1038.    maplist(correct_cls,NCFsI,NCFs),
  1039.    wdmsgl(cf(NCFs)),
  1040.    maplist(clauses_to_boxlog(KB,Why),NCFs,ListOfLists),
  1041.    flatten([ListOfLists],Flattened),
  1042.    thglobal:as_prolog(Flattened,FlattenedL),
  1043.    list_to_set(FlattenedL,FlattenedS),
  1044.    maplist(demodal_sents,FlattenedS,FlattenedO))),!.
  1045.  
  1046.  
  1047.  
  1048.  
  1049. clauses_to_boxlog(KB,Why,In,Prolog):- correct_cls(In,Mid), Mid \=@= In, !,clauses_to_boxlog(KB,Why,Mid,Prolog).
  1050. clauses_to_boxlog(_,_Why,cl([HeadIn],[]),Prolog):- !,is_lit_atom(HeadIn) -> Prolog=HeadIn ; kif_to_boxlog(HeadIn,Prolog).
  1051. clauses_to_boxlog(KB,Why,cl([],BodyIn),Prolog):-  !,
  1052.    is_lit_atom(BodyIn) -> clauses_to_boxlog(KB,Why,cl([inconsistentKB(KB)],BodyIn),Prolog);  kif_to_boxlog(-(BodyIn),Prolog).
  1053. clauses_to_boxlog(_,_Why,cl([HeadIn],BodyIn),(HeadIn:- BodyOut)):- maplist(logical_pos(_KB),BodyIn,Body), list_to_conjuncts(Body,BodyOut),!.
  1054. clauses_to_boxlog(KB,Why,cl([H,Head|List],BodyIn),Prolog):-
  1055.   findall(Answer,((member(E,[H,Head|List]),delete_eq([H,Head|List],E,RestHead),
  1056.     maplist(logical_neg(KB),RestHead,RestHeadS),append(RestHeadS,BodyIn,Body),
  1057.     clauses_to_boxlog(KB,Why,cl([E],Body),Answer))),Prolog),!.
  1058.  
  1059.  
  1060. mpred_t_tell_snark(OP2,RULE):-
  1061.  with_assertions(thlocal:current_pttp_db_oper(mud_call_store_op(OP2)),
  1062.    (show_call(call((must(snark_tell(RULE))))))).
  1063.  
  1064.  
  1065. fix_input_vars(AIn,A):- copy_term(AIn,A),numbervars(A,672,_).
  1066.  
  1067. %:- export(show_boxlog/1).
  1068. %assert_boxlog(AIn):- fix_input_vars(AIn,A), as_dlog(A,AA),kif_to_boxlog(AA,B),!,maplist(snark_tell_boxes(Why),B),!,nl,nl.
  1069. %:- export(show_boxlog2/2).
  1070. %assert_boxlog2(AIn):- fix_input_vars(AIn,A), with_all_dmsg((kif_to_boxlog(A,B),!,maplist(snark_tell_boxes(Why),B),!,nl,nl)).
  1071.  
  1072. snark_test_string(
  1073. "
  1074. % )
  1075. tell.
  1076.  
  1077. all(R,room(R) => exists(D, (door(D) & has(R,D)))).
  1078. room(room1).
  1079.  
  1080. ask.
  1081.  
  1082. room(What).
  1083.  
  1084. door(What).
  1085.  
  1086. :- snark_tell(a(XX) & b(XX) => c(XX)).
  1087. :- snark_tell(all(R,room(R) => exists(D, (door(D) & has(R,D))))).
  1088. :- snark_tell(loves(Child,motherFn(Child))).
  1089. :- snark_tell((p => q)).
  1090. :- snark_tell(~p <=> ~q).
  1091. :- snark_tell(p <=> q).
  1092. :- snark_tell(all(P, person(P) => ~exists(D, dollar(D) & has(P,D)))).
  1093.  
  1094. :- snark_tell(go(sam) & (go(bill) v go(sally) ) & go(nancy)).
  1095.  
  1096. :- snark_tell(rains_tuesday => wear_rain_gear xor carry_umbrella).
  1097. :- snark_tell(exists(P, (person(P) & all(C, car(C) => ~has(P,C))))).
  1098.  
  1099. :- snark_tell(room(R) => exists(D, (door(D) & has(R,D)))).
  1100. :- snark_tell((goes(jane) xor goes(sandra) => goes(bill))).
  1101. :- snark_tell(exists(P, exists(C, (person(P) & car(C) & has(P,C))))).
  1102. :- snark_tell(~all(P,person(P) => exists(C, car(C) & has(P,C)))).
  1103. :- snark_tell((go(sam) & go(bill)) v (go(sally) & go(nancy))).
  1104. :- snark_tell(go(sam) & (go(bill) v go(sally) ) & go(nancy)).
  1105. :- snark_tell(exists(C, course(C) & exists(MT1, midterm(C,MT1) & exists(MT2, midterm(C,MT2) & different(MT1,MT2))))).
  1106. :- snark_tell(exists(C, course(C) & ~exists(MT3, midterm(C,MT3)))).
  1107.  
  1108. "
  1109. ).
  1110.  
  1111.  
  1112. %:- export(tsn/0).
  1113. tsn:- with_all_dmsg(forall(clause(snark,C),must(C))).
  1114.  
  1115. % snark:- make.
  1116. tsnark:- snark_test_string(TODO),snark(STRING(TODO),current_output).
  1117.  
  1118. :- multifile(user:mud_regression_test/0).
  1119. user:mud_regression_test:- tsn.
  1120.  
  1121. :- thread_local(snark_action_mode/1).
  1122. :- asserta_if_new(snark_action_mode(tell)).
  1123.  
  1124. :- thread_local(snark_reader_mode/1).
  1125. :- asserta_if_new(snark_reader_mode(lisp)).
  1126.  
  1127.  
  1128. snark_read(In,Wff,Vs):-
  1129.   (snark_reader_mode(lisp) ->
  1130.     catch((lisp_read(In,WffIn),with_output_to(atom(A),write_term(WffIn,
  1131.       [module(logicmoo_i_snark),numbervars(true),quoted(true)])),
  1132.      read_term_from_atom(A,Wff,[module(logicmoo_i_snark),double_quotes(STRING),variable_names(Vs)])),E,(fmt(E),fail));
  1133.       catch(read_term(In,Wff,[module(logicmoo_i_snark),double_quotes(STRING),variable_names(Vs)]),E,(fmt(E),fail))).
  1134.  
  1135. %= ===== TO test program =====-
  1136. :- ensure_loaded(library(plarkc/dbase_i_sexpr_reader)).
  1137.  
  1138. :- export(snark/0).
  1139. snark:- current_input(In),current_output(Out),!,snark(In,Out).
  1140.  
  1141. open_input(InS,InS):- is_stream(InS),!.
  1142. open_input(STRING(InS),In):- text_to_string(InS,STR),string_codes(STR,Codes),open_chars_stream(Codes,In),!.
  1143.  
  1144. :- export(snark/2).
  1145. snark(InS,Out):-
  1146.   l_open_input(InS,In),
  1147.    repeat,            
  1148.       debugOnError((once((snark_action_mode(Mode),write(Out,Mode),write(Out,'> '))),
  1149.         snark_read(In,Wff,Vs),
  1150.          b_setval('$variable_names', Vs),
  1151.            portray_clause(Out,Wff,[variable_names(Vs),quoted(true)]),
  1152.            once(snark_process(Wff)),
  1153.            Wff == end_of_file)),!.
  1154.  
  1155. :- export(id_to_why/3).
  1156. why_to_id(Term,Wff,IDWhy):- NOT(atom(Term)),term_to_atom(Term,Atom),!,why_to_id(Atom,Wff,IDWhy).
  1157. why_to_id(Atom,Wff,IDWhy):- wid(IDWhy,Atom,Wff),!.
  1158. why_to_id(Atom,Wff,IDWhy):- must(atomic(Atom)),gensym(Atom,IDWhyI),kb_incr(IDWhyI,IDWhy),assertz_if_new(user:wid(IDWhy,Atom,Wff)).
  1159.  
  1160. :- export(snark_process/1).
  1161. snark_process(end_of_file):- !.
  1162. snark_process(prolog):- prolog_repl,!.
  1163. snark_process(Assert):- atom(Assert),retractall(snark_action_mode(_)),asserta(snark_action_mode(Assert)),fmtl(snark_action_mode(Assert)),!.
  1164. snark_process(Wff):- snark_action_mode(Mode),snark_process(Mode,Wff),!.
  1165.  
  1166. snark_process(_,':-'(Wff)):- !, snark_process(call,Wff).
  1167. snark_process(_,'?-'(Wff)):- !, snark_ask(Wff).
  1168. snark_process(_,'ask'(Wff)):- !, snark_ask(Wff).
  1169. snark_process(_,'tell'(Wff)):- !, snark_tell(Wff).
  1170. snark_process(call,Call):- !,call(Call).
  1171. snark_process(tell,Wff):- !, snark_tell(Wff).
  1172. snark_process(ask,Wff):- !, snark_ask(Wff).
  1173. snark_process(Other,Wff):- !, wdmsg(error(missing_snark_process(Other,Wff))),!,fail.
  1174.  
  1175. :- export(snark_ask_sent/1).
  1176. snark_ask_sent(Wff):-
  1177.    why_to_id(ask,Wff,Why),
  1178.    term_variables(Wff,Vars),
  1179.    gensym(z_q,ZQ),
  1180.    Query=..[ZQ,666|Vars],
  1181.    kif_to_boxlog('=>'(Wff,Query),Why,Asserts),!,
  1182.    snark_tell_boxes(Why,Asserts),!,
  1183.    call_cleanup(
  1184.      snark_ask(Query),
  1185.      pttp_retractall_wid(Why)).
  1186.  
  1187.  
  1188. :- export(snark_ask/1).
  1189. snark_ask(P <=> Q):- snark_ask_sent(P <=> Q).
  1190. snark_ask(P => Q):- snark_ask_sent(P => Q).
  1191. snark_ask((P v Q)):- snark_ask_sent(((P v Q))).
  1192. snark_ask((P & Q)):- snark_ask_sent((P & Q)).
  1193. snark_ask(Goal0):-  logical_pos(_KB,Goal0,Goal),
  1194.     no_repeats(user:(
  1195.     add_args(Goal0,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],_ProofOut1,Goal1,_),!,
  1196.         search(Goal1,60,0,1,3,DepthIn,DepthOut))).
  1197.  
  1198. :- export(snark_ask/2).
  1199. snark_ask(Goal0,ProofOut):- logical_pos(_KB,Goal0,Goal),
  1200.     no_repeats(user:(
  1201.     add_args(Goal0,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],ProofOut1,Goal1,_),!,
  1202.         search(Goal1,60,0,1,3,DepthIn,DepthOut),
  1203.         contract_output_proof(ProofOut1,ProofOut))).
  1204.  
  1205. snark_tell(Wff):- why_to_id(tell,Wff,Why),snark_tell(Why,Wff).
  1206.  
  1207. :- export(snark_tell/2).
  1208.  
  1209. snark_tell(_,[]).
  1210. snark_tell(Why,[H|T]):- !,snark_tell(Why,H),kb_incr(Why,Why2),snark_tell(Why2,T).
  1211. snark_tell(Why,Wff):-  must(kif_to_boxlog(Wff,Why,Asserts)),must(snark_tell_boxes(Why,Wff,Asserts)),!.
  1212.  
  1213. snark_tell_boxes(Why,Wff0,Asserts0):- must_det_l((unnumbervars(Asserts0+Wff0,Asserts+Wff),
  1214.   %fully_expand(Get1,Get),
  1215.   get_constraints(Wff,Isas), snark_add_constraints(Why,Isas,Asserts))).
  1216.  
  1217. snark_add_constraints(Why,Isas,Get1Get2):- var(Get1Get2),!,trace_or_throw(var_snark_tell_isa_boxes(Why,Isas,Get1Get2)).
  1218. snark_add_constraints(Why,Isas,(Get1,Get2)):- !,snark_add_constraints(Why,Isas,Get1),kb_incr(Why,Why2),snark_add_constraints(Why2,Isas,Get2).
  1219. snark_add_constraints(Why,Isas,[Get1|Get2]):- !,snark_add_constraints(Why,Isas,Get1),kb_incr(Why,Why2),snark_add_constraints(Why2,Isas,Get2).
  1220. snark_add_constraints(_,_,[]).
  1221. snark_add_constraints(Why,Isas,((H:- B))):- conjoin(Isas,B,BB), snark_tell_boxes1(Why,(H:- BB)).
  1222. snark_add_constraints(Why,Isas,((H))):- snark_tell_boxes1(Why,(H:- Isas)).
  1223.  
  1224. snark_tell_boxes1(_,[]).
  1225. snark_tell_boxes1(Why,[H|T]):- !,must_det_l((snark_tell_boxes1(Why,H),kb_incr(Why,Why2),snark_tell_boxes1(Why2,T))).
  1226. snark_tell_boxes1(Why,AssertI):- must_det_l((simplify_bodies(AssertI,AssertO),snark_tell_boxes2(Why,AssertO))).
  1227.  
  1228. snark_tell_boxes2(Why,Assert):-
  1229.   must_det_l((
  1230.   boxlog_to_prolog(Assert,Prolog),  
  1231.   unnumbervars(Prolog,PTTP),
  1232.   assert_wfs(Why,PTTP))).
  1233.  
  1234. simplify_bodies((H:- B),(H:- BC)):- must_det_l((conjuncts_to_list(B,RB),simplify_list(RB,BB),list_to_conjuncts(BB,BC))).
  1235. simplify_bodies((B),(BC)):- must_det_l((conjuncts_to_list(B,RB),simplify_list(RB,BB),list_to_conjuncts(BB,BC))).
  1236.  
  1237.  
  1238. simplify_list(RB,BBO):- list_to_set(RB,BB),maplist(removeQ,BB,BBO).
  1239.  
  1240. assert_wfs(Why,PrologI):- must_det_l((thglobal:as_prolog(PrologI,Prolog), with_assertions(thlocal:current_why(Why,Prolog),pfc_add_h(Prolog)))).
  1241.  
  1242. pfc_add_h((H:- B)):- subst(H,NOT,neg,HH),subst(B,NOT,~,BB),dmsg((pfc_add=((HH:- BB)))),!.
  1243. pfc_add_h(H):- subst(H,NOT,neg,PrologM),dmsg(pfc_add = (PrologM)),!.
  1244.  
  1245. use_was_isa_h(_,ftTerm,true):- !.
  1246. use_was_isa_h(_,argi(mudEquals,_),true):- !.
  1247. use_was_isa_h(I,T,ISA):- to_isa_out(I,T,ISA),!.
  1248.  
  1249. generate_ante([],[],InOut,InOut).
  1250. generate_ante([I|VarsA],[T|VarsB],In,Isas):- use_was_isa_h(I,T,ISA), conjoin(In,ISA,Mid),generate_ante(VarsA,VarsB,Mid,Isas).
  1251.  
  1252. get_constraints(_,true):- !.
  1253. get_constraints(ListA,Isas):-
  1254.      must_det_l((copy_term(ListA,ListB),
  1255.       term_variables(ListA,VarsA),
  1256.       term_variables(ListB,VarsB),
  1257.       attempt_attribute_args(isAnd,ftAskable,ListB),
  1258.       attribs_to_atoms(VarsB,VarsB),
  1259.       generate_ante(VarsA,VarsB,true,Isas))).
  1260.  
  1261. boxlog_to_prolog(IN,OUT):-leave_as_is(IN),!,IN=OUT.
  1262. boxlog_to_prolog(H, HH):-is_list(H),!,maplist(boxlog_to_prolog,H,HH).
  1263.  
  1264. boxlog_to_prolog((V:- TRUE),VE):- is_true(TRUE),boxlog_to_prolog(V,VE),!.
  1265. boxlog_to_prolog((H:- B),(HH:- BB)):- !,boxlog_to_prolog(H,HH),boxlog_to_prolog(B,BB).
  1266. boxlog_to_prolog((H & B),(HH , BB)):- !,boxlog_to_prolog(H,HH),boxlog_to_prolog(B,BB).
  1267. boxlog_to_prolog((H v B),(HH ; BB)):- !,boxlog_to_prolog(H,HH),boxlog_to_prolog(B,BB).
  1268. boxlog_to_prolog((H , B),(HH , BB)):- !,boxlog_to_prolog(H,HH),boxlog_to_prolog(B,BB).
  1269. boxlog_to_prolog((H ; B),(HH ; BB)):- !,boxlog_to_prolog(H,HH),boxlog_to_prolog(B,BB).
  1270. boxlog_to_prolog(IN,OUT):-demodal(IN,M),IN\=@=M,!,boxlog_to_prolog(M,OUT).
  1271. boxlog_to_prolog(H,O):- H=..[N,nesc(F)],kb_nlit(_,N),nonvar(F),!,HH=..[N,F],boxlog_to_prolog(HH,O).
  1272. boxlog_to_prolog(nesc(F),O):- nonvar(F),!,boxlog_to_prolog(F,O).
  1273. boxlog_to_prolog(NOT(nesc(F)),O):- nonvar(F),!,boxlog_to_prolog(naf(F),O).
  1274. boxlog_to_prolog(~poss(F),O):-nonvar(F),!,boxlog_to_prolog(not_poss(F),O).
  1275. boxlog_to_prolog(n(Neg,H),n(Neg,HH)):- !,boxlog_to_prolog(H,HH).
  1276.  
  1277. boxlog_to_prolog( H, HH):- H=..[F|ARGS],!,boxlog_to_prolog(ARGS,ARGSO),!,HH=..[F|ARGSO].
  1278. boxlog_to_prolog(BL,PTTP):- thglobal:as_prolog(BL,PTTP).
  1279.  
  1280.  
  1281. /*
  1282. :- told.
  1283. :- dmsg_show(_).
  1284. :- dmsg('i see this').
  1285. :- snark_tell(exists(C, course(C) & ~exists(MT3, midterm(C,MT3)))).
  1286. :- snark_test_string(TODO),snark(STRING(TODO),current_output).
  1287. :- set_no_debug.
  1288. */
  1289. /*
  1290. :- notrace.
  1291. :- nodebug.
  1292.  
  1293. :- wdmsg('we see this').
  1294.  
  1295. :- lsting(snark_tell/1).
  1296. :- snark_tell((p => q)).
  1297. :- snark_tell(~p <=> ~q).
  1298. :- snark_tell(tRoom(R) => exists(D, (tDoor(D) & has(R,D)))).
  1299. :- snark_tell(isa(R,tPred) => exists(D, (isa(D,ftInt) & arity(R,D)))).
  1300. :- snark_tell(all(P, person(P) => ~(exists(D, dollar(D) & has(P,D))))).
  1301. :- snark_tell(p <=> q).
  1302. :- snark_tell(all(P, person(P) => exists(D, dollar(D) & has(P,D)))).
  1303. */
  1304. % :- prolog.
  1305.  
  1306. :- snark_tell(all(R,room(R) => exists(D, (door(D) & has(R,D))))).
  1307. % :- snark_tell(loves(Child,motherFn(Child))).
  1308.  
  1309. :- dynamic(snark_pred_head/1).
  1310. :- style_check(-singleton).
  1311.  
  1312. snark_pred_head(P):- var(P),!,isa(F,prologSNARK),arity(F,A),functor(P,F,A).
  1313. snark_pred_head(P):- get_functor(P,F,_),isa(F,prologPTTP).
  1314.  
  1315. :- dynamic(pttp_pred_head/1).
  1316.  
  1317. pttp_pred_head(P):- var(P),isa(F,prologPTTP),arity(F,A),functor(P,F,A).
  1318. pttp_pred_head(P):- get_functor(P,F,_),isa(F,prologPTTP).
  1319.  
  1320. :- multifile(snarky_comment/1).
  1321.  
  1322.  
  1323. pttp_listens_to_head(_OP,P):- pttp_pred_head(P).
  1324.  
  1325. pttp_listens_to_stub(prologPTTP).
  1326. pttp_listens_to_stub(prologSNARK).
  1327.  
  1328.  
  1329. user:provide_mpred_setup(Op,H):- provide_snark_op(Op,H).
  1330.  
  1331. % OPHOOK ASSERT
  1332. provide_snark_op(change(assert,How),(HeadBody)):-
  1333.    pttp_listens_to_head(change(assert,How),HeadBody),
  1334.    why_to_id(provide_snark_op,(HeadBody),ID),
  1335.    snark_tell(ID,(HeadBody)).
  1336.  
  1337. % OPHOOK CALL
  1338. provide_snark_op(call(How),Head):-
  1339.   pttp_listens_to_head(call(How),Head),
  1340.   pttp_call(Head).
  1341.  
  1342. % OPHOOK CLAUSES
  1343. provide_snark_op(clauses(How),(Head:- Body)):-
  1344.    pttp_listens_to_head(clauses(How),Head),
  1345.    provide_mpred_storage_clauses(Head,Body,_Why).
  1346.  
  1347. % OPHOOK
  1348. provide_snark_op(OP,(HeadBody)):-
  1349.    pttp_listens_to_head(OP,HeadBody),
  1350.    snark_process(OP,HeadBody).
  1351.  
  1352.  
  1353. % CLAUSES HOOK
  1354. user:provide_mpred_storage_clauses(H,B,wid3(IDWhy)):- wid(IDWhy,_,(H:- B)).
  1355. user:provide_mpred_storage_clauses(H,true,wid3(IDWhy)):- wid(IDWhy,_,(H)),compound(H),NOT(functor(H,':-',2)).
  1356.  
  1357.  
  1358. % REGISTER HOOK
  1359. user:provide_mpred_setup(OP,HeadIn,StubType,RESULT):-  pttp_listens_to_stub(StubType),!,
  1360.    get_pifunctor(HeadIn,Head,F),
  1361.       assert_if_new(isa(F,prologPTTP)),
  1362.          ensure_universal_stub(Head),
  1363.          RESULT = declared(pttp_listens_to_head(OP,Head)).
  1364.  
  1365. :- uses_logic(logicmoo_kb_refution).
  1366.  
  1367. :- if_startup_script(tsnark).
  1368. :- if_startup_script(ensure_loaded(logicmoo_i_mpred_snark_testing)).
  1369. :- logicmoo_example3.
  1370.  
  1371. end_of_file.
  1372.  
  1373. :- dynamic(user:int_proven_t/10).
  1374.  
  1375. int_proven_t(P, X, Y, E, F, A, B, C, G, D):- t(P,X,Y),
  1376.         test_and_decrement_search_cost(A, 0, B),
  1377.         C=[H, [proven_t(P, X, Y), D, E, F]|I],
  1378.         G=[H|I].
  1379.  
  1380.  
  1381. :- dynamic(user:int_assumed_t/10).
  1382. int_assumed_t(P, X, Y, E, F, A, B, C, G, D):- t(P,X,Y),
  1383.         test_and_decrement_search_cost(A, 0, B),
  1384.         C=[H, [assumed_t(P, X, Y), D, E, F]|I],
  1385.         G=[H|I].
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!