18
20:- module(logicmoo_i_cyc_kb,[
21 is_better_backchained/1,
22 addCycL/1,
23 addCycL1/1,
24 addCycL1/1,
25 cycl_to_mpred/2,
26 as_cycl/2,
27 is_better_backchained/1,
28 rtEscapeFunction/1
29
30 ]). 31:- set_module(class(development)). 32
36
37:- op(500,fx,'~'). 38:- op(1050,xfx,('==>')). 39:- op(1050,xfx,'<==>'). 40:- op(1050,xfx,('<-')). 41:- op(1100,fx,('==>')). 42:- op(1150,xfx,('::::')). 43:-
44 system:((
45 op(1199,fx,('==>')),
46 op(1190,xfx,('::::')),
47 op(1180,xfx,('==>')),
48 op(1170,xfx,'<==>'),
49 op(1160,xfx,('<-')),
50 op(1150,xfx,'=>'),
51 op(1140,xfx,'<='),
52 op(1130,xfx,'<=>'),
53 op(600,yfx,'&'),
54 op(600,yfx,'v'),
55 op(350,xfx,'xor'),
56 op(300,fx,'~'))). 57
58:- dynamic(baseKB:tinyKB/3). 59:- multifile(baseKB:tinyKB/3). 60:- baseKB:export(baseKB:tinyKB/3). 61:- system:import(baseKB:tinyKB/3). 62
63is_simple_gaf(V):-not(compound(V)),!.
64is_simple_gaf(V):-needs_canoncalization(V),!,fail.
65is_simple_gaf(V):-functor(V,F,A),member(F/A,[isa/2,genls/2,argQuotedIsa/3,afterAdding/2,afterRemoving/2]),!.
66is_simple_gaf(V):-needs_indexing(V),!,fail.
67is_simple_gaf(_).
68
69needs_indexing(V):-compound(V),arg(_,V,A),not(is_simple_arg(A)),!,fail.
70
71is_simple_arg(A):-not(compound(A)),!.
72is_simple_arg(A):-functor(A,Simple,_),rtEscapeFunction(Simple).
73
75rtEscapeFunction('TINYKB-ASSERTION').
76rtEscapeFunction('uQuoteFn').
77rtEscapeFunction(X):- clause_b('rtUnreifiableFunction'(X)).
78
79needs_canoncalization(CycL):-is_ftVar(CycL),!,fail.
80needs_canoncalization(CycL):-functor(CycL,F,_),isa_db(F,'rtSentenceOperator').
81needs_canoncalization(CycL):-needs_indexing(CycL).
82
83is_better_backchained(CycL):-is_ftVar(CycL),!,fail.
84is_better_backchained(CycL):-functor(CycL,F,_),isa_db(F,'rtSentenceOperator').
85is_better_backchained(V):-unnumbervars(V,FOO),(((each_subterm(FOO,SubTerm),nonvar(SubTerm),isa_db(SubTerm,rtAvoidForwardChain)))),!.
86
87
88as_cycl(VP,VE):-subst(VP,('-'),(~),V0),subst(V0,('v'),(or),V1),subst(V1,('exists'),(exists),V2),subst(V2,('&'),(and),VE),!.
89
90kif_to_boxlog_ex(I,O):- if_defined(kif_to_boxlog(I,M)),if_defined(boxlog_to_pfc(M,O)).
91
92:- kb_global(baseKB:and/7). 93
94tiny_to_kif:-
95 forall(load_order(C),forall(tinyKB(C,MT,STR),with_current_why(tinyKB(C,MT,STR),addCycL(C)))).
96
97load_order(isa(_,tFunction)).
98load_order(isa(_,ttExpressionType)).
99load_order(isa(_,tRelation)).
100load_order(isa(_,tCol)).
101load_order(P):- tinyKB(isa(F,rtWFFConstraintSatisfactionPredicate)),tinyKB(arity(F,A)),functor(P,F,A).
102load_order(P):- tinyKB(isa(F,rtWFFConstraintPredicate)),tinyKB(arity(F,A)),functor(P,F,A).
103load_order(P):- when(nonvar(P),\+ kif_hook(P)).
104load_order(P):- when(nonvar(P), kif_hook(P)).
105
106:- dynamic(addTiny_added/1). 107addCycL(V):- must_be(nonvar,V),cycl_to_mpred(V,VC),addCycL1(VC),!.
108
109addCycL1(V):-addTiny_added(V),!.
110addCycL1(V):-asserta(addTiny_added(V)),unnumbervars(V,VE),
111 112 show_call(ain(VE)).
113
114
115sent_to_conseq(CycLIn,Consequent):- into_mpred_form_locally(CycLIn,CycL), ignore((tiny_support(CycL,_MT,CALL),retract(CALL))),must(cycl_to_mpred(CycL,Consequent)),!.
116
117
118cycl_to_mpred(V,Out):-cycl_to_mpred0(V,Out).
119
120cycl_to_mpred0(V,V):- var(V),!.
121cycl_to_mpred0((V1 , V2),Out):-!,cycl_to_mpred0(V1,Out),cycl_to_mpred0(V2,Out),!.
122cycl_to_mpred0([V1 | V2],Out):-!,cycl_to_mpred0(V1,Out),cycl_to_mpred0(V2,Out),!.
123cycl_to_mpred0((TRUE=>V),Out):-is_true(TRUE),cycl_to_mpred0(V,Out),!.
124cycl_to_mpred0(<=(V , TRUE),Out):-is_true(TRUE),cycl_to_mpred0(V,Out),!.
125cycl_to_mpred0((V :- TRUE),Out):-is_true(TRUE),cycl_to_mpred0(V,Out),!.
126cycl_to_mpred0(V,Out):- into_mpred_form_locally(V,M),V\=@=M,!,cycl_to_mpred0(M,Out),!.
127cycl_to_mpred0((V :- A),(V :- A)):- !.
128cycl_to_mpred0(V,Out):- cyc_to_pdkb(V,VE),cycl_to_mpred1(VE,Out).
129
130cycl_to_mpred1(V,Out):-defunctionalize('implies',V,VE),V\=@=VE,!,cycl_to_mpred1(VE,Out).
131cycl_to_mpred1(V,Out):-is_simple_gaf(V),!,cycl_to_mpred2(V,Out),!.
132cycl_to_mpred1(V,Out):-kif_to_boxlog_ex(V,VP),[V]\=@=VP,!,as_cycl(VP,VE),cycl_to_mpred0(VE,Out).
133cycl_to_mpred1(V,Out):-cycl_to_mpred2(V,Out),!.
134
135cycl_to_mpred2(V,Out):-unnumbervars(V,Out),!.
136
138
139
140
141into_mpred_form_locally(V,V):- current_prolog_flag(logicmoo_load_state,making_renames),!.
142into_mpred_form_locally(V,R):- maybe_notrace((into_mpred_form(V,R), R\= isa(_,not))),!.
143
144freeze_u(V,G):- freeze(V,call_u(G)).
145
146:- kb_global(baseKB:rtLogicalConnective/1). 147
148get_LogicalConnective(F):- call_u(rtLogicalConnective(F)).
149
150as_compound(G):- compound(G),!.
151as_compound(G):- get_LogicalConnective(F),connective_arity(F,A),functor(G,F,A).
152as_compound(G):- between(2,11,A),functor(G,t,A).
153
154connective_arity(F,A):- connective_arity0(F,A).
155connective_arity(_,A):- between(2,11,A).
156connective_arity0(equiv,2):-!.
157connective_arity0(implies,2):-!.
158connective_arity0(not,1):-!.
159
160inner_connective(F) :- get_LogicalConnective(F), \+ connective_arity0(F,_).
161
162:- multifile(baseKB:istAsserted/2). 163:- kb_global(baseKB:istAsserted/2). 164
165:- assert(((istAsserted(MT,P):- if_defined(kb7166:assertion_content(ist,MT,P,_),fail)))). 166:- assert(((istAsserted(MT,P):- if_defined(nlkb7166:acnl(ist,MT,P,_),fail)))). 168:- assert(((istAsserted(MT,P):- asserted_id(P,ID),if_defined(assertion_mt(ID,MT))))). 169
170baseKB:tAsserted(ist(MT,P)):- !, istAsserted(MT,P).
171baseKB:tAsserted(P):-
172 asserted_id(P,_).
173
174:- multifile(baseKB:ist/2). 175:- kb_global(baseKB:ist/2). 176:- assert(((ist(MT,P):- istAsserted(MT,P)))). 177
178
180
181
182asserted_id(P,ID):- compound(P), P=..[F,F1|ARGS],append(ARGS,[ID],ARGSID),
183 (F==t -> (AP=..[assertion_content,F1|ARGSID],nop(freeze_u(F1,\+ get_LogicalConnective(F1))));
184 AP=..[assertion_content,F,F1|ARGSID]),!,
185 if_defined(kb7166:AP),
186 varnamify(ID),
187 guardify(ID).
188asserted_id(PO,ID):- var(PO),
189 190 between(3,13,N2),N is 16-N2,
191 current_predicate(assertion_content/N),
192 functor(AP,assertion_content,N),
193 AP=..[assertion_content,F|PARGS],
194 append(ARGS,[ID],PARGS),
195 if_defined(kb7166:AP),
196 ((
197 varnamify(ID),
198 ((atom(F) -> P=..[F|ARGS]; P=..[t,F|ARGS])),
199 litterally_guard(ID,P,PO))).
200
201
202litterally_guard(ID,I,O):- get_guard(ID,Guard),!,must_det(and_conj_to_list(Guard,List)),must_det(add_guard_list_needed(I,List,O)),!.
203litterally_guard(_,IO,IO).
204
205add_guard_list(IO,[],IO):-!.
206add_guard_list(I,[List],List=>I):-!.
207add_guard_list(I,List,AList=>I):- AList=..[and|List].
208
209add_guard_list_needed(IO,[],IO):-!.
210add_guard_list_needed(I,List,O):-remove_unneeded(I,List,AList),!,add_guard_list(I,AList,O).
211
212remove_unneeded(I,[List|ListIS],AList):- !,
213 (skip_guard(I,List) -> remove_unneeded(I,ListIS,AList);
214 (remove_unneeded(I,ListIS,MList),AList=[List|MList])).
215remove_unneeded(_,[],[]).
216
217
218
219guardify(ID):- get_guard(ID,Guard),!,must_det(and_conj_to_list(Guard,List)),must_maplist(maybe_add_guard,List),!.
220guardify(_).
221
222get_guard(ID,Guard):- compound(ID),functor(ID,F,A),get_guard(ID,F,A,Guard).
223get_guard(ID,_,1,Guard):- !, assertion_variable_guard(ID,Guard).
224get_guard(ID,F,_,Guard):- functor(GID,F,1),assertion_variable_guard(GID,Guard),!,
225 term_variables(GID+Guard,GVars),
226 (GVars=[GV] -> ID=..[F,GV|_] ; (ID=..[F|GVars])).
227
228get_guard(ID,_,_,Guard):- assertion_variable_guard(ID,Guard).
229
230
231
232skip_guard(_,'quotedIsa'(_,EXPR)):-EXPR='ftExpression'.
233skip_guard(I,Var):- sub_var(Var,I).
234
235maybe_add_guard(G):- skip_guard(_,G),!.
236maybe_add_guard(G):- term_variables(G,Vars),maplist(maybe_add_guard_2(G),Vars).
237maybe_add_guard_2(G,Var):-add_cond(Var,G).
238
239and_conj_to_list(C,[C]):- var(C),!.
240and_conj_to_list([],[]):- !.
241and_conj_to_list(C,C):- \+ compound(C),!.
242and_conj_to_list(AND,List):- AND=..[and|List],!.
243and_conj_to_list(C,[C]).
244
245varnamify(ID):- assertion_varnames(ID,NAMES),!,ID=..[_|VARS],maplist(varnamify,VARS,NAMES).
246varnamify(_).
247varnamify(Var,String):- string_to_atom(String,Atom),nb_current('$variable_names',Was),!,b_setval('$variable_names',[Atom=Var|Was]),
248 name_variable(Var,Atom).
249
250badz:- asserted_id(t(P,A,zzzz),ID),dmsg(badz(asserted_id(t(P,A,zzzz),ID))),fail.
251badz:- asserted_id(t(P,zzzz,B),ID),dmsg(asserted_id(t(P,zzzz,B),ID)),fail.
252badz:- asserted_id(t(zzzz,A,B),ID),dmsg(asserted_id(t(zzzz,A,B),ID)),fail.
253
254test_kb_boxlog:- asserted_id(P,ID),nl,nl,compound(ID),wdmsg(asserted_id(P,ID)),test_boxlog(P).
255
256:- multifile(kb7166:assertion_content/3). 257:- dynamic(kb7166:assertion_content/3). 258:- multifile(kb7166:assertion_content/4). 259:- dynamic(kb7166:assertion_content/4). 260:- baseKB:ain((tAsserted(rtLogicalConnective(F))==>rtLogicalConnective(F))). 261
262:- baseKB:ain(rtArgsVerbatum(tAsserted)). 263
264:- baseKB:ain(((tAsserted(mtCycInternalAnthropacity(MT))==> mtUndressedMt(MT)))). 265
266:- ain((baseKB:mtUndressedMt(iEnglishParaphraseMt))). 267
268cyc_ain(P):- mpred_ainz(P,(kb7166,ax)),writeq(P),nl.
269
270fix_head(HEAD,FHEAD):- fully_expand(HEAD,FHEAD).
271
272pred_in_mt(F,A,MT,Type):- no_repeats(pred_in_mt0(F,A,MT,Type)).
273
274pred_in_mt0(F,A,MT0,Type0):-
275 pred_in_mt1(_QQ,F,A,MT0,Type0).
276
277pred_in_mt1(QQ,F,A,MT0,Type0):-
278 asserted_id(QQ,ID),
279 assertion_mt(ID,MT),
280 append_dir(ID,fact,Type),
281 preds_fa_s(Type,Type0,MT,QQ,F,A,MT0).
282
283append_dir(ID,I,O):- assertion_forward(ID),!,append_dir0(f,I,O).
284append_dir(ID,I,O):- assertion_backward(ID),!,append_dir0(b,I,O).
285append_dir(ID,I,O):- assertion_code(ID),!,append_dir0(c,I,O).
286append_dir(_, I,O):- append_dir0(u,I,O).
287
288append_dir0(C,fact,C):-!.
289append_dir0(C,I,O):- O=..[C,I].
290
291
292preds_fa_s(_Type,_Type0,_MT,QQ,_,_,_MT0):- \+ compound(QQ),!,fail.
293preds_fa_s(Type,Type0,_,ist(MT,QQ),F0,A0,MT0):- !,preds_fa_s(Type,Type0,MT,QQ,F0,A0,MT0).
294preds_fa_s(Type,Type0,MT,not(Q),F0,A0,MT0):- !,preds_fa_s(not(Type),Type0,MT,Q,F0,A0,MT0).
295preds_fa_s(Type,Type0,MT,knows(A,Q),F0,A0,MT0):- !, preds_fa_s(knows(Type),Type0,modal(A,MT),Q,F0,A0,MT0).
296preds_fa_s(Type,Type0,MT,implies(P,Q),F0,A0,MT0):- !, (preds_fa_s(antec(Type),Type0,MT,P,F0,A0,MT0); preds_fa_s(consq(Type),Type0,MT,Q,F0,A0,MT0)).
297preds_fa_s(Type,Type0,MT,QQ,F0,A0,MT0):-
298 functor(QQ,F,A),
299 ((get_LogicalConnective(F),append_dir0(F,Type,FType))
300 -> (arg(_,QQ,Arg),preds_fa_s(FType,Type0,MT,Arg,F0,A0,MT0)) ;
301 (F0=F,A0=A,MT=MT0,Type=Type0)).
302
303scyc:- forall(pred_in_mt(F,A,MT,Type), cyc_ain(cycPredMtType(F,A,MT,Type))).
304
323
324:- fixup_exports.