18
22:- multifile setting_trill_default/2. 23setting_trill_default(det_rules,[and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule]).
24setting_trill_default(nondet_rules,[or_rule]).
25
26set_up(M):-
27 utility_translation:set_up(M),
28 M:(dynamic exp_found/2, keep_env/0, tornado_bdd_environment/1, inconsistent_theory_flag/0, setting_trill/2, tab_end/1, query_option/2),
29 retractall(M:setting_trill(_,_)),
30 retractall(M:query_option(_,_)),
31 retractall(M:tab_end(_)).
32 33 34 35
36clean_up(M):-
37 utility_translation:clean_up(M),
38 M:(dynamic exp_found/2, keep_env/0, tornado_bdd_environment/1, inconsistent_theory_flag/0, setting_trill/2, tab_end/1, query_option/2),
39 retractall(M:exp_found(_,_)),
40 retractall(M:keep_env),
41 retractall(M:tornado_bdd_environment(_)),
42 retractall(M:inconsistent_theory_flag),
43 retractall(M:setting_trill(_,_)),
44 retractall(M:query_option(_,_)),
45 retractall(M:tab_end(_)).
46
50:- multifile prolog:message/1. 51
52prolog:message(or_in_or) -->
53 [ 'Boolean formula wrongly built: or in or' ].
54
55prolog:message(and_in_and) -->
56 [ 'Boolean formula wrongly built: and in and' ].
57
61
65
67find_n_explanations(M,QueryType,QueryArgs,Expls,_):- 68 assert(M:keep_env),
69 find_single_explanation(M,QueryType,QueryArgs,Expls),!.
70
71find_n_explanations(M,_,_,Expls,_):-
72 initial_expl(M,Expls-_).
73
74
75compute_prob_and_close(M,Exps-_,QueryOptions):-
76 M:query_option(compute_prob,CPType),!,
77 get_from_query_options(QueryOptions,compute_prob,CPType,Prob),
78 compute_prob(M,Exps,Prob),!,
79 retractall(M:keep_env),!.
80
81compute_prob_and_close(_M,_,_):-!.
82
84check_and_close(M,Expl,Expl):-
85 M:keep_env,!.
86
87check_and_close(M,Expl,dot(Dot)):-
88 get_bdd_environment(M,Env),
89 create_dot_string(Env,Expl,Dot),
90 clean_environment(M,Env).
91
92is_expl(M,Expl-_):-
93 initial_expl(M,EExpl-_),
94 dif(Expl,EExpl).
95
96
97find_expls(M,_,_,_):-
98 (M:inconsistent_theory_flag -> print_message(warning,inconsistent) ; true),!,false.
99
101find_expls_from_tab_list(M,[],BDD):-
102 empty_expl(M,BDD),!.
103
105find_expls_from_tab_list(M,[Tab|T],E):-
106 get_solved_clashes(Tab,Clashes),
107 findall(E0,(member(Clash,Clashes),clash(M,Clash,Tab,E0)),Expls0),!,
108 109 consistency_check(M,Expls0,Q),
110 ( dif(Q,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)),
111 or_all_f(M,Expls0,Expls1),
112 find_expls_from_tab_list(M,T,E1),
113 and_f(M,Expls1,E1,E).
114
115 find_expls_from_tab_list(M,[_Tab|T],Expl):-
116 \+ length(T,0),
117 find_expls_from_tab_list(M,T,Expl).
118
120consistency_check(_,[],qp):-!.
121
122consistency_check(M,[_-CPs|T],Q):-
123 dif(CPs,[]),!,
124 member(qp,CPs),!,
125 consistency_check(M,T,Q).
126
127consistency_check(M,_,['inconsistent','kb']):-!,
128 assert(M:inconsistent_theory_flag).
129
131
135
137findClassAssertion4OWLNothing(M,ABox,Expl):-
138 findall(Expl1,findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl1,ABox),Expls),
139 dif(Expls,[]),
140 or_all_f(M,Expls,Expl).
141
143
148modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
149 length(LF,1),!.
150
151modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
152 get_abox(Tab0,ABox0),
153 find((sameIndividual(L),Expl1),ABox0),!,
154 sort(L,LS),
155 sort(LF,LFS),
156 LS = LFS,!,
157 dif(L0,Expl1),
158 test(M,L0,Expl1,Expl),
159 remove_from_abox(ABox0,[(sameIndividual(L),Expl1)],ABox),
160 set_abox(Tab0,[(sameIndividual(L),Expl)|ABox],Tab).
161
162modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
163 add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
164 get_abox(Tab0,ABox0),
165 set_abox(Tab1,[(sameIndividual(LF),L0)|ABox0],Tab).
166
167modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
168 length(LF,1),!.
169
170modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
171 get_abox(Tab0,ABox0),
172 find((sameIndividual(L),Expl1),ABox0),!,
173 sort(L,LS),
174 sort(LF,LFS),
175 LS = LFS,!,
176 dif(L0,Expl1),
177 test(M,L0,Expl1,Expl),
178 remove_from_abox(ABox0,[(differentIndividuals(L),Expl1)],ABox),
179 set_abox(Tab0,[(differentIndividuals(L),Expl)|ABox],Tab).
180
181modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
182 add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
183 get_abox(Tab0,ABox),
184 set_abox(Tab1,[(differentIndividuals(LF),L0)|ABox],Tab).
185
186modify_ABox(M,Tab0,C,Ind,L0,Tab):-
187 get_abox(Tab0,ABox0),
188 findClassAssertion(C,Ind,Expl1,ABox0),!,
189 dif(L0,Expl1),
190 test(M,L0,Expl1,Expl),
191 remove_from_abox(ABox0,(classAssertion(C,Ind),Expl1),ABox),
192 set_abox(Tab0,[(classAssertion(C,Ind),Expl)|ABox],Tab1),
193 update_expansion_queue_in_tableau(M,C,Ind,Tab1,Tab).
194
195modify_ABox(M,Tab0,C,Ind,L0,Tab):-
196 add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
197 get_abox(Tab0,ABox),
198 set_abox(Tab1,[(classAssertion(C,Ind),L0)|ABox],Tab2),
199 update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
200
201
202modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
203 get_abox(Tab0,ABox0),
204 findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox0),!,
205 dif(L0,Expl1),
206 test(M,L0,Expl1,Expl),
207 remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl1),ABox),
208 set_abox(Tab0,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab1),
209 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab1,Tab).
210
211
212modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
213 add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
214 get_abox(Tab0,ABox0),
215 set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),L0)|ABox0],Tab2),
216 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
217
219
220
225
226build_abox(M,Tableau,QueryType,QueryArgs):-
227 retractall(M:final_abox(_)),
228 retractall(v(_,_,_)),
229 retractall(na(_,_)),
230 retractall(rule_n(_)),
231 assert(rule_n(0)),
232 get_bdd_environment(M,Env),
233 collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
234 ( dif(ConnectedInds,[]) ->
235 ( findall((classAssertion(Class,Individual),BDDCA-[]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
236 findall((propertyAssertion(Property,Subject, Object),BDDPA-[]),(member(Subject,ConnectedInds),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property),bdd_and(M,Env,[propertyAssertion(Property,Subject, Object)],BDDPA)),LPA),
237 238 findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
239 findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
240 findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),intersect(L,ConnectedInds),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
241 )
242 ; 243 ( findall((classAssertion(Class,Individual),BDDCA-[]),(M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
244 findall((propertyAssertion(Property,Subject, Object),BDDPA-[]),(M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property),bdd_and(M,Env,[propertyAssertion(Property,Subject, Object)],BDDPA)),LPA),
245 246 findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
247 findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
248 findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
249 )
250 ),
251 new_abox(ABox0),
252 new_tabs(Tabs0),
253 init_expansion_queue(LCA,LPA,ExpansionQueue),
254 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
255 append([LCA,LDIA,LPA],CreateTabsList),
256 create_tabs(CreateTabsList,Tableau0,Tableau1),
257 append([LCA,LPA,LNA,LDIA],AddAllList),
258 add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
259 merge_all_individuals(M,LSIA,Tableau2,Tableau3),
260 add_owlThing_list(M,Tableau3,Tableau),
261 !.
262
268
269initial_expl(M,BDD-[]):-
270 get_bdd_environment(M,Env),
271 zero(Env,BDD).
272
273empty_expl(M,BDD-[]):-
274 get_bdd_environment(M,Env),
275 one(Env,BDD).
276
277and_f_ax(M,Axiom,BDD0,BDD):-
278 get_bdd_environment(M,Env),
279 bdd_and(M,Env,[Axiom],BDDAxiom),
280 and_f(M,BDDAxiom-[],BDD0,BDD).
281
283and_f(_,[],BDD,BDD):- !.
284
285and_f(_,BDD,[],BDD):- !.
286
287and_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
288 get_bdd_environment(M,Env),
289 and(Env,BDD0,BDD1,BDD),
290 append(CP0,CP1,CP).
291
292
294or_all_f(M,[],BDD):-
295 initial_expl(M,BDD),!.
296
297or_all_f(M,[H|T],Expl):-
298 or_all_f(M,T,Expl1),
299 or_f(M,H,Expl1,Expl),!.
300
301or_f(_,[],BDD,BDD):- !.
302
303or_f(_,BDD,[],BDD):- !.
304
305or_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
306 get_bdd_environment(M,Env),
307 or(Env,BDD0,BDD1,BDD),
308 append(CP0,CP1,CP).
309
310
316
317test(M,L1,L2-CP2,F-CP):-
318 319 320 or_f(M,L1,L2-CP2,F-CP),
321 dif(L2,F).
322
323
329
330get_choice_point_id(_,0).
331
332create_choice_point(_,_,_,_,_,0).
333
334add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
335 (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
336
337add_choice_point(_,_,Expl,Expl):- !.
338
339
345
346get_bdd_environment(M,Env):-
347 M:tornado_bdd_environment(Env),!.
348
349get_bdd_environment(M,Env):-
350 init(Env),
351 M:assert(tornado_bdd_environment(Env)).
352
353clean_environment(M,Env):-
354 end(Env),
355 retractall(M:tornado_bdd_environment(_)).
356
357build_bdd(_,Env,[],BDD):- !,
358 zero(Env,BDD).
359
360build_bdd(_,_Env,BDD,BDD).
361
362bdd_and(M,Env,[X],BDDX):-
363 get_prob_ax(M,X,AxN,Prob),!,
364 ProbN is 1-Prob,
365 get_var_n(Env,AxN,[],[Prob,ProbN],VX),
366 equality(Env,VX,0,BDDX),!.
367
368bdd_and(_M,Env,[_X],BDDX):- !,
369 one(Env,BDDX)