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).
29 30 31 32
33clean_up(M):-
34 utility_translation:clean_up(M),
35 M:(dynamic exp_found/2, keep_env/0, tornado_bdd_environment/1, inconsistent_theory_flag/0, setting_trill/2),
36 retractall(M:exp_found(_,_)),
37 retractall(M:keep_env),
38 retractall(M:tornado_bdd_environment(_)),
39 retractall(M:inconsistent_theory_flag),
40 retractall(M:setting_trill(_,_)).
41
45:- multifile prolog:message/1. 46
47prolog:message(or_in_or) -->
48 [ 'Boolean formula wrongly built: or in or' ].
49
50prolog:message(and_in_and) -->
51 [ 'Boolean formula wrongly built: and in and' ].
52
56
60
62find_n_explanations(M,QueryType,QueryArgs,Expls,_,Opt):- 63 assert(M:keep_env),
64 find_single_explanation(M,QueryType,QueryArgs,Expls,Opt),!.
65
66find_n_explanations(M,_,_,Expls,_,_):-
67 initial_expl(M,Expls-_).
68
69compute_prob_and_close(M,Exps,Prob):-
70 compute_prob(M,Exps,Prob),
71 retractall(M:keep_env),!.
72
74check_and_close(M,Expl,Expl):-
75 M:keep_env,!.
76
77check_and_close(M,Expl,dot(Dot)):-
78 get_bdd_environment(M,Env),
79 create_dot_string(Env,Expl,Dot),
80 clean_environment(M,Env).
81
82is_expl(M,Expl):-
83 initial_expl(M,EExpl-_),
84 dif(Expl,EExpl).
85
86
87find_expls(M,Tabs,Q,E):-
88 find_expls_int(M,Tabs,Q,E-_),!.
89
90find_expls(M,_,_,_):-
91 M:inconsistent_theory_flag,!,
92 print_message(warning,inconsistent),!,false.
93
95find_expls_int(M,[],_,BDD):-
96 empty_expl(M,BDD),!.
97
99find_expls_int(M,[Tab|T],Q,E):-
100 get_clashes(Tab,Clashes),
101 findall(E0,(member(Clash,Clashes),clash(M,Clash,Tab,E0)),Expls0),!,
102 103 consistency_check(M,Expls0,Q),
104 or_all_f(M,Expls0,Expls1),
105 find_expls_int(M,T,Q,E1),
106 and_f(M,Expls1,E1,E).
107
108find_expls_int(M,[_Tab|T],Query,Expl):-
109 \+ length(T,0),
110 find_expls_int(M,T,Query,Expl).
111
113consistency_check(_,_,['inconsistent','kb']):-!.
114
115consistency_check(_,[],_):-!.
116
117consistency_check(M,[_-CPs|T],Q):-
118 dif(CPs,[]),!,
119 consistency_check(M,T,Q).
120
121consistency_check(M,_,_):-
122 assert(M:inconsistent_theory_flag).
123
125
129
131findClassAssertion4OWLNothing(M,ABox,Expl):-
132 findall(Expl1,findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl1,ABox),Expls),
133 dif(Expls,[]),
134 or_all_f(M,Expls,Expl).
135
137
142modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
143 length(LF,1),!.
144
145modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
146 get_abox(Tab0,ABox0),
147 find((sameIndividual(L),Expl1),ABox0),!,
148 sort(L,LS),
149 sort(LF,LFS),
150 LS = LFS,!,
151 dif(L0,Expl1),
152 test(M,L0,Expl1,Expl),
153 remove_from_abox(ABox0,[(sameIndividual(L),Expl1)],ABox),
154 set_abox(Tab0,[(sameIndividual(L),Expl)|ABox],Tab).
155
156modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
157 add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
158 get_abox(Tab0,ABox0),
159 set_abox(Tab1,[(sameIndividual(LF),L0)|ABox0],Tab).
160
161modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
162 length(LF,1),!.
163
164modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
165 get_abox(Tab0,ABox0),
166 find((sameIndividual(L),Expl1),ABox0),!,
167 sort(L,LS),
168 sort(LF,LFS),
169 LS = LFS,!,
170 dif(L0,Expl1),
171 test(M,L0,Expl1,Expl),
172 remove_from_abox(ABox0,[(differentIndividuals(L),Expl1)],ABox),
173 set_abox(Tab0,[(differentIndividuals(L),Expl)|ABox],Tab).
174
175modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
176 add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
177 get_abox(Tab0,ABox),
178 set_abox(Tab1,[(differentIndividuals(LF),L0)|ABox],Tab).
179
180modify_ABox(M,Tab0,C,Ind,L0,Tab):-
181 get_abox(Tab0,ABox0),
182 findClassAssertion(C,Ind,Expl1,ABox0),!,
183 dif(L0,Expl1),
184 test(M,L0,Expl1,Expl),
185 remove_from_abox(ABox0,(classAssertion(C,Ind),Expl1),ABox),
186 set_abox(Tab0,[(classAssertion(C,Ind),Expl)|ABox],Tab1),
187 update_expansion_queue_in_tableau(M,C,Ind,Tab1,Tab).
188
189modify_ABox(M,Tab0,C,Ind,L0,Tab):-
190 add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
191 get_abox(Tab0,ABox),
192 set_abox(Tab1,[(classAssertion(C,Ind),L0)|ABox],Tab2),
193 update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
194
195
196modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
197 get_abox(Tab0,ABox0),
198 findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox0),!,
199 dif(L0,Expl1),
200 test(M,L0,Expl1,Expl),
201 remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl1),ABox),
202 set_abox(Tab0,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab1),
203 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab1,Tab).
204
205
206modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
207 add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
208 get_abox(Tab0,ABox0),
209 set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),L0)|ABox0],Tab2),
210 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
211
213
214
219
220build_abox(M,Tableau,QueryType,QueryArgs):-
221 retractall(M:final_abox(_)),
222 retractall(v(_,_,_)),
223 retractall(na(_,_)),
224 retractall(rule_n(_)),
225 assert(rule_n(0)),
226 get_bdd_environment(M,Env),
227 collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
228 ( dif(ConnectedInds,[]) ->
229 ( findall((classAssertion(Class,Individual),BDDCA-[]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
230 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),
231 232 findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
233 findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
234 findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),intersect(L,ConnectedInds),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
235 )
236 ; 237 ( findall((classAssertion(Class,Individual),BDDCA-[]),(M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
238 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),
239 240 findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
241 findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
242 findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
243 )
244 ),
245 new_abox(ABox0),
246 new_tabs(Tabs0),
247 init_expansion_queue(LCA,LPA,ExpansionQueue),
248 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
249 append([LCA,LDIA,LPA],CreateTabsList),
250 create_tabs(CreateTabsList,Tableau0,Tableau1),
251 append([LCA,LPA,LNA,LDIA],AddAllList),
252 add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
253 merge_all_individuals(M,LSIA,Tableau2,Tableau3),
254 add_owlThing_list(M,Tableau3,Tableau),
255 !.
256
262
263initial_expl(M,BDD-[]):-
264 get_bdd_environment(M,Env),
265 zero(Env,BDD).
266
267empty_expl(M,BDD-[]):-
268 get_bdd_environment(M,Env),
269 one(Env,BDD).
270
271and_f_ax(M,Axiom,BDD0,BDD):-
272 get_bdd_environment(M,Env),
273 bdd_and(M,Env,[Axiom],BDDAxiom),
274 and_f(M,BDDAxiom-[],BDD0,BDD).
275
277and_f(_,[],BDD,BDD):- !.
278
279and_f(_,BDD,[],BDD):- !.
280
281and_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
282 get_bdd_environment(M,Env),
283 and(Env,BDD0,BDD1,BDD),
284 append(CP0,CP1,CP).
285
286
288or_all_f(M,[],BDD):-
289 initial_expl(M,BDD),!.
290
291or_all_f(M,[H|T],Expl):-
292 or_all_f(M,T,Expl1),
293 or_f(M,H,Expl1,Expl),!.
294
295or_f(_,[],BDD,BDD):- !.
296
297or_f(_,BDD,[],BDD):- !.
298
299or_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
300 get_bdd_environment(M,Env),
301 or(Env,BDD0,BDD1,BDD),
302 append(CP0,CP1,CP).
303
304
310
311test(M,L1,L2-CP2,F-CP):-
312 313 314 or_f(M,L1,L2-CP2,F-CP),
315 dif(L2,F).
316
317
323
324get_choice_point_id(_,0).
325
326create_choice_point(_,_,_,_,_,0).
327
328add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
329 (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
330
331add_choice_point(_,_,Expl,Expl):- !.
332
333
339
340get_bdd_environment(M,Env):-
341 M:tornado_bdd_environment(Env),!.
342
343get_bdd_environment(M,Env):-
344 init(Env),
345 M:assert(tornado_bdd_environment(Env)).
346
347clean_environment(M,Env):-
348 end(Env),
349 retractall(M:tornado_bdd_environment(_)).
350
351build_bdd(_,Env,[],BDD):- !,
352 zero(Env,BDD).
353
354build_bdd(_,_Env,BDD,BDD).
355
356bdd_and(M,Env,[X],BDDX):-
357 get_prob_ax(M,X,AxN,Prob),!,
358 ProbN is 1-Prob,
359 get_var_n(Env,AxN,[],[Prob,ProbN],VX),
360 equality(Env,VX,0,BDDX),!.
361
362bdd_and(_M,Env,[_X],BDDX):- !,
363 one(Env,BDDX)