18
19:- use_module(library(clpb)). 20
24:- multifile setting_trill_default/2. 25setting_trill_default(det_rules,[and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule]).
26setting_trill_default(nondet_rules,[or_rule]).
27
28set_up(M):-
29 utility_translation:set_up(M),
30 M:(dynamic exp_found/2, inconsistent_theory_flag/0, setting_trill/2).
31 32 33 34
35clean_up(M):-
36 utility_translation:clean_up(M),
37 M:(dynamic exp_found/2, inconsistent_theory_flag/0, setting_trill/2),
38 retractall(M:exp_found(_,_)),
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 find_single_explanation(M,QueryType,QueryArgs,Expls,Opt),!.
64
65find_n_explanations(_,_,_,Expls,_,_):-
66 empty_expl(_,Expls-_).
67
68
69compute_prob_and_close(M,Exps,Prob):-
70 compute_prob(M,Exps,Prob).
71
73check_and_close(_,Expl,Expl):-
74 dif(Expl,[]).
75
76is_expl(M,Expl):-
77 initial_expl(M,EExpl-_),
78 dif(Expl,EExpl).
79
80
81find_expls(M,Tabs,Q,E):-
82 find_expls_int(M,Tabs,Q,E-_),!.
83
84find_expls(M,_,_,_):-
85 M:inconsistent_theory_flag,!,
86 print_message(warning,inconsistent),!,false.
87
89find_expls_int(_M,[],_,[]):-!.
90
92find_expls_int(M,[Tab|T],Q,E):-
93 get_clashes(Tab,Clashes),
94 findall(E0,(member(Clash,Clashes),clash(M,Clash,Tab,E0)),Expls0),!,
95 dif(Expls0,[]),
96 97 98 consistency_check(M,Expls0,Q),
99 or_all_f(M,Expls0,Expls1),
100 find_expls_int(M,T,Q,E1),
101 and_f(M,Expls1,E1,E),!.
102
103find_expls_int(M,[_Tab|T],Query0,Expl):-
104 \+ length(T,0),
105 find_expls_int(M,T,Query0,Expl).
106
108consistency_check(_,_,['inconsistent','kb']):-!.
109
110consistency_check(_,[],_):-!.
111
112consistency_check(M,[_-CPs|T],Q):-
113 dif(CPs,[]),!,
114 consistency_check(M,T,Q).
115
116consistency_check(M,_,_):-
117 assert(M:inconsistent_theory_flag).
118
120
124
126findClassAssertion4OWLNothing(M,ABox,Expl):-
127 findall(Expl1,findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl1,ABox),Expls),
128 dif(Expls,[]),
129 or_all_f(M,Expls,Expl).
130
132
137modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
138 length(LF,1),!.
139
140modify_ABox(M,Tab0,sameIndividual(LF),L0-CP0,Tab):-
141 get_abox(Tab0,ABox0),
142 find((sameIndividual(L),Expl1-CP1),ABox0),!,
143 sort(L,LS),
144 sort(LF,LFS),
145 LS = LFS,!,
146 dif(L0-CP0,Expl1-CP1),
147 ((dif(L0,[]),subset([L0],[Expl1])) ->
148 Expl = L0
149 ;
150 (subset([Expl1],[L0]) -> fail
151 ;
152 (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
153 )
154 ),
155 remove_from_abox(ABox0,[(sameIndividual(L),Expl1)],ABox),
156 set_abox(Tab0,[(sameIndividual(L),Expl)|ABox],Tab).
157
158modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
159 add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
160 get_abox(Tab0,ABox),
161 set_abox(Tab1,[(sameIndividual(LF),L0)|ABox],Tab).
162
163modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
164 length(LF,1),!.
165
166modify_ABox(M,Tab0,differentIndividuals(LF),L0-CP0,Tab):-
167 get_abox(Tab0,ABox0),
168 find((sameIndividual(L),Expl1-CP1),ABox0),!,
169 sort(L,LS),
170 sort(LF,LFS),
171 LS = LFS,!,
172 dif(L0-CP0,Expl1-CP1),
173 ((dif(L0,[]),subset([L0],[Expl1])) ->
174 Expl = L0
175 ;
176 (subset([Expl1],[L0]) -> fail
177 ;
178 (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
179 )
180 ),
181 remove_from_abox(ABox0,[(differentIndividuals(L),Expl1)],ABox),
182 set_abox(Tab0,[(differentIndividuals(L),Expl)|ABox],Tab).
183
184modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
185 add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
186 get_abox(Tab0,ABox),
187 set_abox(Tab1,[(differentIndividuals(LF),L0)|ABox],Tab).
188
189modify_ABox(M,Tab0,C,Ind,L0-CP0,Tab):-
190 get_abox(Tab0,ABox0),
191 findClassAssertion(C,Ind,Expl1-CP1,ABox0),!,
192 dif(L0-CP0,Expl1-CP1),
193 ((dif(L0,[]),subset([L0],[Expl1])) ->
194 Expl = L0
195 ;
196 (subset([Expl1],[L0]) -> fail
197 ;
198 (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
199 )
200 ),
201 remove_from_abox(ABox0,(classAssertion(C,Ind),Expl1),ABox),
202 set_abox(Tab0,[(classAssertion(C,Ind),Expl)|ABox],Tab1),
203 update_expansion_queue_in_tableau(M,C,Ind,Tab1,Tab).
204
205
206modify_ABox(M,Tab0,C,Ind,L0,Tab):-
207 add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
208 get_abox(Tab0,ABox0),
209 set_abox(Tab1,[(classAssertion(C,Ind),L0)|ABox0],Tab2),
210 update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
211
212modify_ABox(M,Tab0,P,Ind1,Ind2,L0-CP0,Tab):-
213 get_abox(Tab0,ABox0),
214 findPropertyAssertion(P,Ind1,Ind2,Expl1-CP1,ABox0),!,
215 dif(L0-CP0,Expl1-CP1),
216 ((dif(L0,[]),subset([L0],[Expl1])) ->
217 Expl = L0
218 ;
219 220 (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
221 ),
222 remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl1),ABox),
223 set_abox(Tab0,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab1),
224 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab1,Tab).
225
226
227modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
228 add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
229 get_abox(Tab0,ABox0),
230 set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),L0)|ABox0],Tab2),
231 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
232
234
239
240build_abox(M,Tableau,QueryType,QueryArgs):-
241 retractall(M:final_abox(_)),
242 collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
243 ( dif(ConnectedInds,[]) ->
244 ( findall((classAssertion(Class,Individual),*([classAssertion(Class,Individual)])-[]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual)),LCA),
245 findall((propertyAssertion(Property,Subject, Object),*([propertyAssertion(Property,Subject, Object)])-[]),(member(Subject,ConnectedInds),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA),
246 247 findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
248 findall((differentIndividuals(Ld),*([differentIndividuals(Ld)])-[]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds)),LDIA),
249 findall((sameIndividual(L),*([sameIndividual(L)])-[]),(M:sameIndividual(L),intersect(L,ConnectedInds)),LSIA)
250 )
251 ; 252 ( findall((classAssertion(Class,Individual),*([classAssertion(Class,Individual)])-[]),M:classAssertion(Class,Individual),LCA),
253 findall((propertyAssertion(Property,Subject, Object),*([propertyAssertion(Property,Subject, Object)])-[]),(M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA),
254 255 findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
256 findall((differentIndividuals(Ld),*([differentIndividuals(Ld)])-[]),M:differentIndividuals(Ld),LDIA),
257 findall((sameIndividual(L),*([sameIndividual(L)])-[]),M:sameIndividual(L),LSIA)
258 )
259 ),
260 new_abox(ABox0),
261 new_tabs(Tabs0),
262 init_expansion_queue(LCA,LPA,ExpansionQueue),
263 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
264 append([LCA,LDIA,LPA],CreateTabsList),
265 create_tabs(CreateTabsList,Tableau0,Tableau1),
266 append([LCA,LPA,LNA,LDIA],AddAllList),
267 add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
268 merge_all_individuals(M,LSIA,Tableau2,Tableau3),
269 add_owlThing_list(M,Tableau3,Tableau),
270 !.
271
277
278initial_expl(_M,[]-[]):-!.
279
280empty_expl(_M,[]-[]):-!.
281
282and_f_ax(M,Axiom,F0,F):-
283 and_f(M,*([Axiom])-[],F0,F),!.
284
286and_f(_,[],[],[]):-!.
287
288and_f(_,[],F,F):-!.
289
290and_f(_,F,[],F):-!.
291
292and_f(M,F1-CP1,F2-CP2,F-CP):-
293 and_f(M,F1,F2,F),
294 append(CP1,CP2,CP).
295
297and_f(M,*(A1),*(A2),*(A)):-
298 member(+(O1),A1),
299 member(*(AO1),O1),
300 subset(AO1,A2),!,
301 delete(A1,+(O1),A11),
302 and_f(M,*(A11),*(A2),*(A)).
304and_f(M,*(A1),*(A2),*(A)):-
305 member(+(O1),A1),
306 member(X,O1),
307 member(X,A2),!,
308 delete(A1,+(O1),A11),
309 and_f(M,*(A11),*(A2),*(A)).
311and_f(M,*(A1),*(A2),*(A)):-
312 member(+(O2),A2),
313 member(*(AO2),O2),
314 subset(AO2,A1),!,
315 delete(A2,+(O2),A21),
316 and_f(M,*(A1),*(A21),*(A)).
318and_f(M,*(A1),*(A2),*(A)):-
319 member(+(O2),A2),
320 member(X,O2),
321 member(X,A1),!,
322 delete(A2,+(O2),A21),
323 and_f(M,*(A1),*(A21),*(A)).
325and_f(_M,*(A1),*(A2),*(A)):-!,
326 append(A1,A2,A0),
327 sort(A0,A).
328
330and_f(_M,*(A1),+(O1),*(A1)):-
331 member(X,A1),
332 member(X,O1),!.
333and_f(_M,*(A1),+(O1),*(A)):-!,
334 append(A1,[+(O1)],A).
335
337and_f(_M,+(O1),*(A1),*(A1)):-
338 member(X,A1),
339 member(X,O1),!.
340and_f(_M,+(O1),*(A1),*(A)):-!,
341 append([+(O1)],A1,A).
342
343and_f(_M,+(O1),+(O2),*([+(O1),+(O2)])).
376
434
439val_min(F,LO):-
440 formule_gen(F,LF),
441 val_min2(LF,LO).
442
443val_min2(L,LO):-
444 val_min0(L,L,LSov),
445 val_min1(L,L,LPer),
446 remove_duplicates(LPer,LPer1),
447 differenceFML(LSov,LPer1,LD),
448 differenceFML(L,LD,LO).
449
450val_min0([],_,[]):-!.
451val_min0([X|T],L,[X|L2]):-
452 member(Y,L),
453 dif(Y,X),
454 subset(Y,X),!,
455 val_min0(T,L,L2).
456val_min0([_|T],L,L2):-
457 val_min0(T,L,L2).
458
459val_min1([],_,[]):-!.
460val_min1([X|T],L,[Y|L2]):-
461 member(Y,L),
462 dif(Y,X),
463 is_permutation(X,Y),!,
464 val_min1(T,L,L2).
465val_min1([_|T],L,L2):-
466 val_min1(T,L,L2).
467
468
470differenceFML([],_,[]).
471differenceFML([T|Tail],L2,[T|Other]):- \+ member(T,L2),!,differenceFML(Tail,L2,Other).
472differenceFML([_|C],L2,Diff):- differenceFML(C,L2,Diff).
473
475intersectionFML([],_,[]).
476intersectionFML([T|C],L2,[T|Resto]):- member(T,L2),!,intersectionFML(C,L2,Resto).
477intersectionFML([_|C],L2,LInt):- intersectionFML(C,L2,LInt).
478
480is_or(+(_)).
481is_and(*(_)).
482
483
484find_and_in_formula(F,And):- findall( X, (member(X,F), \+ is_or(X)), And).
485find_or_in_formula(F,Or):- member(+(Or),F),!.
486
487
488
490formule_gen([],[]):- !.
491formule_gen(FC,F):-findall(XRD, (formula_gen(FC,X), remove_duplicates(X,XRD)), FCD), remove_duplicates(FCD,F).
492
493formula_gen([],[]):-!.
494formula_gen([X],[X]):- \+ is_and(X), \+ is_or(X),!.
495formula_gen([*(FC)],F):-
496 find_or_in_formula(FC,Or),!,
497 find_and_in_formula(FC,And),
498 member(X,Or),
499 formula_gen([X],XF),
500 append(And,XF,F).
501formula_gen([*(FC)],And):-
502 find_and_in_formula(FC,And),!.
503formula_gen([+(FC)],F):-
504 member(X,FC),
505 formula_gen([X],XF),
506 append([],XF,F).
507
509formule_decomp([],[],[],[],[],[],[]):- !.
510formule_decomp([],[+(_F2)],[],[],[],[],[]):- !.
511formule_decomp([*(F1)],[],AndF1,[],[],AndF1,[]):-
512 find_and_in_formula(F1,AndF1),!.
513formule_decomp([],[*(F2)],[],AndF2,[],[],AndF2):-
514 find_and_in_formula(F2,AndF2),!.
515formule_decomp([*(F1)],[*(F1)],AndF1,AndF1,AndF1,[],[]):-
516 find_and_in_formula(F1,AndF1),!.
517formule_decomp([*(F1)],[+(_F2)],AndF1,[],[],AndF1,[]):-
518 find_and_in_formula(F1,AndF1),!.
519formule_decomp([*(F1)],[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2):-
520 find_and_in_formula(F1,AndF1),
521 find_and_in_formula(F2,AndF2),
522 intersectionFML(AndF1,AndF2,AndUguali),
523 differenceFML(AndF1,AndUguali,AndDiversiF1),
524 differenceFML(AndF2,AndUguali,AndDiversiF2),!.
525formule_decomp([El1],[+(_F2)],[El1],[],[],[El1],[]):- !.
526formule_decomp([El1],[*(F2)],[El1],AndF2,AndUguali,AndDiversiF1,AndDiversiF2):-
527 find_and_in_formula(F2,AndF2),
528 intersectionFML([El1],AndF2,AndUguali),
529 differenceFML([El1],AndUguali,AndDiversiF1),
530 differenceFML(AndF2,AndUguali,AndDiversiF2),!.
531formule_decomp([*(F1)],[El2],AndF1,[El2],AndUguali,AndDiversiF1,AndDiversiF2):-
532 find_and_in_formula(F1,AndF1),
533 intersectionFML(AndF1,[El2],AndUguali),
534 differenceFML(AndF1,AndUguali,AndDiversiF1),
535 differenceFML([El2],AndUguali,AndDiversiF2),!.
536formule_decomp([],[El2],[],[El2],[],[],[El2]):- !.
537formule_decomp([El1],[],[El1],[],[],[El1],[]):- !.
538formule_decomp([El],[El],[El],[El],[El],[],[]):- !.
539formule_decomp([El1],[El2],[El1],[El2],[],[El1],[El2]):- !.
540
541
550
551or_all_f(_M,[H],H):-!.
552
553or_all_f(M,[H|T],Expl):-
554 or_all_f(M,T,Expl1),
555 or_f(M,H,Expl1,Expl),!.
556
557or_f(_M,F1-CP1,F2-CP2,F-CP):-
558 or_f_int([F1],[F2],[F]),
559 append(CP1,CP2,CP).
560
561or_f_int([*(FC1)],[FC2],OrF):- !,
562 findall( +(X), (member(+(X),FC1)), Or), length(Or,Length),
563 ( (Length > 1) ->
564 (OrF = [+([*(FC1),FC2])])
565 ;
566 (formule_gen([*(FC1)],F1), or_scan(F1,[FC2],OrF))
567 ).
568
569or_f_int(FC1,FC2,OrF):- formule_gen(FC1,F1), or_scan(F1,FC2,OrF).
570
571or_scan([],F2,F2):-!.
572or_scan([T|C],F2,OrF):- ( T = [_] -> NT = T ; NT = [*(T)] ), or_between_formule(NT,F2,OrF1),or_scan(C,OrF1,OrF).
573
575or_between_formule(F1,[],F1):- !.
576or_between_formule([],F2,F2):- !.
577or_between_formule(F,F,F):- !.
585or_between_formule(F1,[+(F2)],OrF):-
586 formule_decomp(F1,[+(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
587 or_between_formule1(F1,[+(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,F2,OrF),!.
588or_between_formule(F1,[*(F2)],OrF):-
589 formule_decomp(F1,[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
590 ( find_or_in_formula(F2,OrF2) -> true ; OrF2 = [] ),
591 or_between_formule1(F1,[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,OrF2,OrF),!.
592or_between_formule(F1,[El2],OrF):-
593 formule_decomp(F1,[El2],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
594 or_between_formule1(F1,[El2],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,[],OrF).
595
596or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,[],_AndDiversiF2,_OrF2,OrF):-
597 598 !,
599 ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)]).
600or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,_AndDiversiF1,[],[],OrF):-
601 602 !,
603 ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)] ).
604or_between_formule1(_F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,AndDiversiF2,[],OrF):-
605 606 dif(AndDiversiF1,[]), dif(AndDiversiF2,[]),!,
607 ( AndDiversiF1 = [_] -> append([],AndDiversiF1,NAndF1) ; NAndF1 = *(AndDiversiF1) ),
608 ( AndDiversiF2 = [_] -> append([],AndDiversiF2,NAndF2) ; NAndF2 = *(AndDiversiF2) ),
609 flatten([NAndF1, NAndF2], Or),
610 OrF = [+(Or)].
611or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,AndDiversiF2,[],OrF):-
612 613 dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(AndUguali,[]),!,
614 ( AndDiversiF1 = [_] -> append([],AndDiversiF1,NAndF1) ; NAndF1 = *(AndDiversiF1) ),
615 ( AndDiversiF2 = [_] -> append([],AndDiversiF2,NAndF2) ; NAndF2 = *(AndDiversiF2) ),
616 flatten([NAndF1, NAndF2], Or),
617 flatten([AndUguali, +(Or)], And),
618 OrF = [*(And)].
619or_between_formule1(F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,[],OrF2,OrF):-
620 621 dif(AndDiversiF1,[]), dif(OrF2,[]),!,
622 find_compatible_or(AndDiversiF1,OrF2,OrF2C,OrF2NC),
623 ( dif(OrF2C,[]) -> (or_f_int(OrF2C,F1,OrFC), flatten([OrFC, OrF2NC], NOr) ) ; append(F1, OrF2,NOr) ),
624 OrF = [+(NOr)].
625or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,[],OrF2,OrF):-
626 627 dif(AndDiversiF1,[]), dif(AndUguali,[]), dif(OrF2,[]),!,
628 ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = [*(AndDiversiF1)] ),
629 find_compatible_or(AndDiversiF1,OrF2,OrF2C,OrF2NC),
630 ( dif(OrF2C,[]) -> (or_f_int(OrF2C,AndDiversiF1N,OrFC),flatten([OrFC, OrF2NC], NOr) ) ; append(AndDiversiF1N, OrF2,NOr) ),
631 flatten([AndUguali, +(NOr)], And),
632 OrF = [*(And)].
633or_between_formule1(_F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,AndDiversiF2,OrF2,OrF):-
634 635 dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(OrF2,[]),!,
636 ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = *(AndDiversiF1) ),
637 flatten([AndDiversiF2, +(OrF2)], AndF2N),
638 NOrF2 = *(AndF2N),
639 flatten([AndDiversiF1N, NOrF2], And),
640 OrF = [+(And)].
641or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,AndDiversiF2,OrF2,OrF):-
642 643 dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(AndUguali,[]), dif(OrF2,[]),!,
644 ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = *(AndDiversiF1) ),
645 flatten([AndDiversiF2, +(OrF2)], AndF2N),
646 NOrF2 = *(AndF2N),
647 flatten([AndDiversiF1N, NOrF2], AndDiversi),
648 flatten([AndUguali, +(AndDiversi)], And),
649 OrF = [*(And)].
650
652find_compatible_or(F1,OrF2,OrF2C,OrF2NC):-
653 findall( Y, ( member(Y,OrF2), ( Y = *(YN) -> find_and_in_formula(YN,AndY) ; AndY = [Y] ), intersectionFML(F1,AndY,I), dif(I,[]),!), OrF2C),
654 differenceFML(OrF2,OrF2C,OrF2NC).
655
656remove_duplicates(A,C):-sort(A,C).
657
663
664hier_initial_expl(_M,[]):-!.
665
666hier_empty_expl(_M,[]):-!.
667
668hier_and_f(M,A,B,C):- and_f(M,A,B,C).
669
670hier_or_f(M,Or1,Or2,Or):- or_f(M,Or1,Or2,Or).
671
672hier_or_f_check(M,Or1,Or2,Or):- or_f(M,Or1,Or2,Or).
673
674hier_ax2ex(_M,Ax,*([Ax])):- !.
675
676get_subclass_explanation(_M,C,D,Expl,Expls):-
677 utility_kb:get_subClass_expl(_,Expls,C,D,Expl).
678
690test(_M,L1,L2):-
691 692 693 create_formula(L1,L2,F),
694 sat(F).
695
696create_formula(L1,L2,(F1*(~(F2)))):-
697 dif(L1,[]), dif(L2,[]),
698 variabilize_formula(L1,F1,[],Vars),
699 variabilize_formula(L2,F2,Vars,_).
700
701variabilize_formula([],[],V,V).
702
703variabilize_formula(*(L),*(F),V0,V1):-
704 variabilize_formula(L,F,V0,V1).
705
706variabilize_formula(+(L),+(F),V0,V1):-
707 variabilize_formula(L,F,V0,V1).
708
709variabilize_formula(~(L),~(F),V0,V1):-
710 variabilize_formula(L,F,V0,V1).
711
712variabilize_formula([H|T],[HV|TV],V0,V1):-
713 not_bool_op(H),
714 member((H-HV),V0),!,
715 variabilize_formula(T,TV,V0,V1).
716
717variabilize_formula([H|T],[HV|TV],V0,V1):-
718 not_bool_op(H),!,
719 variabilize_formula(T,TV,[(H-HV)|V0],V1).
720
721variabilize_formula([H|T],[HV|TV],V0,V2):-
722 variabilize_formula(H,HV,V0,VH),
723 append(VH,V0,V10),
724 sort(V10,V1),
725 variabilize_formula(T,TV,V1,V2).
726
727not_bool_op(H):-
728 \+bool_op(H).
729
730bool_op(+(_)):-!.
731bool_op(*(_)):-!.
732bool_op(~(_)):-!.
733
734
740
741get_choice_point_id(_,0).
742
743create_choice_point(_,_,_,_,_,0).
744
745add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
746 (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
747
748add_choice_point(_,_,Expl,Expl):- !.
749
755
756get_bdd_environment(_M,Env):-
757 init(Env).
758
759clean_environment(_M,Env):-
760 end(Env).
761
762build_bdd(_M,Env,[],BDD):-
763 zero(Env,BDD).
764
765build_bdd(M,Env,*(F),BDD):-
766 bdd_and(M,Env,F,BDD).
767
768build_bdd(M,Env,+(F),BDD):-
769 bdd_or(M,Env,F,BDD).
770
771
772bdd_and(M,Env,[+(X)],BDDX):-!,
773 bdd_or(M,Env,X,BDDX).
774
775bdd_and(_,_Env,[*(_X)],_BDDX):-
776 write('error: *([*(_)])'),
777 print_message(error,and_in_and),!,false.
778
779bdd_and(M,Env,[X],BDDX):-
780 get_prob_ax(M,X,AxN,Prob),!,
781 ProbN is 1-Prob,
782 get_var_n(Env,AxN,[],[Prob,ProbN],VX),
783 equality(Env,VX,0,BDDX),!.
784
785bdd_and(_M,Env,[_X],BDDX):- !,
786 one(Env,BDDX).
787
788bdd_and(M,Env,[+(H)|T],BDDAnd):-!,
789 bdd_or(M,Env,H,BDDH),
790 bdd_and(M,Env,T,BDDT),
791 and(Env,BDDH,BDDT,BDDAnd).
792
793bdd_and(_,_Env,[*(_H)|_T],_BDDX):-
794 write('error: *([*(_)|_])'),
795 print_message(error,and_in_and),!,false.
796
797bdd_and(M,Env,[H|T],BDDAnd):-
798 get_prob_ax(M,H,AxN,Prob),!,
799 ProbN is 1-Prob,
800 get_var_n(Env,AxN,[],[Prob,ProbN],VH),
801 equality(Env,VH,0,BDDH),
802 bdd_and(M,Env,T,BDDT),
803 and(Env,BDDH,BDDT,BDDAnd).
804
805bdd_and(M,Env,[_H|T],BDDAnd):- !,
806 one(Env,BDDH),
807 bdd_and(M,Env,T,BDDT),
808 and(Env,BDDH,BDDT,BDDAnd).
809
810
811bdd_or(M,Env,[*(X)],BDDX):-!,
812 bdd_and(M,Env,X,BDDX).
813
814bdd_or(M,Env,[+(X)],BDDX):-
815 bdd_or(M,Env,X,BDDX).
816
822
823bdd_or(M,Env,[X],BDDX):-
824 get_prob_ax(M,X,AxN,Prob),!,
825 ProbN is 1-Prob,
826 get_var_n(Env,AxN,[],[Prob,ProbN],VX),
827 equality(Env,VX,0,BDDX),!.
828
829bdd_or(_M,Env,[_X],BDDX):- !,
830 one(Env,BDDX).
831
832bdd_or(M,Env,[*(H)|T],BDDAnd):-!,
833 bdd_and(M,Env,H,BDDH),
834 bdd_or(M,Env,T,BDDT),
835 or(Env,BDDH,BDDT,BDDAnd).
836
837bdd_or(M,Env,[+(H)|T],BDDX):-
838 bdd_or(M,Env,H,BDDH),
839 bdd_or(M,Env,T,BDDT),
840 or(Env,BDDH,BDDT,BDDX).
841
847
848bdd_or(M,Env,[H|T],BDDAnd):-
849 get_prob_ax(M,H,AxN,Prob),!,
850 ProbN is 1-Prob,
851 get_var_n(Env,AxN,[],[Prob,ProbN],VH),
852 equality(Env,VH,0,BDDH),
853 bdd_or(M,Env,T,BDDT),
854 or(Env,BDDH,BDDT,BDDAnd).
855
856bdd_or(M,Env,[_H|T],BDDAnd):- !,
857 zero(Env,BDDH),
858 bdd_or(M,Env,T,BDDT),
859 or(Env,BDDH,BDDT,BDDAnd)