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
   15@license Artistic License 2.0
   16@copyright Riccardo Zese
   17*/
   18
   19:- use_module(library(clpb)).   20
   21/********************************
   22  SETTINGS
   23*********************************/
   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  %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):-
  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     % 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):-
  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
  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),
  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
  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
  745add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
  746  (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
  747
  748add_choice_point(_,_,Expl,Expl):- !.
  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)