1/* tornado 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,[and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule]).
   24setting_trill_default(nondet_rules,[or_rule]).
   25
   26set_up(M):-
   27  utility_translation:set_up(M),
   28  M:(dynamic exp_found/2, keep_env/0, tornado_bdd_environment/1, inconsistent_theory_flag/0, setting_trill/2, tab_end/1, query_option/2),
   29  retractall(M:setting_trill(_,_)),
   30  retractall(M:query_option(_,_)),
   31  retractall(M:tab_end(_)).
   32  %retractall(M:setting_trill(_,_)),
   33  %prune_tableau_rules(M).
   34  %foreach(setting_trill_default(DefaultSetting,DefaultVal),assert(M:setting_trill(DefaultSetting,DefaultVal))).
   35
   36clean_up(M):-
   37  utility_translation:clean_up(M),
   38  M:(dynamic exp_found/2, keep_env/0, tornado_bdd_environment/1, inconsistent_theory_flag/0, setting_trill/2, tab_end/1, query_option/2),
   39  retractall(M:exp_found(_,_)),
   40  retractall(M:keep_env),
   41  retractall(M:tornado_bdd_environment(_)),
   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 assert(M:keep_env),
   69 find_single_explanation(M,QueryType,QueryArgs,Expls),!.
   70
   71find_n_explanations(M,_,_,Expls,_):-
   72 initial_expl(M,Expls-_).
   73
   74
   75compute_prob_and_close(M,Exps-_,QueryOptions):-
   76  M:query_option(compute_prob,CPType),!,
   77  get_from_query_options(QueryOptions,compute_prob,CPType,Prob),
   78  compute_prob(M,Exps,Prob),!,
   79  retractall(M:keep_env),!.
   80
   81compute_prob_and_close(_M,_,_):-!.
   82
   83% checks the explanation
   84check_and_close(M,Expl,Expl):-
   85  M:keep_env,!.
   86
   87check_and_close(M,Expl,dot(Dot)):-
   88  get_bdd_environment(M,Env),
   89  create_dot_string(Env,Expl,Dot),
   90  clean_environment(M,Env).
   91
   92is_expl(M,Expl-_):-
   93  initial_expl(M,EExpl-_),
   94  dif(Expl,EExpl).
   95
   96
   97find_expls(M,_,_,_):-
   98  (M:inconsistent_theory_flag -> print_message(warning,inconsistent) ; true),!,false.
   99
  100% checks if an explanations was already found
  101find_expls_from_tab_list(M,[],BDD):-
  102  empty_expl(M,BDD),!.
  103
  104% checks if an explanations was already found (instance_of version)
  105find_expls_from_tab_list(M,[Tab|T],E):-
  106  get_solved_clashes(Tab,Clashes),
  107  findall(E0,(member(Clash,Clashes),clash(M,Clash,Tab,E0)),Expls0),!,
  108  % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  109  consistency_check(M,Expls0,Q),
  110  ( dif(Q,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)),
  111  or_all_f(M,Expls0,Expls1),
  112  find_expls_from_tab_list(M,T,E1),
  113  and_f(M,Expls1,E1,E).
  114
  115  find_expls_from_tab_list(M,[_Tab|T],Expl):-
  116  \+ length(T,0),
  117  find_expls_from_tab_list(M,T,Expl).
  118
  119% this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp
  120consistency_check(_,[],qp):-!.
  121
  122consistency_check(M,[_-CPs|T],Q):-
  123  dif(CPs,[]),!,
  124  member(qp,CPs),!,
  125  consistency_check(M,T,Q).
  126
  127consistency_check(M,_,['inconsistent','kb']):-!,
  128  assert(M:inconsistent_theory_flag).
  129
  130/****************************/
  131
  132/****************************
  133  TABLEAU ALGORITHM
  134****************************/
  135
  136% --------------
  137findClassAssertion4OWLNothing(M,ABox,Expl):-
  138  findall(Expl1,findClassAssertion('http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl1,ABox),Expls),
  139  dif(Expls,[]),
  140  or_all_f(M,Expls,Expl).
  141
  142/* ************* */
  143
  144/***********
  145  update abox
  146  utility for tableau
  147************/
  148modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):-
  149  length(LF,1),!.
  150
  151modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
  152  get_abox(Tab0,ABox0),
  153  find((sameIndividual(L),Expl1),ABox0),!,
  154  sort(L,LS),
  155  sort(LF,LFS),
  156  LS = LFS,!,
  157  dif(L0,Expl1),
  158  test(M,L0,Expl1,Expl),
  159  remove_from_abox(ABox0,[(sameIndividual(L),Expl1)],ABox),
  160  set_abox(Tab0,[(sameIndividual(L),Expl)|ABox],Tab).
  161
  162modify_ABox(M,Tab0,sameIndividual(LF),L0,Tab):-
  163  add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1),
  164  get_abox(Tab0,ABox0),
  165  set_abox(Tab1,[(sameIndividual(LF),L0)|ABox0],Tab).
  166
  167modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):-
  168  length(LF,1),!.
  169
  170modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
  171  get_abox(Tab0,ABox0),
  172  find((sameIndividual(L),Expl1),ABox0),!,
  173  sort(L,LS),
  174  sort(LF,LFS),
  175  LS = LFS,!,
  176  dif(L0,Expl1),
  177  test(M,L0,Expl1,Expl),
  178  remove_from_abox(ABox0,[(differentIndividuals(L),Expl1)],ABox),
  179  set_abox(Tab0,[(differentIndividuals(L),Expl)|ABox],Tab).
  180
  181modify_ABox(M,Tab0,differentIndividuals(LF),L0,Tab):-
  182  add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1),
  183  get_abox(Tab0,ABox),
  184  set_abox(Tab1,[(differentIndividuals(LF),L0)|ABox],Tab).
  185
  186modify_ABox(M,Tab0,C,Ind,L0,Tab):-
  187  get_abox(Tab0,ABox0),
  188  findClassAssertion(C,Ind,Expl1,ABox0),!,
  189  dif(L0,Expl1),
  190  test(M,L0,Expl1,Expl),
  191  remove_from_abox(ABox0,(classAssertion(C,Ind),Expl1),ABox),
  192  set_abox(Tab0,[(classAssertion(C,Ind),Expl)|ABox],Tab1),
  193  update_expansion_queue_in_tableau(M,C,Ind,Tab1,Tab).
  194  
  195modify_ABox(M,Tab0,C,Ind,L0,Tab):-
  196  add_clash_to_tableau(M,Tab0,C-Ind,Tab1),
  197  get_abox(Tab0,ABox),
  198  set_abox(Tab1,[(classAssertion(C,Ind),L0)|ABox],Tab2),
  199  update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab).
  200
  201
  202modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
  203  get_abox(Tab0,ABox0),
  204  findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox0),!,
  205  dif(L0,Expl1),
  206  test(M,L0,Expl1,Expl),
  207  remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl1),ABox),
  208  set_abox(Tab0,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab1),
  209  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab1,Tab).
  210  
  211  
  212modify_ABox(M,Tab0,P,Ind1,Ind2,L0,Tab):-
  213  add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1),
  214  get_abox(Tab0,ABox0),
  215  set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),L0)|ABox0],Tab2),
  216  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab).
  217
  218/* ************* */
  219
  220
  221/*
  222  build_abox
  223  ===============
  224*/
  225
  226build_abox(M,Tableau,QueryType,QueryArgs):-
  227  retractall(M:final_abox(_)),
  228  retractall(v(_,_,_)),
  229  retractall(na(_,_)),
  230  retractall(rule_n(_)),
  231  assert(rule_n(0)),
  232  get_bdd_environment(M,Env),
  233  collect_individuals(M,QueryType,QueryArgs,ConnectedInds),
  234  ( dif(ConnectedInds,[]) ->
  235    ( findall((classAssertion(Class,Individual),BDDCA-[]),(member(Individual,ConnectedInds),M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
  236      findall((propertyAssertion(Property,Subject, Object),BDDPA-[]),(member(Subject,ConnectedInds),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property),bdd_and(M,Env,[propertyAssertion(Property,Subject, Object)],BDDPA)),LPA),
  237      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  238      findall(nominal(NominalIndividual),(member(NominalIndividual,ConnectedInds),M:classAssertion(oneOf(_),NominalIndividual)),LNA),
  239      findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),intersect(Ld,ConnectedInds),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
  240      findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),intersect(L,ConnectedInds),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
  241    )
  242    ; % all the individuals
  243    ( findall((classAssertion(Class,Individual),BDDCA-[]),(M:classAssertion(Class,Individual),bdd_and(M,Env,[classAssertion(Class,Individual)],BDDCA)),LCA),
  244      findall((propertyAssertion(Property,Subject, Object),BDDPA-[]),(M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property),bdd_and(M,Env,[propertyAssertion(Property,Subject, Object)],BDDPA)),LPA),
  245      % findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property),propertyAssertion(SubProperty,Subject,Object)]),subProp(M,SubProperty,Property,Subject,Object),LSPA),
  246      findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA),
  247      findall((differentIndividuals(Ld),BDDDIA-[]),(M:differentIndividuals(Ld),bdd_and(M,Env,[differentIndividuals(Ld)],BDDDIA)),LDIA),
  248      findall((sameIndividual(L),BDDSIA-[]),(M:sameIndividual(L),bdd_and(M,Env,[sameIndividual(L)],BDDSIA)),LSIA)
  249    )
  250  ),
  251  new_abox(ABox0),
  252  new_tabs(Tabs0),
  253  init_expansion_queue(LCA,LPA,ExpansionQueue),
  254  init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0),
  255  append([LCA,LDIA,LPA],CreateTabsList),
  256  create_tabs(CreateTabsList,Tableau0,Tableau1),
  257  append([LCA,LPA,LNA,LDIA],AddAllList),
  258  add_all_to_tableau(M,AddAllList,Tableau1,Tableau2),
  259  merge_all_individuals(M,LSIA,Tableau2,Tableau3),
  260  add_owlThing_list(M,Tableau3,Tableau),
  261  !.
  262
  263/**********************
  264
  265Explanation Management
  266
  267***********************/
  268
  269initial_expl(M,BDD-[]):-
  270  get_bdd_environment(M,Env),
  271  zero(Env,BDD).
  272
  273empty_expl(M,BDD-[]):-
  274  get_bdd_environment(M,Env),
  275  one(Env,BDD).
  276
  277and_f_ax(M,Axiom,BDD0,BDD):-
  278  get_bdd_environment(M,Env),
  279  bdd_and(M,Env,[Axiom],BDDAxiom),
  280  and_f(M,BDDAxiom-[],BDD0,BDD).
  281
  282% and between two BDDs
  283and_f(_,[],BDD,BDD):- !.
  284
  285and_f(_,BDD,[],BDD):- !.
  286
  287and_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
  288  get_bdd_environment(M,Env),
  289  and(Env,BDD0,BDD1,BDD),
  290  append(CP0,CP1,CP).
  291
  292
  293% or between two formulae
  294or_all_f(M,[],BDD):-
  295  initial_expl(M,BDD),!.
  296
  297or_all_f(M,[H|T],Expl):-
  298  or_all_f(M,T,Expl1),
  299  or_f(M,H,Expl1,Expl),!.
  300
  301or_f(_,[],BDD,BDD):- !.
  302  
  303or_f(_,BDD,[],BDD):- !.
  304  
  305or_f(M,BDD0-CP0,BDD1-CP1,BDD-CP):-
  306  get_bdd_environment(M,Env),
  307  or(Env,BDD0,BDD1,BDD),
  308  append(CP0,CP1,CP).
  309
  310
  311/**********************
  312
  313TORNADO TEST
  314
  315***********************/
  316
  317test(M,L1,L2-CP2,F-CP):-
  318  %build_f(L1,L2,F),
  319  %sat(F).
  320  or_f(M,L1,L2-CP2,F-CP),
  321  dif(L2,F).
  322
  323
  324/**********************
  325
  326Choice Points Management
  327
  328***********************/
  329
  330get_choice_point_id(_,0).
  331
  332create_choice_point(_,_,_,_,_,0).
  333
  334add_choice_point(_,qp,Expl-CP0,Expl-CP):- !,
  335  (memberchk(qp,CP0) -> CP=CP0; CP=[qp]).
  336
  337add_choice_point(_,_,Expl,Expl):- !.
  338
  339
  340/**********************
  341
  342 TORNADO Probability Computation
  343
  344***********************/
  345
  346get_bdd_environment(M,Env):- 
  347  M:tornado_bdd_environment(Env),!.
  348
  349get_bdd_environment(M,Env):-
  350  init(Env),
  351  M:assert(tornado_bdd_environment(Env)).
  352
  353clean_environment(M,Env):-
  354  end(Env),
  355  retractall(M:tornado_bdd_environment(_)).
  356
  357build_bdd(_,Env,[],BDD):- !,
  358  zero(Env,BDD).
  359
  360build_bdd(_,_Env,BDD,BDD).
  361
  362bdd_and(M,Env,[X],BDDX):-
  363  get_prob_ax(M,X,AxN,Prob),!,
  364  ProbN is 1-Prob,
  365  get_var_n(Env,AxN,[],[Prob,ProbN],VX),
  366  equality(Env,VX,0,BDDX),!.
  367
  368bdd_and(_M,Env,[_X],BDDX):- !,
  369  one(Env,BDDX)