18
19:- ensure_loaded(base). 20:- ensure_loaded(pttp). 21:- ensure_loaded(builtin). 22:- ensure_loaded(model). 23:- ensure_loaded(io). 24:- ensure_loaded(db). 25:- ensure_loaded(herbrand). 26:- ensure_loaded(hooks). 27:- ensure_loaded(lemma). 28:- ensure_loaded(xray_config). 29
32
36
37clauses((A , B),L,WffNum) :-
38 !,
39 clauses(A,L1,WffNum),
40 WffNum2 is WffNum + 1,
41 clauses(B,L2,WffNum2),
42 conjoin(L1,L2,L).
43clauses( (Gamma :- Alpha : Beta) , L , WffNum ) :-
44 !,
45 clauses((Gamma :- gamma(WffNum,Gamma)),L1,WffNum),
46 clauses((alpha(WffNum,Alpha) :- Alpha),L2,WffNum),
47 conjoin(L1,L2,L3),
48 conjoin(Gamma,Beta,C0), 49 cnf(C0,C1),
50 make_matrix(C1,C2),
51 matrix_reduction(C2,Justification),
52 (delta_ordering(compatibility>admissibility) ->
53 conjoin(justification(Justification),
54 alpha(WffNum,Alpha),
55 Body);
56 57 conjoin(alpha(WffNum,Alpha),
58 justification(Justification),
59 Body)),
60 (compile_proof_printing ->
61 Record = infer_by(default(WffNum:(Gamma :- Alpha : Justification)));
62 63 Record = true),
64 conjoin(Record,Body,Body1),
65 DRule= (gamma(WffNum,Gamma) :- Body1),
66 conjoin(DRule,L3,L).
67
68clauses(A,L,WffNum) :-
69 head_literals(A,Lits),
70 clauses(A,Lits,L,WffNum).
71
72clauses(A,[Lit|Lits],L,WffNum) :-
73 body_for_head_literal(Lit,A,Body1),
74 ((compile_proof_printing,Body1 = true) ->
75 Record = infer_by(unit(WffNum:Lit));
76 compile_proof_printing ->
77 Record = infer_by(extension(WffNum:Lit));
78 79 Record = true),
80 conjoin(Record,Body1,Body),
81 clauses(A,Lits,L1,WffNum),
82 conjoin((Lit :- Body),L1,L).
83clauses(_,[],true,_).
84
88
89add_ancestor((Head :- Body),(Head1 :- Body1)) :-
90 functor(Head,query,_) ->
91 Head1 = Head,
92 add_ancestor_args(Body,[[],[],[]],Body1);
93 functor(Head,gamma,_) ->
94 Head =.. L,
95 append(L,[_,_,Defaults],L1),
96 Head1 =.. L1,
97 add_ancestor_args(Body,[[],[],NewDefaults],Body2),
98 conjoin((NewDefaults = [Head|Defaults]),Body2,Body1);
99 functor(Head,alpha,_) ->
100 Head =.. L,
101 append(L,[_,_,Defaults],L1),
102 Head1 =.. L1,
103 add_ancestor_args(Body,[[],[],Defaults],Body1);
104 105 Head =.. L,
106 append(L,[PosAncestors,NegAncestors,Defaults],L1),
107 Head1 =.. L1,
108 add_ancestor_args(Body,[NewPosAncestors,NewNegAncestors,Defaults],Body2),
109 (Body == Body2 ->
110 Body1 = Body2;
111 negative_literal(Head) ->
112 NewPosAncestors = PosAncestors,
113 conjoin((NewNegAncestors = [Head|NegAncestors]),Body2,Body1);
114 115 NewNegAncestors = NegAncestors,
116 conjoin((NewPosAncestors = [Head|PosAncestors]),Body2,Body1)).
117
118
119ancestor_tests(P,N,Result) :-
120 P == query ->
121 Result = true;
122 P == gamma ->
123 Head = gamma(DefaultID,DefaultConseq,_,_,Defaults),
124 Default = gamma(DefaultID,DefaultConseq),
125 Result = (Head :- identical_member(Default,Defaults), !, fail);
126 P == alpha ->
127 Result = true; 128 129 negated_functor(P,NotP),
130 N3 is N - 3, 131 functor(Head1,P,N3),
132 Head1 =.. [P|Args1],
133 Head2 =.. [NotP|Args1],
134 append(Args1,[PosAncestors,NegAncestors,_],Args),
135 Head =.. [P|Args],
136 (negative_functor(P) ->
137 C1Ancestors = NegAncestors,
138 C2Ancestors = PosAncestors;
139 140 C1Ancestors = PosAncestors,
141 C2Ancestors = NegAncestors),
142 C1 = (Head :- identical_member(Head1,C1Ancestors), !, fail),
143 count_inferences_pred(IncNcalls),
144 (N3 = 0 -> 145 conjoin((identical_member(Head2,C2Ancestors) , !),IncNcalls,V);
146 147 conjoin(unifiable_member(Head2,C2Ancestors),IncNcalls,V)),
148 (compile_proof_printing ->
149 conjoin(V,infer_by(reduction(Head2)),V1);
150 151 V1 = V),
152 C2 = (Head :- V1),
153 conjoin(C1,C2,Result).
154
155
156procedures_with_tests([[P,N]|Preds],Clauses,Procs) :-
157 procedure(P,N,Clauses,Proc0),
158
159 ancestor_tests(P,N,TestsA),
160 lemma_tests(P,N,TestsL),
161 conjoin(TestsA,TestsL,Tests),
162
163 phook_tests(P,N,Tests,Proc0,ProcP),
164
165 procedures_with_tests(Preds,Clauses,ProcsPs),
166 conjoin(ProcP,ProcsPs,Procs).
167procedures_with_tests([],_Clauses,true).
168
169
178
179add_consistency_checking((Head :- Body),(Head1 :- Body1)) :-
180 functor(Head,query,_) ->
181 Head1 = Head,
182 conjoin(model_initialization(MM0),Body,Body2),
183 add_consistency_checking_args(Body2,MM0,MMOut,Body1);
184 185 Head =.. L,
186 append(L,[MMIn,MMOut],L1),
187 Head1 =.. L1,
188 add_consistency_checking_args(Body,MMIn,MMOut,Body1).
189
190add_consistency_checking_args(Body,MMIn,MMOut,Body1) :-
191 Body = (A , B) ->
192 add_consistency_checking_args(A,MMIn,MMIn1,A1),
193 add_consistency_checking_args(B,MMIn1,MMOut,B1),
194 conjoin(A1,B1,Body1);
195 Body = (A ; B) ->
196 add_consistency_checking_args(A,MMIn,MMOut,A1),
197 add_consistency_checking_args(B,MMIn,MMOut,B1),
198 disjoin(A1,B1,Body1);
199 Body =.. [search,Goal|L] ->
200 add_consistency_checking_args(Goal,MMIn,MMOut,Goal1), 201 Body1 =.. [search,Goal1|L];
202 Body = justification(X) ->
203 Body1 = compatible(X,MMIn,MMOut);
204 Body = fail ->
205 Body1 = Body;
206 builtin(Body) ->
207 MMIn = MMOut,
208 Body1 = Body;
209 210 Body =.. L,
211 append(L,[MMIn,MMOut],L1),
212 Body1 =.. L1.
213
214add_model_structure(WffI,Q,C,WffO) :-
215 WffI = (A , B) ->
216 add_model_structure(A,Q,C,A1),
217 add_model_structure(B,Q,C,B1),
218 conjoin(A1,B1,WffO);
219 WffI = (A ; B) ->
220 add_model_structure(A,Q,C,A1),
221 add_model_structure(B,Q,C,B1),
222 disjoin(A1,B1,WffO);
223 WffI = (A :- B) ->
224 add_model_structure(B,Q,C,B1),
225 WffO = (A :- B1);
226 WffI = model_initialization(Var) ->
227 combine_clauses(Q,C,Matrix),
228 WffO = model_initialization(Matrix,Var);
229 230 WffO = WffI.
231
232classical_clauses(WffI,WffO) :-
233 WffI = (A , B) ->
234 classical_clauses(A,A1),
235 classical_clauses(B,B1),
236 conjoin(A1,B1,WffO);
237 WffI = (A ; B) ->
238 classical_clauses(A,A1),
239 classical_clauses(B,B1),
240 disjoin(A1,B1,WffO);
241 WffI = (A :- B) -> 242 WffO = true;
243 builtin(WffI) ->
244 WffO = true;
245 246 WffI = WffO.
247
248query_clause(WffI,WffO) :-
249 WffI = (A , B) ->
250 (query_clause(A,WffO);
251 query_clause(B,WffO));
252 WffI = (A ; B) ->
253 (query_clause(A,WffO);
254 query_clause(B,WffO));
255 WffI = (A :- B) ->
256 (A = query ->
257 classical_clauses(B,WffO);
258 259 fail);
260 261 fail.
262
263query(M) :- 264 (compile_complete_search, compile_proof_printing , lemma_handling_flag) ->
265 query(M,_N,_LemProof,_LemProofEnd,_Proof,_ProofEnd);
266 (compile_complete_search, (compile_proof_printing ; lemma_handling_flag)) ->
267 query(M,_N,_Proof,_ProofEnd);
268 compile_complete_search ->
269 query(M,_N).
270
271query :- 272 (compile_complete_search ->
273 query(1000000);
274 275 ((compile_proof_printing , lemma_handling_flag) ->
276 query(_LemProof,_LemProofEnd,_Proof,_ProofEnd);
277 (compile_proof_printing ; lemma_handling_flag) ->
278 query(Proof,_ProofEnd);
279 280 query)).
281
282
283
287
288xray(Name) :-
289 read_kb(Name,KB),
290 dpttp(Name,KB).
291
292
293dpttp(Name,X) :-
294 time(dpttp1(X,Y:Z),'Compilation Phase I'),
295 time(dpttp2(Name,Y:Z),'Compilation Phase II'),
296 time(dpttp3(Name),'Compilation Phase III').
297
298dpttp(X) :-
299 Name = 'temp',
300 dpttp(Name,X).
301
302dpttp1(X,Y:C) :-
303 nl,
304 write('XRay input formulas:'),
305 apply_to_conjuncts(X,write_clause,_),
306 nl,
307
308 constants(X,H),
309 (H = [] ->
310 nl,write('Empty Herbrand universe.'),nl;
311 312 nl,write('Herbrand universe':H),nl),
313
314 classical_clauses(X,C0),
315 cnf(C0,C1),
316 make_matrix(C1,C2),
317 instantiation(C2,H,C3),
318 matrix_reduction(C3,C),
319
320 (verbose_flag ->
321 nl,
322 write('Classical output formulas:'),
323 apply_to_list(C,write_clause,_),
324 nl;
325 326 true),
327
328 dpttp1(X,C,Y:C).
329
330dpttp1(X,C,Y:C) :-
331 query_clause(X,Q0),
332 variables(Q0,Vars),
333 (Vars=[] ->
334 cnf(Q0,Q1),
335 make_matrix(Q1,Q2),
336 matrix_reduction(Q2,Q),
337
338 XQ=X;
339 340 Q = [],
341
342 apply_to_conjuncts(X,add_answer_preds,XQ)),
343
344 (verbose_flag ->
345 nl,
346 write('Query formula:'),
347 apply_to_conjuncts(Q0,write_clause,_),
348 nl,
349 write(' compiled:'),
350 apply_to_list(Q,write_clause,_),
351 nl,nl;
352 353 true),
354
355 dpttp1(XQ,Q,C,Y:C).
356
357dpttp1(X,Q,C,Y:C) :-
358 clauses(X,XC,1),
359
360 constants(X,H),
361 (H = [] ->
362 XH=true,
363 X0=XC;
364 365 herbrand_preds(H,XH),
366 apply_to_conjuncts(XC,add_herbrand_preds,X0)),
367
368 apply_to_conjuncts(X0,add_count_inferences,X1),
369 apply_to_conjuncts(X1,add_ancestor,X2),
370 predicates(X2,Preds0),
371 reverse(Preds0,Preds),
372 procedures_with_tests(Preds,X2,X3),
373 374 apply_to_conjuncts(X3,add_sound_unification,X4),
375 apply_to_conjuncts(X4,add_consistency_checking,X5),
376 (compile_complete_search ->
377 apply_to_conjuncts(X5,add_complete_search,X6);
378 379 X5=X6),
380 apply_to_conjuncts(X6,add_lemmatization,XL), 381 (compile_proof_printing ->
382 apply_to_conjuncts(XL,add_proof_recording,X7);
383 384 X7 = XL),
385 add_model_structure(X7,Q,C,X8),
386
387 apply_to_conjuncts(X8,add_body_hooks,XD),
388
389 apply_to_conjuncts(X,prolog_clause,XP),
390 conjoin(XP,XD,XR),
391
392 conjoin(XH,XR,Y),
393
394 (verbose_flag ->
395 nl,
396 write('XRay output formulas:'),
397 apply_to_conjuncts(Y,write_clause,_),
398 nl;
399 400 true),
401 !.
402
403dpttp1(X) :-
404 dpttp1(X,_).
405
406dpttp2(Name,Y:Z) :-
407 nl,
408 write('XRay writing compiled clauses ... '),
409 write_ckb(Name,Y),
410 write_cmm(Name,Z),
411 write('done.'),
412 !.
413
414dpttp2(Y:Z) :-
415 Name = 'temp',
416 dpttp2(Name,Y:Z).
417
418dpttp3(Name) :-
419 nl,
420 write('XRay compiling clauses ... '),
421 compile_ckb(Name),
422 write('done.'),
423 nl,
424 write('XRay compiling query ... '),
425 compile_query(Name),
426 write('done.'),
427 nl,
428 !.
429dpttp3 :-
430 Name = 'temp',
431 dpttp3(Name)