2:- module(mpred_pttp_precompiled,[]). 4
5:- '$set_source_module'(baseKB). 6
7:- kb_shared(wrapper_for/2).
10subst_each(In,[],In).
11subst_each(In,[B=A|List],Out):-
12 subst1(In,B,A,Mid),
13 subst_each(Mid,List,Out),!.
14
15subst1( Var, VarS,SUB,SUB ) :- Var==VarS,!.
16subst1( Var, _,_,Var ) :- \+compound(Var),!.
17subst1([H|T],B,A,[HH|TT]):- !,
18 subst1(H,B,A,HH),
19 subst1(T,B,A,TT).
20subst1(HT,B,A,HHTT):- HT=..FARGS,subst1(FARGS,B,A,[FM|MARGS]),
21 (atom(FM)->HHTT=..[FM|MARGS];univ_tl(FM,MARGS,HHTT)).
22
23univ_tl(Call,EList,CallE):-must((compound(Call),is_list(EList))), Call=..LeftSide, append(LeftSide,EList,ListE), CallE=..ListE.
24univ_tl(Call,EList,CallE):-must((compound(Call),is_list(EList))), Call=..LeftSide, append(LeftSide,EList,ListE), CallE=..ListE.
25
26
27
28:- kb_shared(was_pttp_functor/3). 29:- was_dynamic(was_pttp_functor/3). 30
31
33
34
37
38was_pttp_functor(base, askable_t,2-6).
39was_pttp_functor(base, asserted_t,2-6).
40was_pttp_functor(base, fallacy_t,2-6).
41was_pttp_functor(base, possible_t,2-6).
43was_pttp_functor(base, true_t,2-6).
44was_pttp_functor(base, unknown_t,2-6).
45
46was_pttp_functor(base, isa,2-2).
47was_pttp_functor(base, pred_isa_t,2-2).
48was_pttp_functor(base, pred_t,3-3).
49
50
52
53baseKB:use_mpred_t.
54
55:- was_dynamic(t/3). 56:- kb_shared(t/3). 57:- was_dynamic(t/4). 58:- kb_shared(t/4). 59
61
63
64map_int_functors(EXT,CALLF,A,PREREQ):-
65 atom_concat('int_',EXT,INT),
66 functor(I_A_T,INT,A),
67 I_A_T=..[INT|ARGS],
68 T_T=..[CALLF|ARGS],
69 A_T=..[EXT|ARGS],
70 subst_each((i_a_t(H, I, D, E, F, J, G) :-
71 pretest_call((PREREQ,D=E)),
72 F=[K, [a_t, G, H, I]|L], J=[K|L]),
73 [i_a_t = I_A_T,a_t=A_T,call_t=T_T],NEW),
74 assert_if_new(NEW).
75
76
77:- forall(was_pttp_functor(base, asserted_t,Begin-End),
78 forall(between(Begin,End,A),
79 map_int_functors(asserted_t,t,A,(use_mpred_t,baseKB:call_t)))). 80
81
83
84:- was_dynamic(int_pred_t/10). 85:- kb_shared(int_pred_t/10). 86
87:- map_int_functors(pred_t,t,3,((use_mpred_t, G=call_t,arg(1,G,B),arg(2,G,C),dif(B,C),G))). 93
95
96:- was_dynamic(int_not_pred_t/10). 97:- kb_shared(int_not_pred_t/10). 98
99:- map_int_functors(pred_t,t,3,((use_mpred_t, G=call_t,arg(1,G,B),arg(2,G,C),dif(B,C),G))). 100int_not_pred_t(A, B, C, H, I, D, E, F, J, G) :-
101 pretest_call((use_mpred_t,not(baseKB:t(A, B, C)), dif(B,C),D=E)),
102 F=[K, [not_pred_t(A, B, C), G, H, I]|L], J=[K|L].
103
104
106
107:- was_dynamic(int_not_true_t/10). 108:- kb_shared(int_not_true_t/10). 109
110int_not_true_t(A, B, C, H, I, D, E, F, J, G) :-
111 pretest_call((is_extent_known(A),use_mpred_t,not(baseKB:t(A, B, C)), dif(B,C),D=E)),
112 F=[K, [not_true_t(A, B, C), G, H, I]|L], J=[K|L].
113
114
116is_extent_known(wearsClothing).
117is_extent_known(Pred):-wrapper_for(Pred,pred_t).
118
119
121
122wrapper_for(reflexive,pred_isa_t).
123wrapper_for(irreflexive,pred_isa_t).
124wrapper_for(rtSymmetricBinaryPredicate,pred_isa_t).
125wrapper_for(antisymmetric,pred_isa_t).
126
127wrapper_for(genls,pred_t).
128wrapper_for(genls,pred_t).
129
130wrapper_for(skolem,call_builtin).
131
132wrapper_for(genlInverse,pred_t).
133wrapper_for(genlPreds,pred_t).
134wrapper_for(disjointWith,pred_t).
135wrapper_for(negationPreds,pred_t).
136wrapper_for(negationInverse,pred_t).
137
138
139
140:-
141 op(1199,fx,('==>')),
142 op(1190,xfx,('::::')),
143 op(1180,xfx,('==>')),
144 op(1170,xfx,'<==>'),
145 op(1160,xfx,('<-')),
146 op(1150,xfx,'=>'),
147 op(1140,xfx,'<='),
148 op(1130,xfx,'<=>'),
149 op(600,yfx,'&'),
150 op(600,yfx,'v'),
151 op(350,xfx,'xor'),
152 op(300,fx,'~'),
153 op(300,fx,'-'). 154
155
156pttp_logic(logicmoo_kb_logic,
157 ((
158 uses_logic(logicmoo_kb_refution),
159
160 (( genls(C1,C2) & pred_isa_t(C1,P) => pred_isa_t(C2,P) )),
161 (( pred_t(genls,C1,C2) & isa(I,C1) => isa(I,C2) )),
162
163 (( pred_t(disjointWith,C1,C2) => pred_isa_t(C1,P) v pred_isa_t(C2,P) )),
164 (( pred_t(disjointWith,C1,C2) => isa(I,C1) v isa(I,C2) )),
165
166 (( pred_t(genlPreds,P,PSuper) & true_t(P,A,B) => true_t(PSuper,A,B) )),
167 (( pred_t(genlPreds,P,PSuper) & not_true_t(PSuper,A,B) => not_true_t(P,A,B) )),
168 (( pred_t(genlInverse,P,PSuper) & true_t(P,A,B) => true_t(PSuper,B,A) )),
169 (( pred_t(negationPreds,P,PSuper) & true_t(P,A,B) => not_true_t(PSuper,A,B) )),
170 (( pred_t(negationInverse,P,PSuper) & true_t(P,A,B) => not_true_t(PSuper,B,A) )),
171
172 % (( pred_isa_t(predTransitive,P) & true_t(P,A,B) & true_t(P,B,C) => true_t(P,A,C) )),
173 % (( pred_isa_t(predReflexive,P) & true_t(P,A,B) => true_t(P,A,A) & true_t(P,B,B) )),
174 % (( pred_isa_t(predSymmetric,P) & true_t(P,A,B) => true_t(P,B,A) ))
175 (( pred_isa_t(predIrreflexive,P) & true_t(P,A,B) => not_true_t(P,B,A) ))
176 % (( pred_isa_t(predIrreflexive,PSuper) & pred_t(genlInverse,PSuper,P) => pred_isa_t(predIrreflexive,P) )),
177 % (( pred_isa_t(predIrreflexive,PSuper) & pred_t(genlPreds,P,PSuper) => pred_isa_t(predIrreflexive,P) ))
178 ))).
179
180
181% all questions (askable_t) to the KB are
182
183pttp_logic(logicmoo_kb_refution,
184 ((
185
186 % TODO define askable_t
187 (( asserted_t(P,A,B) => true_t(P,A,B) )),
188 (( true_t(P,A,B) => assumed_t(P,A,B) )),
189 (( assumed_t(P,A,B) => -not_true_t(P,A,B) & -fallacy_t(P,A,B) )),
190 (( possible_t(P,A,B) => -not_true_t(P,A,B) & -fallacy_t(P,A,B) )),
191
192 (( true_t(P,A,B) & not_true_t(P,A,B) => fallacy_t(P,A,B) )),
193
194 (( true_t(P,A,B) => -not_true_t(P,A,B) & possible_t(P,A,B) & -unknown_t(P,A,B) )),
195 (( not_true_t(P,A,B) <=> -true_t(P,A,B) & -possible_t(P,A,B) & -unknown_t(P,A,B) )),
196 (( askable_t(P,A,B) => true_t(P,A,B) v unknown_t(P,A,B) v not_true_t(P,A,B) )),
197 (( answerable_t(P,A,B) <=> askable_t(P,A,B) & -unknown_t(P,A,B) )),
198 (( askable_t(P,A,B) <=> -fallacy_t(P,A,B) )),
199 (( answerable_t(P,A,B) => true_t(P,A,B) v -true_t(P,A,B) )),
200 (( true_t(P,A,B) v unknown_t(P,A,B) v not_true_t(P,A,B) ))
201
202
203
204 % TODO define askable_t
205/*
206 (( fallacy_t(P,A,B) => not_true_t(P,A,B) & true_t(P,A,B) & -unknown_t(P,A,B) & -possible_t(P,A,B) )),
207
208 (( unknown_t(P,A,B) => -true_t(P,A,B) & possible_t(P,A,B) & -asserted_t(P,A,B) & -not_true_t(P,A,B) )),
209
210 (( -unknown_t(P,A,B) => true_t(P,A,B) v not_true_t(P,A,B) )),
211 (( -asserted_t(P,A,B) => possible_t(P,A,B) v not_true_t(P,A,B) v fallacy_t(P,A,B) )),
212 (( -true_t(P,A,B) => not_true_t(P,A,B) v fallacy_t(P,A,B) v possible_t(P,A,B) )),
213 (( -possible_t(P,A,B) => not_true_t(P,A,B) v fallacy_t(P,A,B) )),
214 (( -not_true_t(P,A,B) => fallacy_t(P,A,B) v unknown_t(P,A,B) v true_t(P,A,B) )),
215 (( -fallacy_t(P,A,B) => unknown_t(P,A,B) v not_true_t(P,A,B) v true_t(P,A,B) ))
216
217 */
218
219 % (( askable_t(P,A,B) v fallacy_t(P,A,B) )),
220
221 ))).
222
223pttp_logic(logicmoo_kb_refution_between_mts,
224 ((
225
226 % TODO define askable_t
227 (( ist(MT1,asserted_t(P,A,B)) & genlMt(MT1,MT2) => ist(MT2,true_t(P,A,B)) )),
228 (( true_t(P,A,B) => assumed_t(P,A,B) )),
229 (( assumed_t(P,A,B) => -not_true_t(P,A,B) & -fallacy_t(P,A,B) )),
230 (( possible_t(P,A,B) => -not_true_t(P,A,B) & -fallacy_t(P,A,B) )),
231
232 (( true_t(P,A,B) & not_true_t(P,A,B) => fallacy_t(P,A,B) )),
233
234 (( true_t(P,A,B) => -not_true_t(P,A,B) & possible_t(P,A,B) & -unknown_t(P,A,B) )),
235 (( not_true_t(P,A,B) <=> -true_t(P,A,B) & -possible_t(P,A,B) & -unknown_t(P,A,B) )),
236 (( ist(MT1,askable_t(P,A,B)) & genlMt(MT1,MT2) => ist(MT1, (true_t(P,A,B) v unknown_t(P,A,B) v not_true_t(P,A,B) )))),
237 (( answerable_t(P,A,B) <=> askable_t(P,A,B) & -unknown_t(P,A,B) )),
238 (( askable_t(P,A,B) <=> -fallacy_t(P,A,B) )),
239 (( answerable_t(P,A,B) => true_t(P,A,B) v not_true_t(P,A,B) )),
240 (( true_t(P,A,B) v unknown_t(P,A,B) v not_true_t(P,A,B) ))
241
242
243
244 % TODO define askable_t
245/*
246 (( fallacy_t(P,A,B) => not_true_t(P,A,B) & true_t(P,A,B) & -unknown_t(P,A,B) & -possible_t(P,A,B) )),
247
248 (( unknown_t(P,A,B) => -true_t(P,A,B) & possible_t(P,A,B) & -asserted_t(P,A,B) & -not_true_t(P,A,B) )),
249
250 (( -unknown_t(P,A,B) => true_t(P,A,B) v not_true_t(P,A,B) )),
251 (( -asserted_t(P,A,B) => possible_t(P,A,B) v not_true_t(P,A,B) v fallacy_t(P,A,B) )),
252 (( -true_t(P,A,B) => not_true_t(P,A,B) v fallacy_t(P,A,B) v possible_t(P,A,B) )),
253 (( -possible_t(P,A,B) => not_true_t(P,A,B) v fallacy_t(P,A,B) )),
254 (( -not_true_t(P,A,B) => fallacy_t(P,A,B) v unknown_t(P,A,B) v true_t(P,A,B) )),
255 (( -fallacy_t(P,A,B) => unknown_t(P,A,B) v not_true_t(P,A,B) v true_t(P,A,B) ))
256
257 */
258
259 % (( askable_t(P,A,B) v fallacy_t(P,A,B) )),
260
261 ))).
262
263
264
266
267make_base(BF,A):-
268 negated_functor(BF,NF),
269 negated_functor(NF,PF),
270 atom_concat('int_',PF,IPF),
271 atom_concat('int_',NF,INF),
272 EA is A + 6,
273 IA is A + 7,
274 dynamic(IPF/IA),dynamic(INF/IA),dynamic(PF/EA),dynamic(NF/EA),
275 export(IPF/IA),export(INF/IA),export(PF/EA),export(NF/EA),
276
277 functor(PFB,PF,A),
278 PFB=..[PF|ARGS],
279 NFB=..[NF|ARGS],
280 IPFB=..[IPF|ARGS],
281 INFB=..[INF|ARGS],
282 SUBST_L=[pfb=PFB,nfb=NFB,ipfb=IPFB,infb=INFB],
283
284 subst_each(
285[was_pttp_functor(internal,IPF,IA),
286 was_pttp_functor(internal,INF,IA),
287 was_pttp_functor(external,PF,EA),
288 was_pttp_functor(external,NF,EA),
289
290 (pfb(F, E, H, G, I, J) :-
291 D=nfb, ( identical_member_special_loop_check(D, E)
292 -> fail
293 ; ( identical_member_cheaper(D, F), !
294 ; unifiable_member_cheaper(D, F)
295 ), G=H, I=[K, [redn, D, F, E]|L], J=[K|L]
296 ; ipfb(F, E, H, G, I, J, D)
297 )),
298(pfb(F, E, H, G, I, J) :-
299 D=nfb, ( identical_member_special_loop_check(D, E)
300 -> fail
301 ; ( identical_member_cheaper(D, F), !
302 ; unifiable_member_cheaper(D, F)
303 ), G=H, I=[K, [redn, D, F, E]|L], J=[K|L]
304 ; fail
305 )),
306(nfb(F, E, H, G, I, J) :-
307 D=pfb, ( identical_member_special_loop_check(D, E)
308 -> fail
309 ; ( identical_member_cheaper(D, F), !
310 ; unifiable_member_cheaper(D, F)
311 ), G=H, I=[K, [redn, D, F, E]|L], J=[K|L]
312 ; fail
313 )),
314(nfb(F, E, H, G, I, J) :-
315 D=pfb, ( identical_member_special_loop_check(D, E)
316 -> fail
317 ; ( identical_member_cheaper(D, F), !
318 ; unifiable_member_cheaper(D, F)
319 ), G=H, I=[K, [redn, D, F, E]|L], J=[K|L]
320 ; infb(F, E, H, G, I, J, D)
321 ))],SUBST_L,NEW),
322 must_maplist(assert_if_new,NEW).
323
324
326:- forall(was_pttp_functor(base,F,S-E),forall(between(S,E,A),must(make_base(F,A)))). 327
329
331
333
335
336
337:- fixup_exports.