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, tab_end/1, query_option/2),
   31  retractall(M:setting_trill(_,_)),
   32  retractall(M:query_option(_,_)),
   33  retractall(M:tab_end(_)).
   34  %retractall(M:setting_trill(_,_)),
   35  %prune_tableau_rules(M).
   36  %foreach(setting_trill_default(DefaultSetting,DefaultVal),assert(M:setting_trill(DefaultSetting,DefaultVal))).
   37
   38clean_up(M):-
   39  utility_translation:clean_up(M),
   40  M:(dynamic exp_found/2, inconsistent_theory_flag/0, setting_trill/2, tab_end/1, query_option/2),
   41  retractall(M:exp_found(_,_)),
   42  retractall(M:inconsistent_theory_flag),
   43  retractall(M:setting_trill(_,_)),
   44  retractall(M:query_option(_,_)),
   45  retractall(M:tab_end(_)).
   46
   47/*****************************
   48  MESSAGES
   49******************************/
   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
   58/****************************
   59  QUERY PREDICATES
   60*****************************/
   61
   62/***********
   63  Utilities for queries
   64 ***********/
   65
   66% findall
   67find_n_explanations(M,QueryType,QueryArgs,Expls,_):- % This will not check the arg max_expl as TRILLP returns a pinpointing formula
   68  find_single_explanation(M,QueryType,QueryArgs,Expls),!.
   69
   70find_n_explanations(_,_,_,Expls,_):-
   71  empty_expl(_,Expls-_).
   72
   73
   74compute_prob_and_close(M,Exps-_,QueryOptions):-
   75  M:query_option(compute_prob,CPType),!,
   76  get_from_query_options(QueryOptions,compute_prob,CPType,Prob),
   77  compute_prob(M,Exps,Prob),!.
   78
   79compute_prob_and_close(_M,_,_):-!.
   80
   81% checks the explanation
   82check_and_close(_,Expl,Expl):-
   83  dif(Expl,[]).
   84
   85is_expl(M,Expl-_):-
   86  initial_expl(M,EExpl-_),
   87  dif(Expl,EExpl).
   88
   89
   90find_expls(M,_,_,_):-
   91  (M:inconsistent_theory_flag -> print_message(warning,inconsistent) ; true),!,false.
   92
   93% checks if an explanations was already found
   94find_expls_from_tab_list(_M,[],[]):-!.
   95
   96% checks if an explanations was already found (instance_of version)
   97find_expls_from_tab_list(M,[Tab|T],E):-
   98  get_solved_clashes(Tab,Clashes),
   99  findall(E0,(member(Clash,Clashes),clash(M,Clash,Tab,E0)),Expls0),!,
  100  dif(Expls0,[]),
  101  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  102  % if it is so, it asserts the inconcistency and fails
  103  consistency_check(M,Expls0,Q),
  104  ( dif(Q,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)),
  105  or_all_f(M,Expls0,Expls1),
  106  find_expls_from_tab_list(M,T,E1),
  107  and_f(M,Expls1,E1,E),!.
  108
  109find_expls_from_tab_list(M,[_Tab|T],Expl):-
  110  \+ length(T,0),
  111  find_expls_from_tab_list(M,T,Expl).
  112
  113% this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  114consistency_check(_,[],qp):-!.
  115
  116consistency_check(M,[_-CPs|T],Q):-
  117  dif(CPs,[]),!,
  118  member(qp,CPs),!,
  119  consistency_check(M,T,Q).
  120
  121consistency_check(M,_,['inconsistent','kb']):-!,
  122  assert(M:inconsistent_theory_flag).
  123
  124/****************************/
  125
  126/****************************
  127  TABLEAU ALGORITHM
  128****************************/
  129
  130% --------------
  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
  136/* ************* */
  137
  138/***********
  139  update abox
  140  utility for tableau
  141************/
  142modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
  143  length(LF,1),!.
  144
  145modify_ABox(M,Tab0,sameIndividual(LF),L0-CP0,Tab):-
  146  get_abox(Tab0,ABox0),
  147  find((sameIndividual(L),Expl1-CP1),ABox0),!,
  148  sort(L,LS),
  149  sort(LF,LFS),
  150  LS = LFS,!,
  151  dif(L0-CP0,Expl1-CP1),
  152  ((dif(L0,[]),subset([L0],[Expl1])) -> 
  153     Expl = L0
  154   ;
  155     (subset([Expl1],[L0]) -> fail 
  156      ;
  157        (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
  158     )
  159  ),
  160  remove_from_abox(ABox0,[(sameIndividual(L),Expl1)],ABox),
  161  set_abox(Tab0,[(sameIndividual(L),Expl)|ABox],Tab).
  162
  163modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
  164  add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
  165  get_abox(Tab0,ABox),
  166  set_abox(Tab1,[(sameIndividual(LF),L0)|ABox],Tab).
  167
  168modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
  169  length(LF,1),!.
  170
  171modify_ABox(M,Tab0,differentIndividuals(LF),L0-CP0,Tab):-
  172  get_abox(Tab0,ABox0),
  173  find((sameIndividual(L),Expl1-CP1),ABox0),!,
  174  sort(L,LS),
  175  sort(LF,LFS),
  176  LS = LFS,!,
  177  dif(L0-CP0,Expl1-CP1),
  178  ((dif(L0,[]),subset([L0],[Expl1])) -> 
  179     Expl = L0
  180   ;
  181     (subset([Expl1],[L0]) -> fail 
  182      ;
  183        (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
  184     )
  185  ),
  186  remove_from_abox(ABox0,[(differentIndividuals(L),Expl1)],ABox),
  187  set_abox(Tab0,[(differentIndividuals(L),Expl)|ABox],Tab).
  188
  189modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
  190  add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
  191  get_abox(Tab0,ABox),
  192  set_abox(Tab1,[(differentIndividuals(LF),L0)|ABox],Tab).
  193
  194modify_ABox(M,Tab0,C,Ind,L0-CP0,Tab):-
  195  get_abox(Tab0,ABox0),
  196  findClassAssertion(C,Ind,Expl1-CP1,ABox0),!,
  197  dif(L0-CP0,Expl1-CP1),
  198  ((dif(L0,[]),subset([L0],[Expl1])) -> 
  199     Expl = L0
  200   ;
  201     (subset([Expl1],[L0]) -> fail 
  202      ;
  203        (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
  204     )
  205  ),
  206  remove_from_abox(ABox0,(classAssertion(C,Ind),Expl1),ABox),
  207  set_abox(Tab0,[(classAssertion(C,Ind),Expl)|ABox],Tab1),
  208  update_expansion_queue_in_tableau(M,C,Ind,Tab1,Tab).
  209  
  210  
  211modify_ABox(M,Tab0,C,Ind,L0,Tab):-
  212  add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
  213  get_abox(Tab0,ABox0),
  214  set_abox(Tab1,[(classAssertion(C,Ind),L0)|ABox0],Tab2),
  215  update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
  216
  217modify_ABox(M,Tab0,P,Ind1,Ind2,L0-CP0,Tab):-
  218  get_abox(Tab0,ABox0),
  219  findPropertyAssertion(P,Ind1,Ind2,Expl1-CP1,ABox0),!,
  220  dif(L0-CP0,Expl1-CP1),
  221  ((dif(L0,[]),subset([L0],[Expl1])) -> 
  222     Expl = L0
  223   ;
  224     % L0 is the new explanation, i.e. the \psi and Expl1 is the old label of an essertion
  225     (test(M,L0,Expl1),or_f(M,L0-CP0,Expl1-CP1,Expl))
  226  ),
  227  remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl1),ABox),
  228  set_abox(Tab0,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab1),
  229  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab1,Tab).
  230  
  231  
  232modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
  233  add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
  234  get_abox(Tab0,ABox0),
  235  set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),L0)|ABox0],Tab2),
  236  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
  237
  238/* ************* */
  239
  240/*
  241  build_abox
  242  ===============
  243*/
  244
  245build_abox(M,Tableau,QueryType,QueryArgs):-
  246  retractall(M:final_abox(_)),
  247  collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
  248  ( dif(ConnectedInds,[]) ->
  249    ( findall((classAssertion(Class,Individual),*([classAssertion(Class,Individual)])-[]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual)),LCA),
  250      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),
  251      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  252      findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
  253      findall((differentIndividuals(Ld),*([differentIndividuals(Ld)])-[]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds)),LDIA),
  254      findall((sameIndividual(L),*([sameIndividual(L)])-[]),(M:sameIndividual(L),intersect(L,ConnectedInds)),LSIA)
  255    )
  256    ; % all the individuals
  257    ( findall((classAssertion(Class,Individual),*([classAssertion(Class,Individual)])-[]),M:classAssertion(Class,Individual),LCA),
  258      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),
  259      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  260      findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
  261      findall((differentIndividuals(Ld),*([differentIndividuals(Ld)])-[]),M:differentIndividuals(Ld),LDIA),
  262      findall((sameIndividual(L),*([sameIndividual(L)])-[]),M:sameIndividual(L),LSIA)
  263    )
  264  ),
  265  new_abox(ABox0),
  266  new_tabs(Tabs0),
  267  init_expansion_queue(LCA,LPA,ExpansionQueue),
  268  init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
  269  append([LCA,LDIA,LPA],CreateTabsList),
  270  create_tabs(CreateTabsList,Tableau0,Tableau1),
  271  append([LCA,LPA,LNA,LDIA],AddAllList),
  272  add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
  273  merge_all_individuals(M,LSIA,Tableau2,Tableau3),
  274  add_owlThing_list(M,Tableau3,Tableau),
  275  !.
  276
  277/**********************
  278
  279Explanation Management
  280
  281***********************/
  282
  283initial_expl(_M,[]-[]):-!.
  284
  285empty_expl(_M,[]-[]):-!.
  286
  287and_f_ax(M,Axiom,F0,F):-
  288  and_f(M,*([Axiom])-[],F0,F),!.
  289
  290% and between two formulae
  291and_f(_,[],[],[]):-!.
  292
  293and_f(_,[],F,F):-!.
  294
  295and_f(_,F,[],F):-!.
  296
  297and_f(M,F1-CP1,F2-CP2,F-CP):-
  298  and_f(M,F1,F2,F),
  299  append(CP1,CP2,CP).
  300
  301% absorption for subformula (a * (b + (c * d))) * (c * d * e) = a * c * d * e
  302and_f(M,*(A1),*(A2),*(A)):-
  303  member(+(O1),A1),
  304  member(*(AO1),O1),
  305  subset(AO1,A2),!,
  306  delete(A1,+(O1),A11),
  307  and_f(M,*(A11),*(A2),*(A)).
  308% (a * (b + c + e)) * (c * d) = a * c * d
  309and_f(M,*(A1),*(A2),*(A)):-
  310  member(+(O1),A1),
  311  member(X,O1),
  312  member(X,A2),!,
  313  delete(A1,+(O1),A11),
  314  and_f(M,*(A11),*(A2),*(A)).
  315% absorption for subformula (c * d * e)  (a * (b + (c * d))) = c * d * e * a
  316and_f(M,*(A1),*(A2),*(A)):-
  317  member(+(O2),A2),
  318  member(*(AO2),O2),
  319  subset(AO2,A1),!,
  320  delete(A2,+(O2),A21),
  321  and_f(M,*(A1),*(A21),*(A)).
  322% (c * d) * (a * (b + c + e)) = c * d * a
  323and_f(M,*(A1),*(A2),*(A)):-
  324  member(+(O2),A2),
  325  member(X,O2),
  326  member(X,A1),!,
  327  delete(A2,+(O2),A21),
  328  and_f(M,*(A1),*(A21),*(A)).
  329% (a * b) * (a * c) = a * b * c
  330and_f(_M,*(A1),*(A2),*(A)):-!,
  331  append(A1,A2,A0),
  332  sort(A0,A).
  333
  334% absorption x * (x + y) = x
  335and_f(_M,*(A1),+(O1),*(A1)):-
  336  member(X,A1),
  337  member(X,O1),!.
  338and_f(_M,*(A1),+(O1),*(A)):-!,
  339  append(A1,[+(O1)],A).
  340
  341% absorption x * (x + y) = x
  342and_f(_M,+(O1),*(A1),*(A1)):-
  343  member(X,A1),
  344  member(X,O1),!.
  345and_f(_M,+(O1),*(A1),*(A)):-!,
  346  append([+(O1)],A1,A).
  347
  348and_f(_M,+(O1),+(O2),*([+(O1),+(O2)])).
  349/*
  350and_f(M,[],[],[]):-!.
  351and_f(M,[],F2,F2):-!.
  352and_f(M,F1,[],F1):-!.
  353and_f(M,*(L1),*(L2),*(L)):-!,
  354  flatten([L1,L2],L0),
  355  remove_duplicates(L0,L).
  356and_f(M,+(L1),*(L2),*(L)):-!,
  357  flatten([L2,+(L1)],L0),
  358  remove_duplicates(L0,L).
  359and_f(M,*(L1),+(L2),*(L)):-!,
  360  flatten([L1,+(L2)],L0),
  361  remove_duplicates(L0,L).  
  362and_f(M,+(L1),+(L2),*(L)):-!,
  363  flatten([+(L1),+(L2)],L0),
  364  remove_duplicates(L0,L).
  365and_f(M,[El],[*(L2)],*(L)):-!,gtrace,
  366  flatten([El,L2],L0),
  367  remove_duplicates(L0,L).  
  368and_f(M,[El],[+(L2)],*(L)):-!,gtrace,
  369  flatten([El,+(L2)],L0),
  370  remove_duplicates(L0,L).
  371and_f(M,[*(L1)],[El],*(L)):-!,gtrace,
  372  flatten([El,L1],L0),
  373  remove_duplicates(L0,L).  
  374and_f(M,[+(L1)],[El],*(L)):-!,gtrace,
  375  flatten([El,+(L1)],L0),
  376  remove_duplicates(L0,L).  
  377and_f(M,[El1],[El2],*(L)):-gtrace,
  378  flatten([El1,El2],L0),
  379  remove_duplicates(L0,L).
  380*/
  381
  382/*
  383% or between two formulae
  384or_f(M,[],[],[]):-!.
  385
  386or_f(M,[],F,F):-!.
  387
  388or_f(M,F,[],F):-!.
  389
  390% absorption for subformula (a + (b * (c + d))) + (c + d + e) = a + c + d + e
  391or_f(M,+(A1),+(A2),+(A)):-
  392  member(*(O1),A1),
  393  member(+(AO1),O1),
  394  subset(AO1,A2),!,
  395  delete(A1,*(O1),A11),
  396  or_f(M,+(A11),+(A2),+(A)).
  397% (a + (b * c * e)) + (c + d) = a + c + d
  398or_f(M,+(A1),+(A2),+(A)):-
  399  member(*(O1),A1),
  400  member(X,O1),
  401  member(X,A2),!,
  402  delete(A1,*(O1),A11),
  403  or_f(M,+(A11),+(A2),+(A)).
  404% absorption for subformula (c + d + e)  (a + (b * (c + d))) = c + d + e + a
  405or_f(M,+(A1),+(A2),+(A)):-
  406  member(*(O2),A2),
  407  member(+(AO2),O2),
  408  subset(AO2,A1),!,
  409  delete(A2,*(O2),A21),
  410  or_f(M,+(A1),+(A21),+(A)).
  411% (c + d) + (a + (b * c * e)) = c + d + a
  412or_f(M,+(A1),+(A2),+(A)):-
  413  member(*(O2),A2),
  414  member(X,O2),
  415  member(X,A1),!,
  416  delete(A2,*(O2),A21),
  417  or_f(M,+(A1),+(A21),+(A)).
  418% (a + b) + (a + c) = a + b + c
  419or_f(M,+(A1),+(A2),+(A)):-!,
  420  append(A1,A2,A0),
  421  sort(A0,A).
  422
  423% absorption x + (x * y) = x
  424or_f(M,*(A1),+(O1),*(A1)):-
  425  member(X,A1),
  426  member(X,O1),!.
  427or_f(M,*(A1),+(O1),*(A)):-
  428  append(A1,[+(O1)],A).
  429
  430% absorption x + (x * y) = x
  431or_f(M,+(O1),*(A1),*(A1)):-
  432  member(X,A1),
  433  member(X,O1),!.
  434or_f(M,+(O1),*(A1),*(A)):-
  435  append([+(O1)],A1,A).
  436
  437or_f(M,*(O1),*(O2),+([*(O1),*(O2)])).
  438*/
  439
  440/*
  441* Cleans a complex formula A by removing sub-formulae which are permutation or subset 
  442* of other formulae contained in A
  443*/
  444val_min(F,LO):-
  445  formule_gen(F,LF),
  446  val_min2(LF,LO).
  447  
  448val_min2(L,LO):-
  449  val_min0(L,L,LSov),
  450  val_min1(L,L,LPer),
  451  remove_duplicates(LPer,LPer1),
  452  differenceFML(LSov,LPer1,LD),
  453  differenceFML(L,LD,LO).
  454
  455val_min0([],_,[]):-!.
  456val_min0([X|T],L,[X|L2]):-
  457  member(Y,L),
  458  dif(Y,X),
  459  subset(Y,X),!,
  460  val_min0(T,L,L2).
  461val_min0([_|T],L,L2):-
  462  val_min0(T,L,L2).  
  463  
  464val_min1([],_,[]):-!.
  465val_min1([X|T],L,[Y|L2]):-
  466  member(Y,L),
  467  dif(Y,X),
  468  is_permutation(X,Y),!,
  469  val_min1(T,L,L2).
  470val_min1([_|T],L,L2):-
  471  val_min1(T,L,L2).
  472
  473  
  474% difference between formulae
  475differenceFML([],_,[]).
  476differenceFML([T|Tail],L2,[T|Other]):- \+ member(T,L2),!,differenceFML(Tail,L2,Other).
  477differenceFML([_|C],L2,Diff):- differenceFML(C,L2,Diff).
  478
  479% intersection between formulae
  480intersectionFML([],_,[]).
  481intersectionFML([T|C],L2,[T|Resto]):- member(T,L2),!,intersectionFML(C,L2,Resto).
  482intersectionFML([_|C],L2,LInt):- intersectionFML(C,L2,LInt).
  483
  484%
  485is_or(+(_)).
  486is_and(*(_)).
  487
  488
  489find_and_in_formula(F,And):- findall( X, (member(X,F), \+ is_or(X)), And).
  490find_or_in_formula(F,Or):- member(+(Or),F),!.
  491  
  492
  493
  494% develops a formula
  495formule_gen([],[]):- !.
  496formule_gen(FC,F):-findall(XRD, (formula_gen(FC,X), remove_duplicates(X,XRD)), FCD), remove_duplicates(FCD,F).
  497
  498formula_gen([],[]):-!.
  499formula_gen([X],[X]):- \+ is_and(X), \+ is_or(X),!.
  500formula_gen([*(FC)],F):-
  501  find_or_in_formula(FC,Or),!,
  502  find_and_in_formula(FC,And),
  503  member(X,Or),
  504  formula_gen([X],XF),
  505  append(And,XF,F).
  506formula_gen([*(FC)],And):- 
  507  find_and_in_formula(FC,And),!.
  508formula_gen([+(FC)],F):- 
  509  member(X,FC),
  510  formula_gen([X],XF),
  511  append([],XF,F).
  512
  513% Decomposes a fomula
  514formule_decomp([],[],[],[],[],[],[]):- !.
  515formule_decomp([],[+(_F2)],[],[],[],[],[]):- !.
  516formule_decomp([*(F1)],[],AndF1,[],[],AndF1,[]):-
  517  find_and_in_formula(F1,AndF1),!.
  518formule_decomp([],[*(F2)],[],AndF2,[],[],AndF2):-
  519  find_and_in_formula(F2,AndF2),!.
  520formule_decomp([*(F1)],[*(F1)],AndF1,AndF1,AndF1,[],[]):- 
  521  find_and_in_formula(F1,AndF1),!.   
  522formule_decomp([*(F1)],[+(_F2)],AndF1,[],[],AndF1,[]):-
  523  find_and_in_formula(F1,AndF1),!.  
  524formule_decomp([*(F1)],[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2):-
  525  find_and_in_formula(F1,AndF1),
  526  find_and_in_formula(F2,AndF2),
  527  intersectionFML(AndF1,AndF2,AndUguali),
  528  differenceFML(AndF1,AndUguali,AndDiversiF1),
  529  differenceFML(AndF2,AndUguali,AndDiversiF2),!. 
  530formule_decomp([El1],[+(_F2)],[El1],[],[],[El1],[]):- !.
  531formule_decomp([El1],[*(F2)],[El1],AndF2,AndUguali,AndDiversiF1,AndDiversiF2):-
  532  find_and_in_formula(F2,AndF2),
  533  intersectionFML([El1],AndF2,AndUguali),
  534  differenceFML([El1],AndUguali,AndDiversiF1),
  535  differenceFML(AndF2,AndUguali,AndDiversiF2),!.   
  536formule_decomp([*(F1)],[El2],AndF1,[El2],AndUguali,AndDiversiF1,AndDiversiF2):-
  537  find_and_in_formula(F1,AndF1),
  538  intersectionFML(AndF1,[El2],AndUguali),
  539  differenceFML(AndF1,AndUguali,AndDiversiF1),
  540  differenceFML([El2],AndUguali,AndDiversiF2),!.   
  541formule_decomp([],[El2],[],[El2],[],[],[El2]):- !.
  542formule_decomp([El1],[],[El1],[],[],[El1],[]):- !.
  543formule_decomp([El],[El],[El],[El],[El],[],[]):- !.
  544formule_decomp([El1],[El2],[El1],[El2],[],[El1],[El2]):- !.
  545  
  546 
  547%computes a compact formula strarting from 2 formulae 
  548/*
  549or_f(M,[],[],[]):-!.
  550
  551or_f(M,[],F,F):-!.
  552
  553or_f(M,F,[],F):-!.
  554*/
  555
  556or_all_f(_M,[H],H):-!.
  557
  558or_all_f(M,[H|T],Expl):-
  559  or_all_f(M,T,Expl1),
  560  or_f(M,H,Expl1,Expl),!.
  561
  562or_f(_M,F1-CP1,F2-CP2,F-CP):-
  563  or_f_int([F1],[F2],[F]),
  564  append(CP1,CP2,CP).
  565
  566or_f_int([*(FC1)],[FC2],OrF):- !,
  567  findall( +(X), (member(+(X),FC1)), Or), length(Or,Length), 
  568  ( (Length > 1) ->
  569     (OrF = [+([*(FC1),FC2])])
  570   ;
  571     (formule_gen([*(FC1)],F1), or_scan(F1,[FC2],OrF))
  572  ).
  573
  574or_f_int(FC1,FC2,OrF):- formule_gen(FC1,F1), or_scan(F1,FC2,OrF).
  575
  576or_scan([],F2,F2):-!.
  577or_scan([T|C],F2,OrF):- ( T = [_] -> NT = T ; NT = [*(T)] ), or_between_formule(NT,F2,OrF1),or_scan(C,OrF1,OrF).
  578  
  579%computes a compact formula strarting from 2 formulae
  580or_between_formule(F1,[],F1):- !.
  581or_between_formule([],F2,F2):- !.
  582or_between_formule(F,F,F):- !.
  583/*
  584or_between_formule(F1,F2,F2):-
  585  nl,write('Zeresimo caso'),nl,
  586  formule_gen(F1,F1F),
  587  formule_gen(F2,F2F),
  588  findall(X1, (member(X,F1F),is_permutation(X,X1),member(X1,F2F)), Ris), is_permutation(Ris,F2F),!.
  589*/
  590or_between_formule(F1,[+(F2)],OrF):-
  591  formule_decomp(F1,[+(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
  592  or_between_formule1(F1,[+(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,F2,OrF),!. 
  593or_between_formule(F1,[*(F2)],OrF):-
  594  formule_decomp(F1,[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
  595  ( find_or_in_formula(F2,OrF2) -> true ; OrF2 = [] ),
  596  or_between_formule1(F1,[*(F2)],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,OrF2,OrF),!.
  597or_between_formule(F1,[El2],OrF):-
  598  formule_decomp(F1,[El2],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2),
  599  or_between_formule1(F1,[El2],AndF1,AndF2,AndUguali,AndDiversiF1,AndDiversiF2,[],OrF).  
  600  
  601or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,[],_AndDiversiF2,_OrF2,OrF):-
  602  %nl,write('First case'),nl,
  603  !,
  604  ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)]).
  605or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,_AndDiversiF1,[],[],OrF):-
  606  %nl,write('2nd case'),nl,
  607  !,
  608  ( AndUguali = [_] -> append([],AndUguali,OrF) ; OrF = [*(AndUguali)] ).
  609or_between_formule1(_F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,AndDiversiF2,[],OrF):-
  610  %nl,write('3rd case'),nl,
  611  dif(AndDiversiF1,[]), dif(AndDiversiF2,[]),!,
  612  ( AndDiversiF1 = [_] -> append([],AndDiversiF1,NAndF1) ; NAndF1 = *(AndDiversiF1) ),
  613  ( AndDiversiF2 = [_] -> append([],AndDiversiF2,NAndF2) ; NAndF2 = *(AndDiversiF2) ),
  614  flatten([NAndF1, NAndF2], Or),
  615  OrF = [+(Or)].
  616or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,AndDiversiF2,[],OrF):-
  617  %nl,write('4th case'),nl,
  618  dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(AndUguali,[]),!,
  619  ( AndDiversiF1 = [_] -> append([],AndDiversiF1,NAndF1) ; NAndF1 = *(AndDiversiF1) ),
  620  ( AndDiversiF2 = [_] -> append([],AndDiversiF2,NAndF2) ; NAndF2 = *(AndDiversiF2) ),
  621  flatten([NAndF1, NAndF2], Or),
  622  flatten([AndUguali, +(Or)], And),
  623  OrF = [*(And)].
  624or_between_formule1(F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,[],OrF2,OrF):-
  625  %nl,write('5th case'),nl,
  626  dif(AndDiversiF1,[]), dif(OrF2,[]),!,
  627  find_compatible_or(AndDiversiF1,OrF2,OrF2C,OrF2NC),
  628  ( dif(OrF2C,[]) -> (or_f_int(OrF2C,F1,OrFC), flatten([OrFC, OrF2NC], NOr) ) ; append(F1, OrF2,NOr) ),
  629  OrF = [+(NOr)].  
  630or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,[],OrF2,OrF):-
  631  %nl,write('6th case'),nl,
  632  dif(AndDiversiF1,[]), dif(AndUguali,[]), dif(OrF2,[]),!,
  633  ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = [*(AndDiversiF1)] ),
  634  find_compatible_or(AndDiversiF1,OrF2,OrF2C,OrF2NC),
  635  ( dif(OrF2C,[]) -> (or_f_int(OrF2C,AndDiversiF1N,OrFC),flatten([OrFC, OrF2NC], NOr) ) ; append(AndDiversiF1N, OrF2,NOr) ),
  636  flatten([AndUguali, +(NOr)], And),
  637  OrF = [*(And)].
  638or_between_formule1(_F1,_F2,_AndF1,_AndF2,[],AndDiversiF1,AndDiversiF2,OrF2,OrF):-
  639  %nl,write('7th case'),nl,
  640  dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(OrF2,[]),!,
  641  ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = *(AndDiversiF1) ),
  642  flatten([AndDiversiF2, +(OrF2)], AndF2N),
  643  NOrF2 = *(AndF2N),
  644  flatten([AndDiversiF1N, NOrF2], And),
  645  OrF = [+(And)].
  646or_between_formule1(_F1,_F2,_AndF1,_AndF2,AndUguali,AndDiversiF1,AndDiversiF2,OrF2,OrF):-
  647  %nl,write('8th case'),nl,
  648  dif(AndDiversiF1,[]), dif(AndDiversiF2,[]), dif(AndUguali,[]), dif(OrF2,[]),!,
  649  ( AndDiversiF1 = [_] -> append([],AndDiversiF1,AndDiversiF1N) ; AndDiversiF1N = *(AndDiversiF1) ),
  650  flatten([AndDiversiF2, +(OrF2)], AndF2N),
  651  NOrF2 = *(AndF2N),
  652  flatten([AndDiversiF1N, NOrF2], AndDiversi),
  653  flatten([AndUguali, +(AndDiversi)], And),
  654  OrF = [*(And)].
  655
  656%optimization for 5th and 6th cases
  657find_compatible_or(F1,OrF2,OrF2C,OrF2NC):-  
  658  findall(  Y, ( member(Y,OrF2), ( Y = *(YN) -> find_and_in_formula(YN,AndY) ; AndY = [Y] ), intersectionFML(F1,AndY,I), dif(I,[]),!), OrF2C),
  659  differenceFML(OrF2,OrF2C,OrF2NC).
  660  
  661remove_duplicates(A,C):-sort(A,C).
  662
  663/**********************
  664
  665Hierarchy Explanation Management
  666
  667***********************/
  668
  669hier_initial_expl(_M,[]):-!.
  670
  671hier_empty_expl(_M,[]):-!.
  672
  673hier_and_f(M,A,B,C):- and_f(M,A,B,C).
  674
  675hier_or_f(M,Or1,Or2,Or):- or_f(M,Or1,Or2,Or).
  676
  677hier_or_f_check(M,Or1,Or2,Or):- or_f(M,Or1,Or2,Or).
  678
  679hier_ax2ex(_M,Ax,*([Ax])):- !.
  680  
  681get_subclass_explanation(_M,C,D,Expl,Expls):-
  682  utility_kb:get_subClass_expl(_,Expls,C,D,Expl).
  683
  684/**********************
  685
  686TRILLP SAT TEST
  687
  688***********************/
  689/*
  690L1 is the \psi
  691L2 is the old label of the assertion, e.g. lab(n : D) in the unfold rule
  692I 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
  693
  694*/
  695test(_M,L1,L2):-
  696  %build_f(L1,L2,F),
  697  %sat(F).
  698  create_formula(L1,L2,F),
  699  sat(F).
  700
  701create_formula(L1,L2,(F1*(~(F2)))):-
  702  dif(L1,[]), dif(L2,[]),
  703  variabilize_formula(L1,F1,[],Vars),
  704  variabilize_formula(L2,F2,Vars,_).
  705
  706variabilize_formula([],[],V,V).
  707
  708variabilize_formula(*(L),*(F),V0,V1):-
  709  variabilize_formula(L,F,V0,V1).
  710
  711variabilize_formula(+(L),+(F),V0,V1):-
  712  variabilize_formula(L,F,V0,V1).
  713
  714variabilize_formula(~(L),~(F),V0,V1):-
  715  variabilize_formula(L,F,V0,V1).
  716
  717variabilize_formula([H|T],[HV|TV],V0,V1):-
  718  not_bool_op(H),
  719  member((H-HV),V0),!,
  720  variabilize_formula(T,TV,V0,V1).
  721
  722variabilize_formula([H|T],[HV|TV],V0,V1):-
  723  not_bool_op(H),!,
  724  variabilize_formula(T,TV,[(H-HV)|V0],V1).
  725
  726variabilize_formula([H|T],[HV|TV],V0,V2):-
  727  variabilize_formula(H,HV,V0,VH),
  728  append(VH,V0,V10),
  729  sort(V10,V1),
  730  variabilize_formula(T,TV,V1,V2).
  731
  732not_bool_op(H):-
  733  \+bool_op(H).
  734
  735bool_op(+(_)):-!.
  736bool_op(*(_)):-!.
  737bool_op(~(_)):-!.
  738
  739
  740/**********************
  741
  742Choice Points Management
  743
  744***********************/
  745
  746get_choice_point_id(_,0).
  747
  748create_choice_point(_,_,_,_,_,0).
  749
  750add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
  751  (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
  752
  753add_choice_point(_,_,Expl,Expl):- !.
  754
  755/**********************
  756
  757 TRILLP Probability Computation
  758
  759***********************/
  760
  761get_bdd_environment(_M,Env):-
  762  init(Env).
  763
  764clean_environment(_M,Env):-
  765  end(Env).
  766
  767build_bdd(_M,Env,[],BDD):-
  768  zero(Env,BDD).
  769
  770build_bdd(M,Env,*(F),BDD):-
  771  bdd_and(M,Env,F,BDD).
  772
  773build_bdd(M,Env,+(F),BDD):-
  774  bdd_or(M,Env,F,BDD).
  775
  776
  777bdd_and(M,Env,[+(X)],BDDX):-!,
  778  bdd_or(M,Env,X,BDDX).
  779
  780bdd_and(_,_Env,[*(_X)],_BDDX):-
  781  write('error: *([*(_)])'),
  782  print_message(error,and_in_and),!,false.
  783
  784bdd_and(M,Env,[X],BDDX):-
  785  get_prob_ax(M,X,AxN,Prob),!,
  786  ProbN is 1-Prob,
  787  get_var_n(Env,AxN,[],[Prob,ProbN],VX),
  788  equality(Env,VX,0,BDDX),!.
  789
  790bdd_and(_M,Env,[_X],BDDX):- !,
  791  one(Env,BDDX).
  792
  793bdd_and(M,Env,[+(H)|T],BDDAnd):-!,
  794  bdd_or(M,Env,H,BDDH),
  795  bdd_and(M,Env,T,BDDT),
  796  and(Env,BDDH,BDDT,BDDAnd).
  797
  798bdd_and(_,_Env,[*(_H)|_T],_BDDX):-
  799  write('error: *([*(_)|_])'),
  800  print_message(error,and_in_and),!,false.
  801
  802bdd_and(M,Env,[H|T],BDDAnd):-
  803  get_prob_ax(M,H,AxN,Prob),!,
  804  ProbN is 1-Prob,
  805  get_var_n(Env,AxN,[],[Prob,ProbN],VH),
  806  equality(Env,VH,0,BDDH),
  807  bdd_and(M,Env,T,BDDT),
  808  and(Env,BDDH,BDDT,BDDAnd).
  809  
  810bdd_and(M,Env,[_H|T],BDDAnd):- !,
  811  one(Env,BDDH),
  812  bdd_and(M,Env,T,BDDT),
  813  and(Env,BDDH,BDDT,BDDAnd).
  814
  815
  816bdd_or(M,Env,[*(X)],BDDX):-!,
  817  bdd_and(M,Env,X,BDDX).
  818
  819bdd_or(M,Env,[+(X)],BDDX):-
  820  bdd_or(M,Env,X,BDDX).
  821
  822/*
  823bdd_or(_,_Env,[+(_X)],_BDDX):-
  824  write('error: +([+(_)])'),
  825  print_message(error,or_in_or),!,false.
  826*/
  827
  828bdd_or(M,Env,[X],BDDX):-
  829  get_prob_ax(M,X,AxN,Prob),!,
  830  ProbN is 1-Prob,
  831  get_var_n(Env,AxN,[],[Prob,ProbN],VX),
  832  equality(Env,VX,0,BDDX),!.
  833
  834bdd_or(_M,Env,[_X],BDDX):- !,
  835  one(Env,BDDX).
  836
  837bdd_or(M,Env,[*(H)|T],BDDAnd):-!,
  838  bdd_and(M,Env,H,BDDH),
  839  bdd_or(M,Env,T,BDDT),
  840  or(Env,BDDH,BDDT,BDDAnd).
  841
  842bdd_or(M,Env,[+(H)|T],BDDX):-
  843  bdd_or(M,Env,H,BDDH),
  844  bdd_or(M,Env,T,BDDT),
  845  or(Env,BDDH,BDDT,BDDX).
  846
  847/*
  848bdd_or(_,_Env,[+(_H)|_T],_BDDX):-
  849  write('error: +([+(_)|_])'),
  850  print_message(error,or_in_or),!,false.
  851*/
  852
  853bdd_or(M,Env,[H|T],BDDAnd):-
  854  get_prob_ax(M,H,AxN,Prob),!,
  855  ProbN is 1-Prob,
  856  get_var_n(Env,AxN,[],[Prob,ProbN],VH),
  857  equality(Env,VH,0,BDDH),
  858  bdd_or(M,Env,T,BDDT),
  859  or(Env,BDDH,BDDT,BDDAnd).
  860  
  861bdd_or(M,Env,[_H|T],BDDAnd):- !,
  862  zero(Env,BDDH),
  863  bdd_or(M,Env,T,BDDT),
  864  or(Env,BDDH,BDDT,BDDAnd)