1/* trill 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/********************************
   20  SETTINGS
   21*********************************/
   22:- multifile setting_trill_default/2.   23setting_trill_default(det_rules,[o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule]).
   24setting_trill_default(nondet_rules,[or_rule,max_rule,ch_rule]).
   25
   26set_up(M):-
   27  utility_translation:set_up(M),
   28  init_delta(M),
   29  M:(dynamic exp_found/2, setting_trill/2, tab_end/1, query_option/2),
   30  retractall(M:setting_trill(_,_)),
   31  retractall(M:query_option(_,_)),
   32  retractall(M:tab_end(_)).
   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, setting_trill/2, tab_end/1, query_option/2),
   38  retractall(M:exp_found(_,_)),
   39  retractall(M:setting_trill(_,_)),
   40  retractall(M:query_option(_,_)),
   41  retractall(M:tab_end(_)),
   42  retractall(M:delta(_,_)).
   43
   44/***********
   45  Utilities for queries
   46 ***********/
   47
   48% findall
   49find_n_explanations(M,QueryType,QueryArgs,Expls,all):-
   50  !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N)
   51  findall(Expl,find_single_explanation(M,QueryType,QueryArgs,Expl),Expls).
   52
   53% find one in backtracking
   54find_n_explanations(M,QueryType,QueryArgs,Expl,bt):-
   55  !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N)
   56  find_single_explanation(M,QueryType,QueryArgs,Expl).
   57
   58% find_n_sol
   59find_n_explanations(M,QueryType,QueryArgs,Expls,N):-
   60  (number(N) -> % CUT so that no other calls to find_explanation can be ran
   61    (findnsols(N,Expl,find_single_explanation(M,QueryType,QueryArgs,Expl),Expls),!) % CUT otherwise findnsols would backtracks to look for another N sols
   62    ;
   63    (print_message(warning,wrong_number_max_expl),!,false)
   64  ).
   65
   66
   67% to find all axplanations for probabilistic queries
   68all_sub_class_int(M:ClassEx,SupClassEx,Exps):-
   69  all_unsat_int(M:intersectionOf([ClassEx,complementOf(SupClassEx)]),Exps).
   70
   71all_instanceOf_int(M:ClassEx,IndEx,Exps):-
   72  findall(Expl,instanceOf(M:ClassEx,IndEx,Expl),Exps).
   73
   74all_property_value_int(M:PropEx,Ind1Ex,Ind2Ex,Exps):-
   75  findall(Expl,property_value(M:PropEx,Ind1Ex,Ind2Ex,Expl),Exps).
   76
   77all_unsat_int(M:ConceptEx,Exps):-
   78  findall(Expl,unsat_internal(M:ConceptEx,Expl),Exps).
   79
   80
   81all_inconsistent_theory_int(M:Exps):-
   82  findall(Expl,inconsistent_theory(M:Expl),Exps).
   83
   84
   85compute_prob_and_close(M,Expl,QueryOptions):-
   86  M:query_option(compute_prob,expl),!,
   87  get_from_query_options(QueryOptions,compute_prob,expl,Prob),
   88  compute_prob_single_explanation(M,Expl,Prob),!.
   89
   90compute_prob_and_close(M,_,QueryOptions):-
   91  M:query_option(compute_prob,query),!,
   92  get_from_query_options(QueryOptions,compute_prob,query,Prob),
   93  findall(Exp,M:exp_found(qp,Exp),Exps),
   94  compute_prob(M,Exps,Prob),!.
   95
   96compute_prob_and_close(_M,_,_):-!.
   97
   98% checks the explanation
   99check_and_close(_,Expl0,Expl):-
  100  dif(Expl0,[]),
  101  sort(Expl0,Expl).
  102
  103is_expl(M,Expl):-
  104  dif(Expl,[]),
  105  dif(Expl,[[]]),
  106  initial_expl(M,EExpl),
  107  dif(Expl,EExpl).
  108
  109/*
  110find_expls(M,[],['inconsistent','kb'],E):-!,
  111  findall(Exp,M:exp_found(['inconsistent','kb'],Exp),Expl0),
  112  remove_supersets(Expl0,Expl),!,
  113  member(E,Expl).
  114
  115find_expls(M,[],_Q,_):-
  116  M:exp_found(['inconsistent','kb'],_),!,
  117  print_message(warning,inconsistent),!,false.
  118
  119find_expls(M,[],Q,E):-
  120  findall(Exp,M:exp_found(Q,Exp),Expl0),
  121  remove_supersets(Expl0,Expl),!,
  122  member(E,Expl).
  123*/
  124% checks if an explanations was already found (instance_of version)
  125find_expls(M,[Clash|_],Tab,E):- %gtrace,  % QueryArgs
  126  clash(M,Clash,Tab,EL0),
  127  member(E0-CPs0,EL0),
  128  sort(CPs0,CPs1),
  129  dif(E0,[]),
  130  sort(E0,E),
  131  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  132  % if it is so, the explanation is labelled as inconsistent kb via Q
  133  consistency_check(CPs1,[],Q),
  134  %findall(Exp,M:exp_found([C,I],Exp),Expl),
  135  %not_already_found(M,Expl,[C,I],E),
  136  ( dif(Q,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)),
  137  \+ M:exp_found(Q,E),
  138  assert(M:exp_found(Q,E)). % QueryArgs
  139
  140find_expls(M,[_Clash|Clashes],Tab,E):-
  141  find_expls(M,Clashes,Tab,E).
  142
  143% checks if an explanations was already found
  144find_expls_from_tab_list(M,[],E):-%gtrace,
  145  %findall(Exp-CPs,M:exp_found([C,I,CPs],Exp),Expl),
  146  %dif(Expl,[]),
  147  findall(Ex0,find_expls_from_choice_point_list(M,Ex0),L0),
  148  findall(Ex1,M:exp_found(_,Ex1),L1),
  149  append(L0,L1,L),
  150  remove_supersets(L,Ls),
  151  member(E,Ls),
  152  \+ M:exp_found(_,E),
  153  assert(M:exp_found(tc,E)).
  154
  155find_expls_from_tab_list(M,[Tab|_T],E):- %gtrace,  % QueryArgs
  156  get_solved_clashes(Tab,Clashes),
  157  member(Clash,Clashes),
  158  clash(M,Clash,Tab,EL0),
  159  member(E0-CPs0,EL0),
  160  sort(CPs0,CPs1),
  161  dif(E0,[]),
  162  sort(E0,E),
  163  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  164  % if it is so, the explanation is labelled as inconsistent kb via Q
  165  consistency_check(CPs1,CPs2,_),
  166  %dif(CPs2,[]),
  167  get_latest_choice(CPs2,ID,Choice),
  168  subtract(CPs1,[cpp(ID,Choice)],CPs), %remove cpp from CPs1 so the qp remains inside choice points list
  169  update_choice_point_list(M,ID,Choice,E,CPs),
  170  fail.
  171
  172
  173find_expls_from_tab_list(M,[_Tab|T],Expl):-
  174  %\+ length(T,0),
  175  find_expls_from_tab_list(M,T,Expl).
  176
  177
  178combine_expls_from_nondet_rules(M,cp(_,_,_,_,_,Expl),E):-%gtrace,
  179  check_non_empty_choice(Expl,ExplList),
  180  and_all_f(M,ExplList,ExplanationsList),
  181  %check_presence_of_other_choices(ExplanationsList,Explanations,Choices),
  182  member(E0-Choices0,ExplanationsList),
  183  sort(E0,E),
  184  sort(Choices0,Choices1),
  185  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  186  % if it is so, the explanation is labelled as inconsistent kb via Q
  187  consistency_check(Choices1,Choices,Q),
  188  (
  189    dif(Choices,[]) ->
  190    (
  191      %TODO gestione altri cp
  192      get_latest_choice(Choices,ID,Choice),
  193      subtract(Choices0,[cpp(ID,Choice)],CPs), %remove cpp from Choices1 so the qp remains inside choice points list
  194      update_choice_point_list(M,ID,Choice,E,CPs),
  195      fail % to force recursion
  196    ) ;
  197    (
  198      ( dif(Q,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)),
  199      \+ M:exp_found(Q,E)
  200    )
  201  ).
  202
  203find_expls_from_choice_point_list(M,E):-
  204  extract_choice_point_list(M,CP),
  205  (
  206    combine_expls_from_nondet_rules(M,CP,E) ;
  207    find_expls_from_choice_point_list(M,E)
  208  ).
  209
  210
  211check_non_empty_choice(Expl,ExplList):-
  212  dict_pairs(Expl,_,PairsList),
  213  findall(Ex,member(_-Ex,PairsList),ExplList),
  214  \+ memberchk([],ExplList).
  215
  216
  217check_presence_of_other_choices([],[],[]).
  218
  219check_presence_of_other_choices([E-[]|ExplanationsList],[E|Explanations],Choices):- !,
  220  check_presence_of_other_choices(ExplanationsList,Explanations,Choices).
  221
  222check_presence_of_other_choices([E-CP|ExplanationsList],[E|Explanations],[CP|Choices]):-
  223  check_presence_of_other_choices(ExplanationsList,Explanations,Choices).
  224
  225check_CP([],_).
  226
  227check_CP([cp(CP,N)|CPT],L):-
  228  findall(cp,member(_-[cp(CP,N)|CPT],L),ExplPartsList),
  229  length(ExplPartsList,N),
  230  check_CP(CPT,L).
  231
  232
  233not_already_found(_M,[],_Q,_E):-!.
  234
  235not_already_found(_M,[H|_T],_Q,E):-
  236  subset(H,E),!,
  237  fail.
  238
  239not_already_found(M,[H|_T],Q,E):-
  240  subset(E,H),!,
  241  retract(M:exp_found(Q,H)).
  242
  243not_already_found(M,[_H|T],Q,E):-
  244  not_already_found(M,T,Q,E).
  245
  246
  247get_latest_choice([],0,0).
  248
  249get_latest_choice(CPs,ID,Choice):-
  250  get_latest_choice_point(CPs,0,ID),
  251  get_latest_choice_of_cp(CPs,ID,0,Choice).
  252
  253get_latest_choice_point([],ID,ID).
  254
  255get_latest_choice_point([cpp(ID0,_)|T],ID1,ID):-
  256  ID2 is max(ID1,ID0),
  257  get_latest_choice_point(T,ID2,ID).
  258
  259
  260get_latest_choice_of_cp([],_,C,C).
  261
  262get_latest_choice_of_cp([cpp(ID,C0)|T],ID,C1,C):- !,
  263  C2 is max(C1,C0),
  264  get_latest_choice_of_cp(T,ID,C2,C).
  265
  266get_latest_choice_of_cp([_|T],ID,C1,C):-
  267  get_latest_choice_of_cp(T,ID,C1,C).
  268
  269
  270remove_supersets([H|T],ExplanationsList):-
  271  remove_supersets([H],T,ExplanationsList).
  272
  273remove_supersets(E,[],E).
  274
  275remove_supersets(E0,[H|T],ExplanationsList):-
  276  remove_supersets_int(E0,H,E),
  277  remove_supersets(E,T,ExplanationsList).
  278
  279remove_supersets_int(E0,H,E0):-
  280  memberchk(H,E0),!.
  281
  282remove_supersets_int(E0,H,E0):-
  283  member(H1,E0),
  284  subset(H1,H),!.
  285
  286remove_supersets_int(E0,H,E):-
  287  member(H1,E0),
  288  subset(H,H1),!,
  289  nth0(_,E0,H1,E1),
  290  remove_supersets_int(E1,H,E).
  291
  292remove_supersets_int(E,H,[H|E]).
  293
  294
  295% this predicate checks if there are inconsistencies in the KB, i.e., explanations with query placeholder qp
  296% if it is so, the explanation is labelled as inconsistent kb
  297%consistency_check(CPs,CPs,['inconsistent','kb'],['inconsistent','kb']):- !.
  298
  299consistency_check(CPs0,CPs,Q):-
  300  (nth0(_,CPs0,qp,CPs) -> (Q=qp) ; (Q=['inconsistent','kb'],CPs=CPs0)).
  301
  302
  303/****************************/
  304
  305/****************************
  306  TABLEAU ALGORITHM
  307****************************/
  308
  309% --------------
  310findClassAssertion4OWLNothing(_M,ABox,Expl):-
  311  findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl,ABox).
  312
  313
  314%-------------
  315% clash managing
  316
  317%------------
  318:- multifile clash/4.  319
  320/*
  321clash(M,maxCardinality(N,S,C)-Ind,Tab,Expl):-
  322  get_abox(Tab,ABox),
  323  %write('clash 9'),nl,
  324  findClassAssertion(maxCardinality(N,S,C),Ind,Expl1,ABox),
  325  s_neighbours(M,Ind,S,Tab,SN),
  326  individual_class_C(SN,C,ABox,SNC),
  327  length(SNC,LSS),
  328  LSS @> N,
  329  make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
  330
  331clash(M,maxCardinality(N,S)-Ind,Tab,Expl):-
  332  get_abox(Tab,ABox),
  333  %write('clash 10'),nl,
  334  findClassAssertion(maxCardinality(N,S),Ind,Expl1,ABox),
  335  s_neighbours(M,Ind,S,Tab,SN),
  336  length(SN,LSS),
  337  LSS @> N,
  338  make_expl(M,Ind,S,SN,Expl1,ABox,Expl).
  339
  340clash(M,exactCardinality(N,S,C)-Ind,Tab,Expl):-
  341  get_abox(Tab,ABox),
  342  %write('clash 9'),nl,
  343  findClassAssertion(exactCardinality(N,S,C),Ind,Expl1,ABox),
  344  s_neighbours(M,Ind,S,Tab,SN),
  345  individual_class_C(SN,C,ABox,SNC),
  346  length(SNC,LSS),
  347  dif(LSS,N),
  348  make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
  349
  350clash(M,exactCardinality(N,S)-Ind,Tab,Expl):-
  351  get_abox(Tab,ABox),
  352  %write('clash 10'),nl,
  353  findClassAssertion(exactCardinality(N,S),Ind,Expl1,ABox),
  354  s_neighbours(M,Ind,S,Tab,SN),
  355  length(SN,LSS),
  356  dif(LSS,N),
  357  make_expl(M,Ind,S,SN,Expl1,ABox,Expl).
  358
  359
  360
  361:- multifile check_clash/3.
  362
  363check_clash(M,maxCardinality(N,S,C)-Ind,Tab):-
  364  get_abox(Tab,ABox),
  365  %write('clash 9'),nl,
  366  s_neighbours(M,Ind,S,Tab,SN),
  367  individual_class_C(SN,C,ABox,SNC),
  368  length(SNC,LSS),
  369  LSS @> N,!.
  370  
  371check_clash(M,maxCardinality(N,S)-Ind,Tab):-
  372  %write('clash 10'),nl,
  373  s_neighbours(M,Ind,S,Tab,SN),
  374  length(SN,LSS),
  375  LSS @> N,!.
  376  
  377check_clash(M,exactCardinality(N,S,C)-Ind,Tab):-
  378  get_abox(Tab,ABox),
  379  %write('clash 9'),nl,
  380  s_neighbours(M,Ind,S,Tab,SN),
  381  individual_class_C(SN,C,ABox,SNC),
  382  length(SNC,LSS),
  383  dif(LSS,N),!.
  384  
  385check_clash(M,exactCardinality(N,S)-Ind,Tab):-
  386  %write('clash 10'),nl,
  387  s_neighbours(M,Ind,S,Tab,SN),
  388  length(SN,LSS),
  389  dif(LSS,N),!.
  390*/
  391
  392% --------------
  393
  394make_expl(_,_,_,[],Expl,_,Expl).
  395
  396make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):-
  397  findPropertyAssertion(S,Ind,H,Expl2,ABox),
  398  and_f(M,Expl2,Expl0,Expl1),
  399  make_expl(M,Ind,S,T,Expl1,ABox,Expl).
  400% --------------
  401
  402
  403/***********
  404  rules
  405************/
  406
  407/*
  408  unfold_rule
  409  ===========
  410*/
  411
  412% ----------------
  413% unionOf, intersectionOf, subClassOf, negation, allValuesFrom, someValuesFrom, exactCardinality(min and max), maxCardinality, minCardinality
  414:- multifile find_neg_class/2.  415
  416find_neg_class(exactCardinality(N,R,C),unionOf([maxCardinality(NMax,R,C),minCardinality(NMin,R,C)])):-
  417  NMax is N - 1,
  418  NMin is N + 1.
  419
  420find_neg_class(minCardinality(N,R,C),maxCardinality(NMax,R,C)):-
  421  NMax is N - 1.
  422
  423find_neg_class(maxCardinality(N,R,C),minCardinality(NMin,R,C)):-
  424  NMin is N + 1.
  425
  426%-----------------
  427:- multifile find_sub_sup_class/4.  428
  429%role for concepts exactCardinality
  430find_sub_sup_class(M,exactCardinality(N,R),exactCardinality(N,S),subPropertyOf(R,S)):-
  431  M:subPropertyOf(R,S).
  432
  433%concept for concepts exactCardinality
  434find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,R,D),Ax):-
  435  find_sub_sup_class(M,C,D,Ax),
  436  atomic(D).
  437
  438%role for concepts exactCardinality
  439find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,S,C),subPropertyOf(R,S)):-
  440  M:subPropertyOf(R,S).
  441
  442%role for concepts maxCardinality
  443find_sub_sup_class(M,maxCardinality(N,R),maxCardinality(N,S),subPropertyOf(R,S)):-
  444  M:subPropertyOf(R,S).
  445
  446%concept for concepts maxCardinality
  447find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,R,D),Ax):-
  448  find_sub_sup_class(M,C,D,Ax),
  449  atomic(D).
  450
  451%role for concepts maxCardinality
  452find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,S,C),subPropertyOf(R,S)):-
  453  M:subPropertyOf(R,S).
  454
  455%role for concepts minCardinality
  456find_sub_sup_class(M,minCardinality(N,R),minCardinality(N,S),subPropertyOf(R,S)):-
  457  M:subPropertyOf(R,S).
  458
  459%concept for concepts minCardinality
  460find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,R,D),Ax):-
  461  find_sub_sup_class(M,C,D,Ax),
  462  atomic(D).
  463
  464%role for concepts minCardinality
  465find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,S,C),subPropertyOf(R,S)):-
  466  M:subPropertyOf(R,S).
  467
  468/* ************* */
  469
  470/***********
  471  update abox
  472  utility for tableau
  473************/
  474modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
  475  length(LF,1),!.
  476
  477modify_ABox(M,Tab0,sameIndividual(LF),Expl1,Tab):-
  478  get_abox(Tab0,ABox0),
  479  ( find((sameIndividual(L),Expl0),ABox0) ->
  480  	( sort(L,LS),
  481  	  sort(LF,LFS),
  482  	  LS = LFS,!,
  483  	  absent(Expl0,Expl1,Expl),
  484      remove_from_abox(ABox0,[(sameIndividual(L),Expl0)],ABox)
  485  	)
  486  ;
  487  	(ABox = ABox0,Expl = Expl1,L = LF)
  488  ),
  489  add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
  490  set_abox(Tab1,[(sameIndividual(L),Expl)|ABox],Tab).
  491
  492modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
  493  length(LF,1),!.
  494
  495modify_ABox(M,Tab0,differentIndividuals(LF),Expl1,Tab):-
  496  get_abox(Tab0,ABox0),
  497  ( find((differentIndividuals(L),Expl0),ABox0) ->
  498  	( sort(L,LS),
  499  	  sort(LF,LFS),
  500  	  LS = LFS,!,
  501  	  absent(Expl0,Expl1,Expl),
  502  	  remove_from_abox(ABox0,[(differentIndividuals(L),Expl0)],ABox)
  503  	)
  504  ;
  505  	(ABox = ABox0,Expl = Expl1,L = LF)
  506  ),
  507  add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
  508  set_abox(Tab1,[(differentIndividuals(L),Expl)|ABox],Tab).
  509
  510modify_ABox(M,Tab0,C,Ind,Expl1,Tab):-
  511  get_abox(Tab0,ABox0),
  512  ( find((classAssertion(C,Ind),Expl0),ABox0) ->
  513    ( absent(Expl0,Expl1,Expl),
  514      remove_from_abox(ABox0,(classAssertion(C,Ind),Expl0),ABox)
  515    )
  516  ;
  517    (ABox = ABox0,Expl = Expl1)
  518  ),
  519  add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
  520  set_abox(Tab1,[(classAssertion(C,Ind),Expl)|ABox],Tab2),
  521  update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
  522
  523modify_ABox(M,Tab0,P,Ind1,Ind2,Expl1,Tab):-
  524  get_abox(Tab0,ABox0),
  525  ( find((propertyAssertion(P,Ind1,Ind2),Expl0),ABox0) ->
  526    ( absent(Expl0,Expl1,Expl),
  527      remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl0),ABox)
  528    )
  529  ;
  530    (ABox = ABox0,Expl = Expl1)
  531  ),
  532  add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
  533  set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab2),
  534  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
  535
  536/* ************* */
  537
  538% -------------------
  539notDifferentIndividuals(M,X,Y,ABox):-
  540  \+ inAssertDifferentIndividuals(M,X,Y),
  541  \+ inABoxDifferentIndividuals(X,Y,ABox).
  542
  543% --------------
  544
  545inAssertDifferentIndividuals(M,differentIndividuals(X),differentIndividuals(Y)):-
  546  !,
  547  M:differentIndividuals(LI),
  548  member(X0,X),
  549  member(X0,LI),
  550  member(Y0,Y),
  551  member(Y0,LI).
  552
  553inAssertDifferentIndividuals(M,X,sameIndividual(Y)):-
  554  !,
  555  M:differentIndividuals(LI),
  556  member(X,LI),
  557  member(Y0,Y),
  558  member(Y0,LI).
  559
  560inAssertDifferentIndividuals(M,sameIndividual(X),Y):-
  561  !,
  562  M:differentIndividuals(LI),
  563  member(X0,X),
  564  member(X0,LI),
  565  member(Y,LI).
  566
  567inAssertDifferentIndividuals(M,X,Y):-
  568  M:differentIndividuals(LI),
  569  member(X,LI),
  570  member(Y,LI).
  571
  572% ------------------
  573
  574inABoxDifferentIndividuals(sameIndividual(X),sameIndividual(Y),ABox):-
  575  !,
  576  find((differentIndividuals(LI),_),ABox),
  577  member(X0,X),
  578  member(X0,LI),
  579  member(Y0,Y),
  580  member(Y0,LI).
  581
  582inABoxDifferentIndividuals(X,sameIndividual(Y),ABox):-
  583  !,
  584  find((differentIndividuals(LI),_),ABox),
  585  member(X,LI),
  586  member(Y0,Y),
  587  member(Y0,LI).
  588
  589inABoxDifferentIndividuals(sameIndividual(X),Y,ABox):-
  590  !,
  591  find((differentIndividuals(LI),_),ABox),
  592  member(X0,X),
  593  member(X0,LI),
  594  member(Y,LI).
  595
  596inABoxDifferentIndividuals(X,Y,ABox):-
  597  find((differentIndividuals(LI),_),ABox),
  598  member(X,LI),
  599  member(Y,LI).
  600
  601% --------------------
  602
  603listIntersection([],_,[]).
  604
  605listIntersection([HX|TX],LCY,TI):-
  606  \+ member(HX,LCY),
  607  listIntersection(TX,LCY,TI).
  608
  609listIntersection([HX|TX],LCY,[HX|TI]):-
  610  member(HX,LCY),
  611  listIntersection(TX,LCY,TI).
  612
  613% ---------------
  614
  615findExplForClassOf(LC,LI,ABox0,Expl):-
  616  member(C,LC),
  617  member(I,LI),
  618  findClassAssertion(C,I,Expl,ABox0).
  619%  member((classAssertion(C,I),Expl),ABox0).
  620
  621/* ************ */
  622
  623
  624/*  absent
  625  =========
  626*/
  627absent(Expl0,Expl1,Expl):- % Expl0 already present expls, Expl1 new expls to add, Expl the combination of two lists
  628  absent0(Expl0,Expl1,Expl),!.
  629
  630%------------------
  631absent0(Expl0,Expl1,Expl):-
  632  absent1(Expl0,Expl1,Expl,Added),
  633  dif(Added,0).
  634
  635absent1(Expl,[],Expl,0).
  636
  637absent1(Expl0,[H-CP|T],[H-CP|Expl],1):-
  638  absent2(Expl0,H),!,
  639  absent1(Expl0,T,Expl,_).
  640
  641absent1(Expl0,[_|T],Expl,Added):-
  642  absent1(Expl0,T,Expl,Added).
  643
  644absent2([H-_],Expl):- !,
  645  \+ subset(H,Expl).
  646
  647absent2([H-_|T],Expl):-
  648  \+ subset(H,Expl),!,
  649  absent2(T,Expl).
  650
  651/* **************** */
  652
  653/*
  654  build_abox
  655  ===============
  656*/
  657
  658/*build_abox(M,ABox):-
  659  findall((classAssertion(Class,Individual),[classAssertion(Class,Individual)]),classAssertion(Class,Individual),LCA),
  660  findall((propertyAssertion(Property,Subject, Object),[propertyAssertion(Property,Subject, Object)]),propertyAssertion(Property,Subject, Object),LPA),
  661  findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property,Subject,Object),propertyAssertion(SubProperty,Subject,Object)]),subPropertyOf(SubProperty,Property),LSPA),
  662  new_abox(ABox0),
  663  add_all_to_tableau(LCA,ABox0,ABox1),
  664  add_all_to_tableau(LPA,ABox1,ABox2),
  665  add_all_to_tableau(LSPA,ABox2,ABox).
  666*/
  667
  668
  669build_abox(M,Tableau,QueryType,QueryArgs):-
  670  retractall(M:final_abox(_)),
  671  collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
  672  get_axioms_of_individuals(M,ConnectedInds,LCA,LPA,LNA,LDIA,LSIA),
  673  new_abox(ABox0),
  674  new_tabs(Tabs0),
  675  init_expansion_queue(LCA,LPA,ExpansionQueue),
  676  init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
  677  %append([LCA,LPA,LDIA],CreateTabsList),
  678  %create_tabs(CreateTabsList,Tableau0,Tableau1),
  679  append([LCA,LPA,LNA,LDIA],AddAllList),
  680  add_all_to_tableau(M,AddAllList,Tableau0,Tableau2),
  681  merge_all_individuals(M,LSIA,Tableau2,Tableau3),
  682  add_owlThing_list(M,Tableau3,Tableau),
  683  !.
  684
  685
  686get_axioms_of_individuals(M,IndividualsList,LCA,LPA,LNA,LDIA,LSIA):-
  687  ( dif(IndividualsList,[]) ->
  688    ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),(member(Individual,IndividualsList),M:classAssertion(Class,Individual)),LCA),
  689      findall((propertyAssertion(Property,Subject, Object),[[propertyAssertion(Property,Subject, Object)]-[]]),(member(Subject,IndividualsList),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA),
  690      findall(nominal(NominalIndividual),(member(NominalIndividual,IndividualsList),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
  691      findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),(M:differentIndividuals(Ld),intersect(Ld,IndividualsList)),LDIA),
  692      findall((sameIndividual(L),[[sameIndividual(L)]-[]]),(M:sameIndividual(L),intersect(L,IndividualsList)),LSIA)
  693    )
  694    ; % all the individuals
  695    ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),M:classAssertion(Class,Individual),LCA),
  696      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),
  697      findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
  698      findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),M:differentIndividuals(Ld),LDIA),
  699      findall((sameIndividual(L),[[sameIndividual(L)]-[]]),M:sameIndividual(L),LSIA)
  700    )
  701  ).
  702
  703
  704/* ********** */
  705
  706/**********************
  707
  708  Explanation Management
  709
  710***********************/
  711
  712and_all_f(M,ExplPartsList,E) :-
  713  empty_expl(M,EmptyE),
  714  and_all_f(M,ExplPartsList,EmptyE,E).
  715
  716and_all_f(_,[],E,E) :- !.
  717
  718and_all_f(M,[H|T],E0,E):-
  719  and_f(M,E0,H,E1),
  720  and_all_f(M,T,E1,E).
  721
  722initial_expl(_M,[[]-[]]):-!.
  723
  724empty_expl(_M,[[]-[]]):-!.
  725
  726and_f_ax(M,Axiom,F0,F):-
  727  and_f(M,[[Axiom]-[]],F0,F).
  728
  729and_f(_M,[],[],[]):- !.
  730
  731and_f(_M,[],L,L):- !.
  732
  733and_f(_M,L,[],L):- !.
  734
  735and_f(_M,L1,L2,F):-
  736  and_f1(L1,L2,[],F).
  737
  738and_f1([],_,L,L).
  739
  740and_f1([H1-CP1|T1],L2,L3,L):-
  741  and_f2(H1,CP1,L2,L12),
  742  append(L3,L12,L4),
  743  and_f1(T1,L2,L4,L).
  744
  745and_f2(_,_,[],[]):- !.
  746
  747/*
  748and_f2(L1,CP1,[H2-CP2|T2],[H-CP|T]):-%gtrace,
  749  can_i_and(L1,CP1,H2,CP2),!,
  750  ( subset(L1,H2) -> 
  751    H = H2
  752    ;
  753    ( subset(H2,L1) -> 
  754      H = L1
  755      ;
  756      append(L1,H2,H)
  757    )
  758  ),
  759  append(CP1,CP2,CP),
  760  and_f2(L1,CP1,T2,T).
  761*/
  762
  763
  764and_f2(L1,CP1,[H2-CP2|T2],[H-CP|T]):-%gtrace,
  765  append(L1,H2,H),
  766  append(CP1,CP2,CP),
  767  and_f2(L1,CP1,T2,T).
  768
  769
  770can_i_and(L1,CP1,H2,CP2):-
  771  dif(L1,[]),
  772  dif(H2,[]),
  773  (member(A,CP1),
  774  member(A,CP2)),!.
  775
  776same_cpp_or_not(CP1,CP2):-
  777  (\+ member(cpp(_,_),CP1) ; \+ member(cpp(_,_),CP2)),!.
  778
  779or_f([],E,E).
  780
  781or_f([E0|T],E1,E):-
  782  memberchk(E0,E1),!,
  783  or_f(T,E1,E).
  784
  785or_f([E0|T],E1,[E0|E]):-
  786  or_f(T,E1,E).
  787
  788/**********************
  789
  790Choice Points Management
  791
  792***********************/
  793
  794/*
  795  Initializes delta/2 containing the list of choice points and the number of choice points created.
  796  Every choice point is modeled by the predicate cp/5 containing the ID of the choice point,
  797  the individual and the class that triggered the creation of the choice point,
  798  the rule that created the cp:
  799  - or: or_rule
  800  - mr: max_rule
  801  Also it contains the list of possible choices and the explanations for each choice.
  802*/
  803init_delta(M):-
  804  retractall(M:delta(_,_)),
  805  assert(M:delta([],0)).
  806
  807get_choice_point_id(M,ID):-
  808  M:delta(_,ID).
  809
  810% Creates a new choice point and adds it to the delta/2 set of choice points.
  811create_choice_point(M,Ind,Rule,Class,Choices,ID0):-
  812  init_expl_per_choice(Choices,ExplPerChoice),
  813  M:delta(CPList,ID0),
  814  ID is ID0 + 1,
  815  retractall(M:delta(_,_)),
  816  assert(M:delta([cp(ID0,Ind,Rule,Class,Choices,ExplPerChoice)|CPList],ID)).
  817
  818
  819init_expl_per_choice(Choices,ExplPerChoice):-
  820  length(Choices,N),
  821  init_expl_per_choice_int(0,N,epc{0:[]},ExplPerChoice).
  822
  823init_expl_per_choice_int(N,N,ExplPerChoice,ExplPerChoice).
  824
  825init_expl_per_choice_int(N0,N,ExplPerChoice0,ExplPerChoice):-
  826  ExplPerChoice1 = ExplPerChoice0.put(N0,[]),
  827  N1 is N0 + 1,
  828  init_expl_per_choice_int(N1,N,ExplPerChoice1,ExplPerChoice).
  829
  830
  831% cpp/2 is the choice point pointer. It contains the CP's ID (from the list of choice points delta/2)
  832% and the pointer of the choice maide at the choice point
  833add_choice_point(_,_,[],[]). 
  834
  835add_choice_point(_,CPP,[Expl-CP0|T0],[Expl-CP|T]):- %CPP=cpp(CPID,N)
  836  (
  837    dif(CP0,[]) ->
  838    (
  839        append([CPP],CP0,CP)
  840    )
  841    ;
  842    (
  843      CP = [CPP]
  844    )
  845  ),
  846  add_choice_point(_,CPP,T0,T).
  847
  848
  849get_choice_point_list(M,CP):-
  850  M:delta(CP,_).
  851
  852extract_choice_point_list(M,CP):-
  853  M:delta([CP|CPList],ID),
  854  retractall(M:delta(_,_)),
  855  assert(M:delta(CPList,ID)).
  856
  857update_choice_point_list(M,ID,Choice,E,CPs):-
  858  M:delta(CPList0,ID0),
  859  memberchk(cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),CPList0),
  860  ExplToUpdate = ExplPerChoice0.get(Choice), 
  861  ( % if the set of explanations for the choice is empty it simply adds the new explanation -> union i.e., append([E-CPs],ExplToUpdate,ExplUpdated)
  862    % otherwise it adds only new explanations dropping those that are already present or those that are supersets of 
  863    % already present explanations -> absent(ExplToUpdate,[E-CPs],ExplUpdated)
  864    dif(ExplToUpdate,[]) ->
  865    (
  866      or_f(ExplToUpdate,[E-CPs],ExplUpdated)
  867    ) ;
  868    (
  869      ExplUpdated=[E-CPs]
  870    )
  871  ),
  872  ExplPerChoice = ExplPerChoice0.put(Choice,ExplUpdated),
  873  update_choice_point_list_int(CPList0,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,CPList),
  874  retractall(M:delta(_,_)),
  875  assert(M:delta(CPList,ID0)).
  876
  877update_choice_point_list_int([],_,_,[]):-
  878  writeln("Probably something wrong happened. Please report the problem opening an issue on github!").
  879  % It should never arrive here.
  880
  881update_choice_point_list_int([cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0)|T],
  882                    cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,
  883                    [cp(ID,Ind,Rule,Class,Choices,ExplPerChoice)|T]) :- !.
  884
  885update_choice_point_list_int([H|T],
  886                  cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,
  887                  [H|T1]):-
  888  update_choice_point_list_int(T,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,T1).
  889
  890/**********************
  891
  892 TRILL Probability Computation
  893
  894***********************/
  895
  896get_bdd_environment(_M,Env):-
  897  init(Env).
  898
  899clean_environment(_M,Env):-
  900  end(Env).
  901
  902
  903build_bdd(M,Env,[X],BDD):- !,
  904  bdd_and(M,Env,X,BDD).
  905
  906build_bdd(M,Env, [H|T],BDD):-
  907  build_bdd(M,Env,T,BDDT),
  908  bdd_and(M,Env,H,BDDH),
  909  or(Env,BDDH,BDDT,BDD).
  910
  911build_bdd(_M,Env,[],BDD):- !,
  912  zero(Env,BDD).
  913
  914
  915bdd_and(M,Env,[X],BDDX):-
  916  get_prob_ax(M,X,AxN,Prob),!,
  917  ProbN is 1-Prob,
  918  get_var_n(Env,AxN,[],[Prob,ProbN],VX),
  919  equality(Env,VX,0,BDDX),!.
  920
  921bdd_and(_M,Env,[_X],BDDX):- !,
  922  one(Env,BDDX).
  923
  924bdd_and(M,Env,[H|T],BDDAnd):-
  925  get_prob_ax(M,H,AxN,Prob),!,
  926  ProbN is 1-Prob,
  927  get_var_n(Env,AxN,[],[Prob,ProbN],VH),
  928  equality(Env,VH,0,BDDH),
  929  bdd_and(M,Env,T,BDDT),
  930  and(Env,BDDH,BDDT,BDDAnd).
  931  
  932bdd_and(M,Env,[_H|T],BDDAnd):- !,
  933  one(Env,BDDH),
  934  bdd_and(M,Env,T,BDDT),
  935  and(Env,BDDH,BDDT,BDDAnd)