1/* trillp predicates
2
3This module performs reasoning over probabilistic description logic knowledge bases.
4It reads probabilistic knowledge bases in RDF format or in Prolog format, a functional-like
5sintax based on definitions of Thea library, and answers queries by finding the set
6of explanations or computing the probability.
7
8[1] http://vangelisv.github.io/thea/
9
10See https://github.com/rzese/trill/blob/master/doc/manual.pdf or
11http://ds.ing.unife.it/~rzese/software/trill/manual.html for
12details.
13
14@author Riccardo Zese
17*/
18
19:- use_module(library(clpb)).   20
21/********************************
22  SETTINGS
23*********************************/
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  %retractall(M:setting_trill(_,_)),
32  %prune_tableau_rules(M).
33  %foreach(setting_trill_default(DefaultSetting,DefaultVal),assert(M:setting_trill(DefaultSetting,DefaultVal))).
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
42/*****************************
43  MESSAGES
44******************************/
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
53/****************************
54  QUERY PREDICATES
55*****************************/
56
57/***********
58  Utilities for queries
59 ***********/
60
61% findall
62find_n_explanations(M,QueryType,QueryArgs,Expls,_,Opt):- % This will not check the arg max_expl as TRILLP returns a pinpointing formula
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
72% checks the explanation
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
88% checks if an explanations was already found
89find_expls_int(_M,[],_,[]):-!.
90
91% checks if an explanations was already found (instance_of version)
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  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
97  % if it is so, it asserts the inconcistency and fails
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
107% this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
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
119/****************************/
120
121/****************************
122  TABLEAU ALGORITHM
123****************************/
124
125% --------------
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
131/* ************* */
132
133/***********
134  update abox
135  utility for tableau
136************/
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):-
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):-
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):-
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     % L0 is the new explanation, i.e. the \psi and Expl1 is the old label of an essertion
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):-
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
233/* ************* */
234
235/*
236  build_abox
237  ===============
238*/
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      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
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    ; % all the individuals
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      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
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),
268  merge_all_individuals(M,LSIA,Tableau2,Tableau3),
270  !.
271
272/**********************
273
274Explanation Management
275
276***********************/
277
278initial_expl(_M,[]-[]):-!.
279
280empty_expl(_M,[]-[]):-!.
281
282and_f_ax(M,Axiom,F0,F):-
283  and_f(M,*([Axiom])-[],F0,F),!.
284
285% and between two formulae
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
296% absorption for subformula (a * (b + (c * d))) * (c * d * e) = a * c * d * e
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)).
303% (a * (b + c + e)) * (c * d) = a * c * d
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)).
310% absorption for subformula (c * d * e)  (a * (b + (c * d))) = c * d * e * 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)).
317% (c * d) * (a * (b + c + e)) = c * d * 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)).
324% (a * b) * (a * c) = a * b * c
325and_f(_M,*(A1),*(A2),*(A)):-!,
326  append(A1,A2,A0),
327  sort(A0,A).
328
329% absorption x * (x + y) = x
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
336% absorption x * (x + y) = x
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)])).
344/*
345and_f(M,[],[],[]):-!.
346and_f(M,[],F2,F2):-!.
347and_f(M,F1,[],F1):-!.
348and_f(M,*(L1),*(L2),*(L)):-!,
349  flatten([L1,L2],L0),
350  remove_duplicates(L0,L).
351and_f(M,+(L1),*(L2),*(L)):-!,
352  flatten([L2,+(L1)],L0),
353  remove_duplicates(L0,L).
354and_f(M,*(L1),+(L2),*(L)):-!,
355  flatten([L1,+(L2)],L0),
356  remove_duplicates(L0,L).
357and_f(M,+(L1),+(L2),*(L)):-!,
358  flatten([+(L1),+(L2)],L0),
359  remove_duplicates(L0,L).
360and_f(M,[El],[*(L2)],*(L)):-!,gtrace,
361  flatten([El,L2],L0),
362  remove_duplicates(L0,L).
363and_f(M,[El],[+(L2)],*(L)):-!,gtrace,
364  flatten([El,+(L2)],L0),
365  remove_duplicates(L0,L).
366and_f(M,[*(L1)],[El],*(L)):-!,gtrace,
367  flatten([El,L1],L0),
368  remove_duplicates(L0,L).
369and_f(M,[+(L1)],[El],*(L)):-!,gtrace,
370  flatten([El,+(L1)],L0),
371  remove_duplicates(L0,L).
372and_f(M,[El1],[El2],*(L)):-gtrace,
373  flatten([El1,El2],L0),
374  remove_duplicates(L0,L).
375*/
376
377/*
378% or between two formulae
379or_f(M,[],[],[]):-!.
380
381or_f(M,[],F,F):-!.
382
383or_f(M,F,[],F):-!.
384
385% absorption for subformula (a + (b * (c + d))) + (c + d + e) = a + c + d + e
386or_f(M,+(A1),+(A2),+(A)):-
387  member(*(O1),A1),
388  member(+(AO1),O1),
389  subset(AO1,A2),!,
390  delete(A1,*(O1),A11),
391  or_f(M,+(A11),+(A2),+(A)).
392% (a + (b * c * e)) + (c + d) = a + c + d
393or_f(M,+(A1),+(A2),+(A)):-
394  member(*(O1),A1),
395  member(X,O1),
396  member(X,A2),!,
397  delete(A1,*(O1),A11),
398  or_f(M,+(A11),+(A2),+(A)).
399% absorption for subformula (c + d + e)  (a + (b * (c + d))) = c + d + e + a
400or_f(M,+(A1),+(A2),+(A)):-
401  member(*(O2),A2),
402  member(+(AO2),O2),
403  subset(AO2,A1),!,
404  delete(A2,*(O2),A21),
405  or_f(M,+(A1),+(A21),+(A)).
406% (c + d) + (a + (b * c * e)) = c + d + a
407or_f(M,+(A1),+(A2),+(A)):-
408  member(*(O2),A2),
409  member(X,O2),
410  member(X,A1),!,
411  delete(A2,*(O2),A21),
412  or_f(M,+(A1),+(A21),+(A)).
413% (a + b) + (a + c) = a + b + c
414or_f(M,+(A1),+(A2),+(A)):-!,
415  append(A1,A2,A0),
416  sort(A0,A).
417
418% absorption x + (x * y) = x
419or_f(M,*(A1),+(O1),*(A1)):-
420  member(X,A1),
421  member(X,O1),!.
422or_f(M,*(A1),+(O1),*(A)):-
423  append(A1,[+(O1)],A).
424
425% absorption x + (x * y) = x
426or_f(M,+(O1),*(A1),*(A1)):-
427  member(X,A1),
428  member(X,O1),!.
429or_f(M,+(O1),*(A1),*(A)):-
430  append([+(O1)],A1,A).
431
432or_f(M,*(O1),*(O2),+([*(O1),*(O2)])).
433*/
434
435/*
436* Cleans a complex formula A by removing sub-formulae which are permutation or subset
437* of other formulae contained in A
438*/
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
469% difference between formulae
470differenceFML([],_,[]).
471differenceFML([T|Tail],L2,[T|Other]):- \+ member(T,L2),!,differenceFML(Tail,L2,Other).
472differenceFML([_|C],L2,Diff):- differenceFML(C,L2,Diff).
473
474% intersection between formulae
475intersectionFML([],_,[]).
476intersectionFML([T|C],L2,[T|Resto]):- member(T,L2),!,intersectionFML(C,L2,Resto).
477intersectionFML([_|C],L2,LInt):- intersectionFML(C,L2,LInt).
478
479%
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
489% develops a formula
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
508% Decomposes a fomula
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
542%computes a compact formula strarting from 2 formulae
543/*
544or_f(M,[],[],[]):-!.
545
546or_f(M,[],F,F):-!.
547
548or_f(M,F,[],F):-!.
549*/
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
574%computes a compact formula strarting from 2 formulae
575or_between_formule(F1,[],F1):- !.
576or_between_formule([],F2,F2):- !.
577or_between_formule(F,F,F):- !.
578/*
579or_between_formule(F1,F2,F2):-
580  nl,write('Zeresimo caso'),nl,
581  formule_gen(F1,F1F),
582  formule_gen(F2,F2F),
583  findall(X1, (member(X,F1F),is_permutation(X,X1),member(X1,F2F)), Ris), is_permutation(Ris,F2F),!.
584*/
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  %nl,write('First case'),nl,
598  !,
599  ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)]).
600or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,_AndDiversiF1,[],[],OrF):-
601  %nl,write('2nd case'),nl,
602  !,
603  ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)] ).
604or_between_formule1(_F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,AndDiversiF2,[],OrF):-
605  %nl,write('3rd case'),nl,
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  %nl,write('4th case'),nl,
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  %nl,write('5th case'),nl,
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  %nl,write('6th case'),nl,
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  %nl,write('7th case'),nl,
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  %nl,write('8th case'),nl,
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
651%optimization for 5th and 6th cases
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
658/**********************
659
660Hierarchy Explanation Management
661
662***********************/
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
679/**********************
680
681TRILLP SAT TEST
682
683***********************/
684/*
685L1 is the \psi
686L2 is the old label of the assertion, e.g. lab(n : D) in the unfold rule
687I check if L1*(~L2) is satisfiable with sat/2. If it is satifiable it means that L1 does not model L2, i.e. \psi \not\models L2
688
689*/
690test(_M,L1,L2):-
691  %build_f(L1,L2,F),
692  %sat(F).
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
735/**********************
736
737Choice Points Management
738
739***********************/
740
741get_choice_point_id(_,0).
742
743create_choice_point(_,_,_,_,_,0).
744
746  (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
747
749
750/**********************
751
752 TRILLP Probability Computation
753
754***********************/
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
817/*
818bdd_or(_,_Env,[+(_X)],_BDDX):-
819  write('error: +([+(_)])'),
820  print_message(error,or_in_or),!,false.
821*/
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
842/*
843bdd_or(_,_Env,[+(_H)|_T],_BDDX):-
844  write('error: +([+(_)|_])'),
845  print_message(error,or_in_or),!,false.
846*/
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)