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