trill

   20:- module(trill,[sub_class/2, sub_class/3, prob_sub_class/3, sub_class/4, all_sub_class/3,
   21                 instanceOf/2, instanceOf/3, prob_instanceOf/3, instanceOf/4, all_instanceOf/3,
   22                 property_value/3, property_value/4, prob_property_value/4, property_value/5, all_property_value/4,
   23                 unsat/1, unsat/2, prob_unsat/2, unsat/3, all_unsat/2,
   24                 inconsistent_theory/0, inconsistent_theory/1, prob_inconsistent_theory/1, inconsistent_theory/2, all_inconsistent_theory/1,
   25                 resume_query/1, compute_query_prob/1, reset_query/0,
   26                 axiom/1, kb_prefixes/1, add_kb_prefix/2, add_kb_prefixes/1, add_axiom/1, add_axioms/1, remove_kb_prefix/2, remove_kb_prefix/1, remove_axiom/1, remove_axioms/1,
   27                 load_kb/1, load_owl_kb/1, load_owl_kb_from_string/1, init_trill/1,
   28                 set_tableau_expansion_rules/2] ).   29
   30:- meta_predicate sub_class(:,+).   31:- meta_predicate sub_class(:,+,-).   32:- meta_predicate sub_class(:,+,-,+).   33:- meta_predicate all_sub_class(:,+,-).   34:- meta_predicate prob_sub_class(:,+,-).   35:- meta_predicate instanceOf(:,+).   36:- meta_predicate instanceOf(:,+,-).   37:- meta_predicate instanceOf(:,+,-,+).   38:- meta_predicate all_instanceOf(:,+,-).   39:- meta_predicate prob_instanceOf(:,+,-).   40:- meta_predicate property_value(:,+,+).   41:- meta_predicate property_value(:,+,+,-).   42:- meta_predicate property_value(:,+,+,-,+).   43:- meta_predicate all_property_value(:,+,+,-).   44:- meta_predicate prob_property_value(:,+,+,-).   45:- meta_predicate unsat(:).   46:- meta_predicate unsat(:,-).   47:- meta_predicate unsat(:,-,+).   48:- meta_predicate all_unsat(:,-).   49:- meta_predicate prob_unsat(:,-).   50:- meta_predicate inconsistent_theory(:).   51:- meta_predicate inconsistent_theory(:,+).   52:- meta_predicate all_inconsistent_theory(:).   53:- meta_predicate prob_inconsistent_theory(:).   54:- meta_predicate resume_query(:).   55:- meta_predicate compute_query_prob(:).   56:- meta_predicate axiom(:).   57:- meta_predicate kb_prefixes(:).   58:- meta_predicate add_kb_prefix(:,+).   59:- meta_predicate add_kb_prefixes(:).   60:- meta_predicate add_axiom(:).   61:- meta_predicate add_axioms(:).   62:- meta_predicate remove_kb_prefix(:,+).   63:- meta_predicate remove_kb_prefix(:).   64:- meta_predicate remove_axiom(:).   65:- meta_predicate remove_axioms(:).   66:- meta_predicate load_kb(+).   67:- meta_predicate load_owl_kb(+).   68:- meta_predicate load_owl_kb_from_string(+).   69:- meta_predicate set_algorithm(:).   70:- meta_predicate init_trill(+).   71:- meta_predicate set_tableau_expansion_rules(:,+).   72
   73:- use_module(library(lists)).   74:- use_module(library(ugraphs)).   75:- use_module(library(rbtrees)).   76:- use_module(library(dif)).   77:- use_module(library(pengines)).   78:- use_module(library(sandbox)).   79:- use_module(library(aggregate)).   80
   81:- reexport(library(bddem)).   82
   83:- style_check(-discontiguous).   84
   85%:- table ancestor1/4.
   86:- table blocked/2.   87
   88/********************************
   89  DISPONTE IRIS
   90*********************************/
   91
   92disponte_iri('http://sites.google.com/a/unife.it/ml/disponte#probability'). % Retro-compatibility
   93disponte_iri('https://sites.google.com/a/unife.it/ml/disponte#probability'). % Retro-compatibility
   94disponte_iri('http://ml.unife.it/disponte#probability'). % Retro-compatibility
   95disponte_iri('https://ml.unife.it/disponte#probability'). % Retro-compatibility
   96disponte_iri('http://ai.unife.it/disponte#probability').
   97disponte_iri('https://ai.unife.it/disponte#probability').
   98
   99/********************************
  100  SETTINGS
  101*********************************/
  102:- multifile setting_trill_default/2.  103
  104/********************************
  105  LOAD KNOWLEDGE BASE
  106*********************************/

 load_kb(++FileName:kb_file_name) is det

The predicate loads the knowledge base contained in the given file. The knowledge base must be defined in TRILL format, to use also OWL/RDF format use the predicate owl_rdf/1. /

  114load_kb(FileName):-
  115  user:consult(FileName).

 load_owl_kb(++FileName:kb_file_name) is det

The predicate loads the knowledge base contained in the given file. The knowledge base must be defined in pure OWL/RDF format. /

  123load_owl_kb(FileName):-
  124  load_owl(FileName).

 load_owl_kb_from_string(++KB:string) is det

The predicate loads the knowledge base contained in the given string. The knowledge base must be defined in pure OWL/RDF format. /

  132load_owl_kb_from_string(String):-
  133  load_owl_from_string(String).
  134
  135/*****************************/
  136
  137/*****************************
  138  UTILITY PREDICATES
  139******************************/
  140%defined in utility_translation
  141:- multifile add_kb_prefix/2, add_kb_prefixes/1, add_axiom/1, add_axioms/1,
  142             remove_kb_prefix/2, remove_kb_prefix/1, remove_axiom/1, remove_axioms/1.

 add_kb_prefix(:ShortPref:string, ++LongPref:string) is det

This predicate registers the alias ShortPref for the prefix defined in LongPref. The empty string '' can be defined as alias. /

 add_kb_prefixes(:Prefixes:list) is det

This predicate registers all the alias prefixes contained in Prefixes. The input list must contain pairs alias=prefix, i.e., [('foo'='http://example.foo#')]. The empty string '' can be defined as alias. /

 add_axiom(:Axiom:axiom) is det

This predicate adds the given axiom to the knowledge base. The axiom must be defined following the TRILL syntax. /

 add_axioms(:Axioms:list) is det

This predicate adds the axioms of the list to the knowledge base. The axioms must be defined following the TRILL syntax. /

 remove_kb_prefix(:ShortPref:string, ++LongPref:string) is det

This predicate removes from the registered aliases the one given in input. /

 remove_kb_prefix(:Name:string) is det

This predicate takes as input a string that can be an alias or a prefix and removes the pair containing the string from the registered aliases. /

 remove_axiom(:Axiom:axiom) is det

This predicate removes the given axiom from the knowledge base. The axiom must be defined following the TRILL syntax. /

 remove_axioms(++Axioms:list) is det

This predicate removes the axioms of the list from the knowledge base. The axioms must be defined following the TRILL syntax. /

 axiom(:Axiom:axiom) is det

This predicate searches in the loaded knowledge base axioms that unify with Axiom. /

  205:- multifile axiom/1.  206/*axiom(M:Axiom):-
  207  M:ns4query(NSList),
  208  expand_all_ns(M,[Axiom],NSList,[AxiomEx]),
  209  M:axiom(AxiomEx).*/
  210
  211:- multifile kb_prefixes/1.

 set_tableau_expansion_rules(:DetRules:list, ++NondetRules:list) is det

This predicate set the rules as taken in input, maintaining order and number of rules. DetRules is the list of deterministic rules, NondetRules the list of non-deterministic ones. /

  219set_tableau_expansion_rules(M:DetRules,NondetRules):-
  220  retractall(M:setting_trill(det_rules,_)),
  221  retractall(M:setting_trill(nondet_rules,_)),
  222  assert(M:setting_trill(det_rules,DetRules)),
  223  assert(M:setting_trill(nondet_rules,NondetRules)).
  224
  225/*****************************
  226  MESSAGES
  227******************************/
  228:- multifile prolog:message/1.  229
  230prolog:message(iri_not_exists(IRIs)) -->
  231  [ 'IRIs not existent or wrong argument: ~w' -[IRIs] ].
  232
  233prolog:message(inconsistent) -->
  234  [ 'Inconsistent ABox' ].
  235
  236prolog:message(consistent) -->
  237  [ 'Consistent ABox' ].
  238
  239prolog:message(wrong_number_max_expl) -->
  240  [ 'max_expl option can take integer values or "all"' ].
  241
  242prolog:message(timeout_reached) -->
  243  [ 'Timeout reached' ].
  244
  245prolog:message(unknown_query_option(Option)) -->
  246  [ 'Unknown query option: ~w' -[Option] ].
  247
  248/*****************************
  249  QUERY OPTIONS
  250******************************/

 query_option(+OptList:list, +Option:term, ?Value:term)

Check if the option defined by Option is in OptList and returns the option Value.

Options can be:

• assert_abox(Boolean) if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1.
• compute_prob(mode,Prob) if mode is query trill is forced to find all the explanations, and compute the probability of the query is computed and unified with Prob (same as using prob_<query> but it also returns the set of justifications); if mode is expl trill will compute the probability of each single explanation.
• max_expl(Value) to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanations.
• time_limit(Value) to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations.

*/

  264trill_available_option(assert_abox,in).
  265trill_available_option(compute_prob,in,out).
  266trill_available_option(max_expl,in).
  267trill_available_option(time_limit,in).
  268
  269get_from_query_options(OptList,Option,SingleValue):-
  270  trill_available_option(Option,_),!,
  271  Opt=..[Option,SingleValue],
  272  memberchk(Opt,OptList).
  273
  274get_from_query_options(OptList,Option,Value1,Value2):-
  275  trill_available_option(Option,_,_),
  276  Opt=..[Option,Value1,Value2],
  277  memberchk(Opt,OptList).
  278
  279
  280set_query_options(_,[]):- !.
  281
  282set_query_options(M,[QueryOption|TailQueryOptions]) :-
  283  QueryOption=..[Option|Value],
  284  add_trill_query_option(M,Option,Value),
  285  set_query_options(M,TailQueryOptions).
  286
  287add_trill_query_option(M,Option,[ValueIn]) :-
  288  trill_available_option(Option,in),!,
  289  retractall(M:query_option(Option,_)),
  290  assert(M:query_option(Option,ValueIn)).
  291
  292add_trill_query_option(M,Option,_ValueOut) :-
  293  trill_available_option(Option,out),!,
  294  retractall(M:query_option(Option,_)),
  295  assert(M:query_option(Option,true)).
  296
  297add_trill_query_option(M,Option,[ValueIn,_ValueOut]) :-
  298  trill_available_option(Option,in,out),!,
  299  retractall(M:query_option(Option,_)),
  300  assert(M:query_option(Option,ValueIn)).
  301
  302add_trill_query_option(_M,Option,_Value) :-
  303  print_message(warning,unknown_query_option(Option)),!.
  304
  305/****************************
  306  QUERY PREDICATES
  307*****************************/
  308
  309execute_query(M,QueryType,QueryArgsNC,Expl,QueryOptions):-
  310  check_query_args(M,QueryType,QueryArgsNC,QueryArgs),
  311  set_up_reasoner(M),
  312  set_query_options(M,QueryOptions),!,
  313  find_explanations(M,QueryType,QueryArgs,Expl),
  314  is_expl(M,Expl),
  315  compute_prob_and_close(M,Expl,QueryOptions).
  316
  317
  318% Execution monitor
  319find_explanations(M,QueryType,QueryArgs,Expl):-
  320  get_open_query_monitor(M,QueryType,QueryArgs),
  321  get_n_explanation_monitor(M,MonitorNExpl),
  322  get_time_limit_monitor(M,MonitorTimeLimit),
  323  find_n_explanations(M,QueryType,QueryArgs,Expl,MonitorNExpl),
  324  check_time_limit_monitor(M,MonitorTimeLimit).
  325
  326
  327find_single_explanation(M,QueryType,QueryArgs,Expl):-
  328  build_abox(M,Tableau,QueryType,QueryArgs), % will expand the KB without the query
  329  (absence_of_clashes(Tableau) ->  % TODO if QueryType is inconsistent no check
  330    (
  331      add_q(M,QueryType,Tableau,QueryArgs,Tableau0),
  332      set_up_tableau(M),
  333      set_next_from_expansion_queue(Tableau0,_EA,Tableau1),
  334      get_explanation(M,Tableau1,Expl)
  335    )
  336  ;
  337    print_message(warning,inconsistent),!,false
  338  ).
  339
  340/*************
  341 
  342  Monitor predicates
  343
  344**************/
  345
  346% Monitors
  347%  --- number of explanations ---
  348get_n_explanation_monitor(M,MonitorNExpl):-
  349  M:query_option(max_expl,MonitorNExpl),!. 
  350
  351get_n_explanation_monitor(M,all):-
  352  M:query_option(compute_prob,query),!.
  353
  354get_n_explanation_monitor(_M,bt):-!.
  355
  356
  357% --- time limit ---
  358get_time_limit_monitor(M,MonitorTimeLimit):-
  359  M:query_option(time_limit,TimeLimit),!,
  360  retractall(M:setting_trill(timeout,_)),
  361  get_time(Start),
  362  MonitorTimeLimit is Start + TimeLimit,
  363  assert(M:setting_trill(timeout,MonitorTimeLimit)).
  364
  365get_time_limit_monitor(_M,inf):-!.
  366
  367check_time_limit_monitor(_M,inf):-!. % forse no cut.
  368
  369check_time_limit_monitor(M,MonitorTimeLimit):-
  370  get_time(End),
  371  End < MonitorTimeLimit,!,
  372  retractall(M:query_option(time_limit,_)),
  373  NewTimeLimit is MonitorTimeLimit - End,
  374  assert(M:query_option(time_limit,NewTimeLimit)).
  375
  376check_time_limit_monitor(_M,_MonitorTimeLimit):-
  377  print_message(warning,timeout_reached),false.
  378
  379check_time_limit_monitor_status(M):-
  380  M:setting_trill(timeout,Timeout),!,
  381  get_time(Now),
  382  Timeout<Now. % I must stop
  383
  384% --- open query ---
  385get_open_query_monitor(M,QueryType,QueryArgs):-
  386  retractall(M:query_option(active_query,_)),
  387  assert(M:query_option(active_query,[QueryType,QueryArgs])).
  388
  389check_open_query_monitor_status(M,QueryType,QueryArgs):-
  390  M:query_option(active_query,[QueryType,QueryArgs]),!.
  391
  392check_open_query_monitor(M):-
  393  retractall(M:query_option(active_query,_)).
  394/* *************** */
  395
  396set_up_reasoner(M):-
  397  set_up(M),
  398  retractall(M:exp_found(_,_)),
  399  retractall(M:exp_found(_,_,_)),
  400  retractall(M:trillan_idx(_)),
  401  assert(M:trillan_idx(1)).
  402
  403set_up_tableau(M):-
  404  % TO CHANGE move to KB loading
  405  %setting_trill_default(det_rules,DetRules),
  406  %setting_trill_default(nondet_rules,NondetRules),
  407  %set_tableau_expansion_rules(M:DetRules,NondetRules). 
  408  prune_tableau_rules(M).
  409
  410% instanceOf
  411add_q(M,io,Tableau0,[ClassEx,IndEx],Tableau):- !,
  412  neg_class(ClassEx,NClassEx),
  413  add_q(M,Tableau0,classAssertion(NClassEx,IndEx),Tableau1),
  414  add_clash_to_tableau(M,Tableau1,NClassEx-IndEx,Tableau2),
  415  update_expansion_queue_in_tableau(M,NClassEx,IndEx,Tableau2,Tableau).
  416
  417% property_value
  418add_q(M,pv,Tableau0,[PropEx,Ind1Ex,Ind2Ex],Tableau):-!,
  419  neg_class(PropEx,NPropEx), %use of neg_class to negate property
  420  add_q(M,Tableau0,propertyAssertion(NPropEx,Ind1Ex,Ind2Ex),Tableau1),
  421  add_clash_to_tableau(M,Tableau1,NPropEx-Ind1Ex-Ind2Ex,Tableau2),
  422  update_expansion_queue_in_tableau(M,NPropEx,Ind1Ex,Ind2Ex,Tableau2,Tableau).
  423
  424
  425% sub_class
  426add_q(M,sc,Tableau0,[SubClassEx,SupClassEx],Tableau):- !,
  427  neg_class(SupClassEx,NSupClassEx),
  428  query_ind(QInd),
  429  add_q(M,Tableau0,classAssertion(intersectionOf([SubClassEx,NSupClassEx]),QInd),Tableau1),
  430  utility_translation:add_kb_atoms(M,class,[intersectionOf([SubClassEx,NSupClassEx])]), % This is necessary to correctly prune expansion rules
  431  add_owlThing_ind(M,Tableau1,QInd,Tableau2),
  432  add_clash_to_tableau(M,Tableau2,intersectionOf([SubClassEx,NSupClassEx])-QInd,Tableau3),
  433  update_expansion_queue_in_tableau(M,intersectionOf([SubClassEx,NSupClassEx]),QInd,Tableau3,Tableau).
  434
  435% unsat
  436add_q(M,un,Tableau0,['unsat',ClassEx],Tableau):- !,
  437  query_ind(QInd),
  438  add_q(M,Tableau0,classAssertion(ClassEx,QInd),Tableau1),
  439  add_owlThing_ind(M,Tableau1,QInd,Tableau2),
  440  add_clash_to_tableau(M,Tableau2,ClassEx-QInd,Tableau3),
  441  update_expansion_queue_in_tableau(M,ClassEx,QInd,Tableau3,Tableau).
  442
  443% inconsistent_theory
  444add_q(_,it,Tableau,['inconsistent','kb'],Tableau):- !. % Do nothing
  445
  446/*
  447  Auxiliary predicates to extract the det of individuals connected to the query
  448*/
  449
  450% Find the individuals directly connected to the given one
  451gather_connected_individuals(M,Ind,ConnectedInds):-
  452  find_successors(M,Ind,SuccInds),
  453  find_predecessors(M,Ind,PredInds),
  454  append(SuccInds,PredInds,ConnectedInds).
  455
  456find_successors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,Ind,ConnectedInd)), List).
  457find_predecessors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,ConnectedInd,Ind)), List).
  458
  459intersect([H|_], List) :- member(H, List), !.
  460intersect([_|T], List) :- intersect(T, List).
  461
  462% Recursively gather all the connected individuals, i.e., isolate the relevant fragment of the KB.
  463%scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet).
  464scan_connected_individuals(_,[],_,IndividualsSet0,IndividualsSet):-
  465  sort(IndividualsSet0,IndividualsSet).
  466
  467scan_connected_individuals(M,[H|IndividualsToCheck],IndividualsChecked,IndividualsSet0,IndividualsSet):-
  468  memberchk(H,IndividualsChecked),!,
  469  scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet).
  470
  471
  472scan_connected_individuals(M,[H|IndividualsToCheck0],IndividualsChecked,IndividualsSet0,IndividualsSet):-
  473  gather_connected_individuals(M,H,NewIndividualsToCheck),
  474  append(IndividualsSet0,NewIndividualsToCheck,IndividualsSet1),
  475  append(IndividualsToCheck0,NewIndividualsToCheck,IndividualsToCheck),
  476  scan_connected_individuals(M,IndividualsToCheck,[H|IndividualsChecked],IndividualsSet1,IndividualsSet).
  477
  478
  479% Builds the list of individuals conneted given the query type
  480collect_individuals(M,io,[_,IndEx],IndividualsSet):-
  481  scan_connected_individuals(M,[IndEx],[],[IndEx],IndividualsSet).
  482
  483collect_individuals(M,pv,[_,Ind1Ex,Ind2Ex],IndividualsSet):-
  484  scan_connected_individuals(M,[Ind1Ex,Ind2Ex],[],[Ind1Ex,Ind2Ex],IndividualsSet).
  485
  486collect_individuals(_,sc,[_,_],[QInd]):- % It is not necessary to check the KB as the individual of the query is a new fresh individual not included in the KB.
  487  query_ind(QInd).
  488
  489collect_individuals(_,un,['unsat',_],[QInd]):- % It is not necessary to check the KB as the individual of the query is a new fresh individual not included in the KB.
  490  query_ind(QInd).
  491
  492collect_individuals(_,it,['inconsistent','kb'],[]):-!.
  493
  494/*
  495  check the KB atoms to consider only the necessary expansion rules, pruning the useless ones
  496*/
  497prune_tableau_rules(M):-
  498  M:kb_atom(KBA),
  499  Classes=KBA.class,
  500  setting_trill_default(det_rules,DetRules),
  501  prune_tableau_rules(Classes,DetRules,PrunedDetRules),
  502  setting_trill_default(nondet_rules,NondetRules),
  503  prune_tableau_rules(Classes,NondetRules,PrunedNondetRules),
  504  set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules).
  505
  506add_tableau_rules_from_class(M,someValuesFrom(_,_)):-
  507  M:setting_trill(det_rules,Rules),
  508  memberchk(exists_rule,Rules),!.
  509
  510add_tableau_rules_from_class(M,C):-
  511  M:kb_atom(KBA),
  512  Classes=KBA.class,
  513  setting_trill_default(det_rules,DetRules),
  514  prune_tableau_rules([C|Classes],DetRules,PrunedDetRules),
  515  setting_trill_default(nondet_rules,NondetRules),
  516  prune_tableau_rules([C|Classes],NondetRules,PrunedNondetRules),
  517  set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules).
  518
  519% o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule,or_rule,max_rule,ch_rule
  520prune_tableau_rules(_,[],[]).
  521
  522prune_tableau_rules(KBA,[o_rule|TR],[o_rule|PTR]):-
  523  memberchk(oneOf(_),KBA),!,
  524  prune_tableau_rules(KBA,TR,PTR).
  525
  526prune_tableau_rules(KBA,[and_rule|TR],[and_rule|PTR]):-
  527  memberchk(intersectionOf(_),KBA),!,
  528  prune_tableau_rules(KBA,TR,PTR).
  529
  530prune_tableau_rules(KBA,[unfold_rule|TR],[unfold_rule|PTR]):-
  531  !,
  532  prune_tableau_rules(KBA,TR,PTR).
  533
  534prune_tableau_rules(KBA,[add_exists_rule|TR],[add_exists_rule|PTR]):-
  535  !,
  536  prune_tableau_rules(KBA,TR,PTR).
  537
  538prune_tableau_rules(KBA,[forall_rule|TR],[forall_rule|PTR]):-
  539  memberchk(allValuesFrom(_,_),KBA),!,
  540  prune_tableau_rules(KBA,TR,PTR).
  541
  542prune_tableau_rules(KBA,[forall_plus_rule|TR],[forall_plus_rule|PTR]):-
  543  memberchk(allValuesFrom(_,_),KBA),!,
  544  prune_tableau_rules(KBA,TR,PTR).
  545
  546prune_tableau_rules(KBA,[exists_rule|TR],[exists_rule|PTR]):-
  547  memberchk(someValuesFrom(_,_),KBA),!,
  548  prune_tableau_rules(KBA,TR,PTR).
  549
  550prune_tableau_rules(KBA,[min_rule|TR],[min_rule|PTR]):-
  551  (memberchk(minCardinality(_,_),KBA); memberchk(minCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  552  prune_tableau_rules(KBA,TR,PTR).
  553
  554prune_tableau_rules(KBA,[or_rule|TR],[or_rule|PTR]):-
  555  memberchk(unionOf(_),KBA),!,
  556  prune_tableau_rules(KBA,TR,PTR).
  557
  558prune_tableau_rules(KBA,[max_rule|TR],[max_rule|PTR]):-
  559  (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  560  prune_tableau_rules(KBA,TR,PTR).
  561
  562
  563prune_tableau_rules(KBA,[ch_rule|TR],[ch_rule|PTR]):-
  564  (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  565  prune_tableau_rules(KBA,TR,PTR).
  566
  567prune_tableau_rules(KBA,[_|TR],PTR):-
  568  prune_tableau_rules(KBA,TR,PTR).
  569
  570/***********
  571  Queries
  572  - with and without explanations -
  573 ***********/

 instanceOf(:Class:concept_description, ++Ind:individual_name, -Expl:list, -Expl:list, ++Opt:list)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and name or the full URI of an individual and returns one explanation for the instantiation of the individual to the given class. The returning explanation is a set of axioms. The predicate fails if the individual does not belong to the class. Opt is a list containing settings for the execution of the query. */

  584instanceOf(M:Class,Ind,Expl,Opt):-
  585  execute_query(M,io,[Class,Ind],Expl,Opt).

 instanceOf(:Class:concept_description, ++Ind:individual_name)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and name or the full URI of an individual and returns one explanation for the instantiation of the individual to the given class. The returning explanation is a set of axioms. The predicate fails if the individual does not belong to the class. /

  597instanceOf(M:Class,Ind,Expl):-
  598  instanceOf(M:Class,Ind,Expl,[]).

 all_instanceOf(:Class:concept_description, ++Ind:individual_name)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and name or the full URI of an individual and returns all the explanations for the instantiation of the individual to the given class. The returning explanations are in the form if a list (set) of set of axioms. The predicate fails if the individual does not belong to the class. /

  609all_instanceOf(M:Class,Ind,Expl):-
  610  execute_query(M,io,[Class,Ind],Expl,[max_expl(all)]).

 instanceOf(:Class:concept_description, ++Ind:individual_name) is det

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and name or the full URI of an individual and returns true if the individual belongs to the class, false otherwise. /

  619instanceOf(M:Class,Ind):-
  620  execute_query(M,io,[Class,Ind],_,[max_expl(1)]),!.

 property_value(:Prop:property_name, ++Ind1:individual_name, ++Ind2:individual_name, -Expl:list, ++Opt:list)

This predicate takes as input the name or the full URI of a property and of two individuals and returns one explanation for the fact Ind1 is related with Ind2 via Prop. The returning explanation is a set of axioms. The predicate fails if the two individual are not Prop-related. * Opt is a list containing options for the execution of the query. Options can be:

• assert_abox(Boolean) if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1.
• compute_prob(mode,Prob) if mode is query trill is forced to find all the explanations, and compute the probability of the query is computed and unified with Prob (same as using prob_<query> but it also returns the set of justifications); if mode is expl trill will compute the probability of each single explanation.
• max_expl(Value) to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanations.
• time_limit(Value) to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations.

/

  636property_value(M:Prop, Ind1, Ind2,Expl,Opt):-
  637  execute_query(M,pv,[Prop, Ind1, Ind2],Expl,Opt).

 property_value(:Prop:property_name, ++Ind1:individual_name, ++Ind2:individual_name, -Expl:list)

This predicate takes as input the name or the full URI of a property and of two individuals and returns one explanation for the fact Ind1 is related with Ind2 via Prop. The returning explanation is a set of axioms. The predicate fails if the two individual are not Prop-related. /

  647property_value(M:Prop, Ind1, Ind2,Expl):-
  648  property_value(M:Prop, Ind1, Ind2,Expl,[]).

 all_property_value(:Prop:property_name, ++Ind1:individual_name, ++Ind2:individual_name, -Expl:list)

This predicate takes as input the name or the full URI of a property and of two individuals and returns all the explanations for the fact Ind1 is related with Ind2 via Prop. The returning explanations are in the form if a list (set) of set of axioms. The predicate fails if the individual does not belong to the class. /

  658all_property_value(M:Prop, Ind1, Ind2,Expl):-
  659  execute_query(M,pv,[Prop, Ind1, Ind2],Expl,[max_expl(all)]).

 property_value(:Prop:property_name, ++Ind1:individual_name, ++Ind2:individual_name) is det

This predicate takes as input the name or the full URI of a property and of two individuals and returns true if the two individual are Prop-related, false otherwise. /

  667property_value(M:Prop, Ind1, Ind2):-
  668  execute_query(M,pv,[Prop, Ind1, Ind2],_,[max_expl(1)]),!.

 sub_class(:Class:concept_description, ++SupClass:concept_description, -Expl:list, ++Opt:list)

This predicate takes as input two concepts which can be given by the name or the full URI of two a simple concept or the definition of a complex concept as a ground term and returns one explanation for the subclass relation between Class and SupClass. The returning explanation is a set of axioms. The predicate fails if there is not a subclass relation between the two classes. Opt is a list containing options for the execution of the query. Options can be:

• assert_abox(Boolean) if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1.
• compute_prob(mode,Prob) if mode is query trill is forced to find all the explanations, and compute the probability of the query is computed and unified with Prob (same as using prob_<query> but it also returns the set of justifications); if mode is expl trill will compute the probability of each single explanation.
• max_expl(Value) to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanations.
• time_limit(Value) to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations.

/

  685sub_class(M:Class,SupClass,Expl,Opt):-
  686  execute_query(M,sc,[Class,SupClass],Expl,Opt).

 sub_class(:Class:concept_description, ++SupClass:concept_description, -Expl:list)

This predicate takes as input two concepts which can be given by the name or the full URI of two a simple concept or the definition of a complex concept as a ground term and returns one explanation for the subclass relation between Class and SupClass. The returning explanation is a set of axioms. The predicate fails if there is not a subclass relation between the two classes. /

  697sub_class(M:Class,SupClass,Expl):-
  698  sub_class(M:Class,SupClass,Expl,[]).

 all_sub_class(:Class:concept_description, ++SupClass:concept_description, -Expl:list)

This predicate takes as input two concepts which can be given by the name or the full URI of two a simple concept or the definition of a complex concept as a ground term and returns all the explanations for the subclass relation between Class and SupClass. The returning explanations are in the form if a list (set) of set of axioms. The predicate fails if Class is not subclass of SupClass. /

  709all_sub_class(M:Class,SupClass,Expl):-
  710  execute_query(M,sc,[Class,SupClass],Expl,[max_expl(all)]).

 sub_class(:Class:concept_description, ++SupClass:concept_description) is det

This predicate takes as input two concepts which can be given by the name or the full URI of two a simple concept or the definition of a complex concept as a ground term and returns true if Class is a subclass of SupClass, and false otherwise. /

  718sub_class(M:Class,SupClass):-
  719  execute_query(M,sc,[Class,SupClass],_,[max_expl(1)]),!.

 unsat(:Concept:concept_description, -Expl:list, ++Opt:list)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and returns one explanation for the unsatisfiability of the concept. The returning explanation is a set of axioms. The predicate fails if the concept is satisfiable. Opt is a list containing options for the execution of the query. Options can be:

• assert_abox(Boolean) if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1.
• compute_prob(mode,Prob) if mode is query trill is forced to find all the explanations, and compute the probability of the query is computed and unified with Prob (same as using prob_<query> but it also returns the set of justifications); if mode is expl trill will compute the probability of each single explanation.
• max_expl(Value) to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanations.
• time_limit(Value) to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations.

/

  735unsat(M:Concept,Expl,Opt):-
  736  execute_query(M,un,[Concept],Expl,Opt).

 unsat(:Concept:concept_description, -Expl:list)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and returns one explanation for the unsatisfiability of the concept. The returning explanation is a set of axioms. The predicate fails if the concept is satisfiable. /

  746unsat(M:Concept,Expl):-
  747  unsat(M:Concept,Expl,[]).

 all_unsat(:Concept:concept_description, -Expl:list)

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and returns all the explanations for the unsatisfiability of the concept. The returning explanations are in the form if a list (set) of set of axioms. The predicate fails if the individual does not belong to the class. /

  757all_unsat(M:Concept,Expl):-
  758  execute_query(M,un,[Concept],Expl,[max_expl(all)]).

 unsat(:Concept:concept_description) is det

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and returns true if the concept is unsatisfiable, false otherwise. /

  766unsat(M:Concept):-
  767  execute_query(M,un,[Concept],_,[max_expl(1)]),!.

 inconsistent_theory(:Expl:list, ++Opt:list)

This predicate returns one explanation for the inconsistency of the loaded knowledge base. Opt is a list containing options for the execution of the query. Options can be:

• assert_abox(Boolean) if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1.
• compute_prob(mode,Prob) if mode is query trill is forced to find all the explanations, and compute the probability of the query is computed and unified with Prob (same as using prob_<query> but it also returns the set of justifications); if mode is expl trill will compute the probability of each single explanation.
• max_expl(Value) to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanations.
• time_limit(Value) to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations.

/

  780inconsistent_theory(M:Expl,Opt):-
  781  execute_query(M,it,[],Expl,Opt).

 inconsistent_theory(:Expl:list)

This predicate returns one explanation for the inconsistency of the loaded knowledge base. /

  788inconsistent_theory(M:Expl):-
  789  inconsistent_theory(M:Expl,[]).

 all_inconsistent_theory(:Expl:list)

This predicate returns all the explanations for the inconsistency of the loaded knowledge base. The returning explanations are in the form if a list (set) of set of axioms. The predicate fails if the individual does not belong to the class. /

  798all_inconsistent_theory(M:Expl):-
  799  execute_query(M,it,[],Expl,[max_expl(all)]).

 inconsistent_theory

This predicate returns true if the loaded knowledge base is inconsistent, otherwise it fails. /

  806inconsistent_theory:-
  807  get_trill_current_module(M),
  808  execute_query(M,it,[],_,[max_expl(1)]),!.

 prob_instanceOf(:Class:concept_description, ++Ind:individual_name, --Prob:double) is det

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and name or the full URI of an individual and returns the probability of the instantiation of the individual to the given class. /

  817prob_instanceOf(M:Class,Ind,Prob):-
  818  instanceOf(M:Class,Ind,_,[compute_prob(query,Prob)]).

 prob_property_value(:Prop:property_name, ++Ind1:individual_name, ++Ind2:individual_name, --Prob:double) is det

This predicate takes as input the name or the full URI of a property and of two individuals and returns the probability of the fact Ind1 is related with Ind2 via Prop. /

  826prob_property_value(M:Prop, Ind1, Ind2,Prob):-
  827  property_value(M:Prop, Ind1, Ind2,_,[compute_prob(query,Prob)]).

 prob_sub_class(:Class:concept_description, ++SupClass:class_name, --Prob:double) is det

This predicate takes as input two concepts which can be given by the name or the full URI of two a simple concept or the definition of a complex concept as a ground term and returns the probability of the subclass relation between Class and SupClass. /

  836prob_sub_class(M:Class,SupClass,Prob):-
  837  sub_class(M:Class,SupClass,_,[compute_prob(query,Prob)]).

 prob_unsat(:Concept:concept_description, --Prob:double) is det

This predicate takes as input the name or the full URI of a class or the definition of a complex concept as a ground term and returns the probability of the unsatisfiability of the concept. /

  846prob_unsat(M:Concept,Prob):-
  847  unsat(M:Concept,_,[compute_prob(query,Prob)]).

 prob_inconsistent_theory(:Prob:double) is det

If the knowledge base is inconsistent, this predicate returns the probability of the inconsistency. /

  854prob_inconsistent_theory(M:Prob):-
  855  inconsistent_theory(M:_,[compute_prob(query,Prob)]).

 resume_query(:Expl:list) is det

Continues with the search for new justifications for the previous query if a previous query is open. It only works returning justifications one by one. /

  863resume_query(M:Expl):-
  864  check_open_query_monitor_status(M,_,_),
  865  M:tab_end(Tab),
  866  retract(M:tab_end(Tab)),
  867  set_up_tableau(M),
  868  check_and_set_next_from_expansion_queue(Tab,_EA,Tab1),
  869  get_explanation(M,Tab1,Expl).

 compute_query_prob(:Prob:double) is det

Computes the probability of the previous query if there is one open. /

  876compute_query_prob(M:Prob) :-
  877  check_open_query_monitor_status(M,_,_),
  878  findall(Exp,M:exp_found(qp,Exp),Exps),
  879  compute_prob(M,Exps,Prob),!.

 reset_query is det

Closes the open query and reset the reasoner status to prepare it for a new query. /

  886reset_query:-
  887  get_trill_current_module(M),
  888  set_up_reasoner(M).
  889
  890
  891
  892/***********
  893  Utilities for queries
  894 ***********/
  895
  896% adds the query into the ABox
  897add_q(M,Tableau0,Query,Tableau):-
  898  query_empty_expl(M,Expl),
  899  add_to_tableau(Tableau0,(Query,Expl),Tableau1),
  900  create_tabs([(Query,Expl)],Tableau1,Tableau).
  901
  902
  903% initialize an empty explanation for the query with the query placeholder 'qp' in teh choicepoint list
  904query_empty_expl(M,Expl):-%gtrace,
  905  empty_expl(M,EExpl),
  906  add_choice_point(M,qp,EExpl,Expl).
  907
  908
  909% expands query arguments using prefixes and checks their existence in the kb
  910% returns the non-present arguments
  911check_query_args(M,QT,QA,QAEx):-
  912  from_query_type_to_args_type(QT,AT),
  913  check_query_args_1(M,AT,QA,QAExT,NotEx),!,
  914  check_query_not_existent_args(QA,QAExT,NotEx,QAEx),!.
  915
  916check_query_not_existent_args(QA,QAExT,[],QAEx) :- !,
  917  ( length(QA,1) -> 
  918    QAEx = ['unsat'|QAExT]
  919    ;
  920    ( length(QA,0) -> QAEx = ['inconsistent','kb'] ; QAEx = QAExT)
  921  ).
  922check_query_not_existent_args(_QA,_QAExT,NotEx,_QAEx) :-
  923  print_message(warning,iri_not_exists(NotEx)),!.
  924
  925from_query_type_to_args_type(io,[class,ind]):- !.
  926from_query_type_to_args_type(pv,[prop,ind,ind]):- !.
  927from_query_type_to_args_type(sc,[class,class]):- !.
  928from_query_type_to_args_type(un,[class]):- !.
  929from_query_type_to_args_type(it,[]):- !.
  930
  931check_query_args_1(_,_,[],[],[]).
  932
  933check_query_args_1(M,[ATH|ATT],[H|T],[HEx|TEx],NotEx):-
  934  check_query_args_2(M,[ATH],[H],[HEx]),!,
  935  check_query_args_1(M,ATT,T,TEx,NotEx).
  936
  937check_query_args_1(M,[_|ATT],[H|T],TEx,[H|NotEx]):-
  938  check_query_args_1(M,ATT,T,TEx,NotEx).
  939
  940% expands query arguments using prefixes and checks their existence in the kb
  941check_query_args_2(M,AT,L,LEx) :-
  942  M:ns4query(NSList),
  943  expand_all_ns(M,L,NSList,false,LEx), %from utility_translation module
  944  check_query_args_presence(M,AT,LEx).
  945
  946check_query_args_presence(_M,_AT,[]):-!.
  947
  948check_query_args_presence(M,[class|ATT],['http://www.w3.org/2002/07/owl#Thing'|T]) :-
  949  check_query_args_presence(M,ATT,T).
  950
  951check_query_args_presence(M,[AT|ATT],[H|T]) :-
  952  nonvar(H),
  953  atomic(H),!,
  954  find_atom_in_axioms(M,AT,H),%!,
  955  check_query_args_presence(M,ATT,T).
  956
  957check_query_args_presence(M,[AT|ATT],[H|T]) :-
  958  nonvar(H),
  959  \+ atomic(H),!,
  960  H =.. [CE|L],
  961  flatten(L,L1),
  962  from_expression_to_args_type(CE,AT,L1,ATs),
  963  check_query_args_presence(M,ATs,L1),
  964  check_query_args_presence(M,ATT,T).
  965
  966/*
  967check_query_args_presence(M,[_|T]):-
  968  check_query_args_presence(M,T).
  969*/
  970
  971% looks for presence of atoms in kb's axioms
  972find_atom_in_axioms(M,class,H):-
  973  M:kb_atom(L1),
  974  ( member(H,L1.class) ),!.
  975
  976find_atom_in_axioms(M,ind,H):-
  977  M:kb_atom(L1),
  978  ( member(H,L1.individual) ; member(H,L1.datatype) ),!.
  979
  980find_atom_in_axioms(M,prop,H):-
  981  M:kb_atom(L1),
  982  ( member(H,L1.objectProperty) ; member(H,L1.dataProperty) ; member(H,L1.annotationProperty) ),!.
  983
  984find_atom_in_axioms(_,num,H):-
  985  integer(H),!.
  986
  987from_expression_to_args_type(complementOf,class,_,[class]) :- !.
  988from_expression_to_args_type(someValuesFrom,class,_,[prop,class]) :- !.
  989from_expression_to_args_type(allValuesFrom,class,_,[prop,class]) :- !.
  990from_expression_to_args_type(hasValue,class,_,[prop,ind]) :- !.
  991from_expression_to_args_type(hasSelf,class,_,[prop]) :- !.
  992from_expression_to_args_type(minCardinality,class,[_,_,_],[num,prop,class]) :- !.
  993from_expression_to_args_type(minCardinality,class,[_,_],[num,prop]) :- !.
  994from_expression_to_args_type(maxCardinality,class,[_,_,_],[num,prop,class]) :- !.
  995from_expression_to_args_type(maxCardinality,class,[_,_],[num,prop]) :- !.
  996from_expression_to_args_type(exactCardinality,class,[_,_,_],[num,prop,class]) :- !.
  997from_expression_to_args_type(exactCardinality,class,[_,_],[num,prop]) :- !.
  998from_expression_to_args_type(inverseOf,prop,_,[prop]) :- !.
  999from_expression_to_args_type(ExprList,AT,L1,ATs):-
 1000  is_expr_list(ExprList,AT,ListType),!,
 1001  create_list(ListType,L1,ATs).
 1002
 1003
 1004is_expr_list(intersectionOf,class,class).
 1005is_expr_list(unionOf,class,class).
 1006is_expr_list(oneOf,class,ind).
 1007is_expr_list(propertyChain,prop,prop).
 1008
 1009create_list([],_,[]).
 1010
 1011create_list([_|T],AT,[AT|ATT]):-
 1012  create_list(T,AT,ATT).
 1013
 1014
 1015
 1016
 1017
 1018
 1019
 1020/****************************/
 1021
 1022/**************
 1023  FIND FUNCTIONS
 1024***************/
 1025
 1026findClassAssertion(C,Ind,Expl1,ABox):-
 1027  (
 1028    is_list(Ind) ->
 1029    (
 1030      find((classAssertion(C,sameIndividual(Ind)),Expl1),ABox)
 1031    ) ;
 1032    (
 1033      find((classAssertion(C,Ind),Expl1),ABox)
 1034    )
 1035  ).
 1036
 1037findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox):-
 1038	(
 1039    is_list(Ind1) ->
 1040    (
 1041      Ind1S=sameIndividual(Ind1)
 1042    ) ;
 1043    (
 1044      Ind1S=Ind1
 1045    )
 1046  ),
 1047  (
 1048    is_list(Ind2) ->
 1049    (
 1050      Ind2S=sameIndividual(Ind2)
 1051    ) ;
 1052    (
 1053      Ind2S=Ind2
 1054    )
 1055  ),
 1056  find((propertyAssertion(R,Ind1S,Ind2S),Expl1),ABox).
 1057
 1058
 1059/****************************
 1060  TABLEAU ALGORITHM
 1061****************************/
 1062
 1063/*
 1064find_clash(M,(ABox0,Tabs0),Expl2):-
 1065  apply_rules((ABox0,Tabs0),(ABox,Tabs)),
 1066  clash(M,(ABox,Tabs),Expl).
 1067*/
 1068
 1069%-------------
 1070% clash managing
 1071% previous version, manages only one clash at time
 1072% need some tricks in some rules for managing the cases of more than one clash
 1073% TO IMPROVE!
 1074%------------
 1075:- multifile clash/4. 1076
 1077clash(M,owlnothing,Tab,Expl):-
 1078  get_abox(Tab,ABox),
 1079  %write('clash 6'),nl,
 1080  findClassAssertion4OWLNothing(M,ABox,Expl).
 1081
 1082clash(M,C-Ind,Tab,Expl):-
 1083  get_abox(Tab,ABox),
 1084  %write('clash 1'),nl,
 1085  findClassAssertion(C,Ind,Expl1,ABox),
 1086  neg_class(C,NegC),
 1087  findClassAssertion(NegC,Ind,Expl2,ABox),
 1088  and_f(M,Expl1,Expl2,Expl).
 1089
 1090clash(M,sameIndividual(LS),Tab,Expl):-
 1091  get_abox(Tab,ABox),
 1092  %write('clash 2.a'),nl,
 1093  findSameIndividual(LS,(sameIndividual(LSABox),Expl1),ABox),
 1094  find((differentIndividuals(LD),Expl2),ABox),
 1095  member(X,LSABox),
 1096  member(Y,LSABox),
 1097  member(X,LD),
 1098  member(Y,LD),
 1099  dif(X,Y),
 1100  and_f(M,Expl1,Expl2,Expl).
 1101
 1102clash(M,differentIndividuals(LS),Tab,Expl):-
 1103  get_abox(Tab,ABox),
 1104  %write('clash 2.b'),nl,
 1105  findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl1),ABox),
 1106  find((sameIndividual(LD),Expl2),ABox),
 1107  member(X,LSABox),
 1108  member(Y,LSABox),
 1109  member(X,LD),
 1110  member(Y,LD),
 1111  dif(X,Y),
 1112  and_f(M,Expl1,Expl2,Expl).
 1113
 1114clash(M,C-sameIndividual(L1),Tab,Expl):-
 1115  get_abox(Tab,ABox),
 1116  %write('clash 3'),nl,
 1117  findClassAssertion(C,sameIndividual(L1),Expl1,ABox),
 1118  neg_class(C,NegC),
 1119  findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox),
 1120  samemember(L1,L2),!,
 1121  and_f(M,Expl1,Expl2,Expl).
 1122
 1123samemember(L1,L2):-
 1124  member(X,L1),
 1125  member(X,L2),!.
 1126
 1127clash(M,C-Ind1,Tab,Expl):-
 1128  get_abox(Tab,ABox),
 1129  %write('clash 4'),nl,
 1130  findClassAssertion(C,Ind1,Expl1,ABox),
 1131  neg_class(C,NegC),
 1132  findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox),
 1133  member(Ind1,L2),
 1134  and_f(M,Expl1,Expl2,Expl).
 1135
 1136clash(M,C-sameIndividual(L1),Tab,Expl):-
 1137  get_abox(Tab,ABox),
 1138  %write('clash 5'),nl,
 1139  findClassAssertion(C,sameIndividual(L1),Expl1,ABox),
 1140  neg_class(C,NegC),
 1141  findClassAssertion(NegC,Ind2,Expl2,ABox),
 1142  member(Ind2,L1),
 1143  and_f(M,Expl1,Expl2,Expl).
 1144
 1145clash(M,C1-Ind,Tab,Expl):-
 1146  get_abox(Tab,ABox),
 1147  %write('clash 7'),nl,
 1148  M:disjointClasses(L), % TODO use hierarchy
 1149  member(C1,L),
 1150  member(C2,L),
 1151  dif(C1,C2),
 1152  findClassAssertion(C1,Ind,Expl1,ABox),
 1153  findClassAssertion(C2,Ind,Expl2,ABox),
 1154  and_f(M,Expl1,Expl2,ExplT),
 1155  and_f_ax(M,disjointClasses(L),ExplT,Expl).
 1156
 1157clash(M,C1-Ind,Tab,Expl):-
 1158  get_abox(Tab,ABox),
 1159  %write('clash 8'),nl,
 1160  M:disjointUnion(Class,L), % TODO use hierarchy
 1161  member(C1,L),
 1162  member(C2,L),
 1163  dif(C1,C2),
 1164  findClassAssertion(C1,Ind,Expl1,ABox),
 1165  findClassAssertion(C2,Ind,Expl2,ABox),
 1166  and_f(M,Expl1,Expl2,ExplT),
 1167  and_f_ax(M,disjointUnion(Class,L),ExplT,Expl).
 1168
 1169clash(M,P-Ind1-Ind2,Tab,Expl):-
 1170  get_abox(Tab,ABox),
 1171  %write('clash 11'),nl,
 1172  findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox),
 1173  neg_class(P,NegP), % use of neg_class with a property
 1174  findPropertyAssertion(NegP,Ind1,Ind2,Expl2,ABox),
 1175  and_f(M,Expl1,Expl2,Expl).
 1176
 1177
 1178/*
 1179clash(M,Tab,Expl):-
 1180  %write('clash 9'),nl,
 1181  findClassAssertion(maxCardinality(N,S,C),Ind,Expl1,ABox),
 1182  s_neighbours(M,Ind,S,Tab,SN),
 1183  get_abox(Tab,ABox),
 1184  individual_class_C(SN,C,ABox,SNC),
 1185  length(SNC,LSS),
 1186  LSS @> N,
 1187  make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
 1188
 1189clash(M,Tab,Expl):-
 1190  %write('clash 10'),nl,
 1191  findClassAssertion(maxCardinality(N,S),Ind,Expl1,ABox),
 1192  s_neighbours(M,Ind,S,Tab,SN),
 1193  length(SN,LSS),
 1194  LSS @> N,
 1195  make_expl(Ind,S,SN,Expl1,ABox,Expl).
 1196
 1197
 1198% --------------
 1199
 1200make_expl(_,_,_,[],Expl,_,Expl).
 1201
 1202make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):-
 1203  findPropertyAssertion(S,Ind,H,Expl2,ABox),
 1204  and_f(M,Expl2,Expl0,Expl1),
 1205  make_expl(M,Ind,S,T,Expl1,ABox,Expl).
 1206*/
 1207
 1208findSameIndividual(LS,(sameIndividual(LSABox),Expl),ABox):-
 1209  find((sameIndividual(LSABox),Expl),ABox),
 1210  all_members(LS,LSABox).
 1211
 1212findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl),ABox):-
 1213  find((differentIndividuals(LSABox),Expl),ABox),
 1214  all_members(LS,LSABox).
 1215
 1216all_members(LS,LSABox):-
 1217  member(H1,LS),
 1218  member(H2,LS),
 1219  dif(H1,H2),
 1220  member(H1,LSABox),
 1221  member(H2,LSABox),!.
 1222
 1223
 1224
 1225:- multifile check_clash/3. 1226
 1227check_clash(_,'http://www.w3.org/2002/07/owl#Nothing'-_,_):-
 1228  %write('clash 6'),nl,
 1229  !.
 1230
 1231check_clash(_,C-Ind,Tab):-
 1232  get_abox(Tab,ABox),
 1233  %write('clash 1'),nl,
 1234  neg_class(C,NegC),
 1235  findClassAssertion(NegC,Ind,_,ABox),!.
 1236  
 1237check_clash(_,sameIndividual(LS),Tab):-
 1238  get_abox(Tab,ABox),
 1239  %write('clash 2.a'),nl,
 1240  find((differentIndividuals(LD),_Expl2),ABox),
 1241  member(X,LS),
 1242  member(Y,LS),
 1243  member(X,LD),
 1244  member(Y,LD),
 1245  dif(X,Y),!.
 1246  
 1247check_clash(_,differentIndividuals(LS),Tab):-
 1248  get_abox(Tab,ABox),
 1249  %write('clash 2.b'),nl,
 1250  find((sameIndividual(LD),_Expl2),ABox),
 1251  member(X,LS),
 1252  member(Y,LS),
 1253  member(X,LD),
 1254  member(Y,LD),
 1255  dif(X,Y),!.
 1256  
 1257check_clash(_,C-sameIndividual(L1),Tab):-
 1258  get_abox(Tab,ABox),
 1259  %write('clash 3'),nl,
 1260  neg_class(C,NegC),
 1261  findClassAssertion(NegC,sameIndividual(L2),_Expl2,ABox),
 1262  member(X,L1),
 1263  member(X,L2),!.
 1264  
 1265check_clash(_,C-Ind1,Tab):-
 1266  get_abox(Tab,ABox),
 1267  %write('clash 4'),nl,
 1268  neg_class(C,NegC),
 1269  findClassAssertion(NegC,sameIndividual(L2),_Expl2,ABox),
 1270  member(Ind1,L2),!.
 1271  
 1272check_clash(_,C-sameIndividual(L1),Tab):-
 1273  get_abox(Tab,ABox),
 1274  %write('clash 5'),nl,
 1275  neg_class(C,NegC),
 1276  findClassAssertion(NegC,Ind2,_,ABox),
 1277  member(Ind2,L1),!.
 1278  
 1279check_clash(M,C1-Ind,Tab):-
 1280  get_abox(Tab,ABox),
 1281  %write('clash 7'),nl,
 1282  M:disjointClasses(L), % TODO use hierarchy
 1283  member(C1,L),
 1284  member(C2,L),
 1285  dif(C1,C2),
 1286  findClassAssertion(C2,Ind,_,ABox),!.
 1287  
 1288check_clash(M,C1-Ind,Tab):-
 1289  get_abox(Tab,ABox),
 1290  %write('clash 8'),nl,
 1291  M:disjointUnion(_Class,L), % TODO use hierarchy
 1292  member(C1,L),
 1293  member(C2,L),
 1294  dif(C1,C2),
 1295  findClassAssertion(C2,Ind,_,ABox),!.
 1296
 1297check_clash(_,P-Ind1-Ind2,Tab):-
 1298  get_abox(Tab,ABox),
 1299  %write('clash 11'),nl,
 1300  neg_class(P,NegP),  % use of neg_class with a property
 1301  findPropertyAssertion(NegP,Ind1,Ind2,_,ABox),!.
 1302
 1303% -------------
 1304% rules application
 1305% -------------
 1306expand_queue(_M,Tab,Tab,Expl):-
 1307  get_clashes(Tab,Clashes),
 1308  dif(Clashes,[]),
 1309  dif(Expl,[]).
 1310
 1311expand_queue(M,Tab,_,_):-
 1312  test_end_expand_queue(M,Tab),!,%gtrace,
 1313  assert(M:tab_end(Tab)),
 1314  fail.
 1315
 1316expand_queue(M,Tab0,Tab,Expl):-
 1317  extract_from_expansion_queue(Tab0,EA,Tab1),!,
 1318  apply_all_rules(M,Tab1,EA,Tab2,Expl),
 1319  % update_queue(M,T,NewExpQueue),
 1320  expand_queue(M,Tab2,Tab,Expl).
 1321
 1322
 1323test_end_expand_queue(M,_):-
 1324  check_time_limit_monitor_status(M),!.
 1325
 1326test_end_expand_queue(_,Tab):-
 1327  expansion_queue_is_empty(Tab).
 1328
 1329%expand_queue(M,ABox0,[_EA|T],ABox):-
 1330%  expand_queue(M,ABox0,T,ABox).
 1331
 1332get_explanation(M,Tab,Expl):-
 1333  get_explanation_int(M,Tab,Expl).
 1334
 1335get_explanation(M,_,Expl):-
 1336  findall(Tab,M:tab_end(Tab),L),
 1337  %retractall(M:tab_end(_)),
 1338  find_expls_from_tab_list(M,L,Expl).
 1339
 1340get_explanation_int(M,Tab,_):-
 1341  test_end_expand_queue(M,Tab),!,
 1342  assert(M:tab_end(Tab)),
 1343  fail.
 1344
 1345get_explanation_int(M,Tab0,Expl):-
 1346  extract_current_from_expansion_queue(Tab0,EA),
 1347  apply_all_rules(M,Tab0,EA,Tab1,Expl0),
 1348  ( dif(Expl0,[]) ->
 1349      Expl = Expl0
 1350      ;
 1351      get_explanation_int(M,Tab1,Expl)
 1352  ).
 1353
 1354apply_all_rules(M,Tab0,EA,Tab,Expl):-
 1355  M:setting_trill(det_rules,Rules),
 1356  apply_det_rules(M,Rules,Tab0,EA,Tab1),
 1357  get_clashes(Tab1,Clash),
 1358  assert(M:tab_end(Tab1)),
 1359  continue_or_return_expl(M,Rules,Tab0,EA,Tab1,Clash,Tab,Expl).
 1360
 1361continue_or_return_expl(M,Rules,Tab0,EA,Tab1,[],Tab,Expl):-!,
 1362  continue(M,Rules,Tab0,EA,Tab1,[],Tab,Expl).
 1363  
 1364continue_or_return_expl(M,_Rules,_Tab0,_EA,Tab,Clash,Tab,Expl):- 
 1365  find_expls(M,Clash,Tab,Expl).
 1366
 1367continue_or_return_expl(M,Rules,Tab0,EA,Tab1,Clash,Tab,Expl):-!,
 1368  continue(M,Rules,Tab0,EA,Tab1,Clash,Tab,Expl).
 1369
 1370continue(M,_Rules,Tab0,EA,Tab1,_Clash,Tab,Expl):-
 1371  retract(M:tab_end(Tab1)),
 1372  pop_clashes(Tab1,_,Tab2),
 1373  ( test_end_apply_rule(M,Tab0,Tab2) ->
 1374      ( set_next_from_expansion_queue(Tab0,_EA1,Tab), 
 1375        Expl=[]
 1376      ) 
 1377      ;
 1378      apply_all_rules(M,Tab2,EA,Tab,Expl)
 1379  ).
 1380
 1381
 1382
 1383apply_det_rules(M,_,Tab,_,Tab):-
 1384  check_time_limit_monitor_status(M),!.
 1385
 1386apply_det_rules(M,[],Tab0,EA,Tab):-
 1387  M:setting_trill(nondet_rules,Rules),
 1388  apply_nondet_rules(M,Rules,Tab0,EA,Tab).
 1389
 1390apply_det_rules(M,[H|_],Tab0,EA,Tab):-
 1391  %C=..[H,Tab,Tab1],
 1392  call(H,M,Tab0,EA,Tab),!.
 1393
 1394apply_det_rules(M,[_|T],Tab0,EA,Tab):-
 1395  apply_det_rules(M,T,Tab0,EA,Tab).
 1396
 1397
 1398apply_nondet_rules(M,_,Tab,_,Tab):-
 1399  check_time_limit_monitor_status(M),!.
 1400
 1401apply_nondet_rules(_,[],Tab,_EA,Tab).
 1402
 1403apply_nondet_rules(M,[H|_],Tab0,EA,Tab):-
 1404  %C=..[H,Tab,L],
 1405  call(H,M,Tab0,EA,L),!,
 1406  member(Tab,L),
 1407  dif(Tab0,Tab).
 1408
 1409apply_nondet_rules(M,[_|T],Tab0,EA,Tab):-
 1410  apply_nondet_rules(M,T,Tab0,EA,Tab).
 1411
 1412
 1413test_end_apply_rule(M,_,_):-
 1414  check_time_limit_monitor_status(M),!.
 1415
 1416test_end_apply_rule(_,Tab0,Tab1):-
 1417  same_tableau(Tab0,Tab1).
 1418
 1419/*
 1420apply_all_rules(M,Tab0,Tab):-
 1421  apply_nondet_rules([or_rule,max_rule],
 1422                  Tab0,Tab1),
 1423  (Tab0=Tab1 ->
 1424  Tab=Tab1;
 1425  apply_all_rules(M,Tab1,Tab)).
 1426
 1427apply_det_rules([],Tab,Tab).
 1428apply_det_rules([H|_],Tab0,Tab):-
 1429  %C=..[H,Tab,Tab1],
 1430  once(call(H,Tab0,Tab)).
 1431apply_det_rules([_|T],Tab0,Tab):-
 1432  apply_det_rules(T,Tab0,Tab).
 1433apply_nondet_rules([],Tab0,Tab):-
 1434  apply_det_rules([o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule],Tab0,Tab).
 1435apply_nondet_rules([H|_],Tab0,Tab):-
 1436  %C=..[H,Tab,L],
 1437  once(call(H,Tab0,L)),
 1438  member(Tab,L),
 1439  dif(Tab0,Tab).
 1440apply_nondet_rules([_|T],Tab0,Tab):-
 1441  apply_nondet_rules(T,Tab0,Tab).
 1442*/
 1443
 1444
 1445/***********
 1446  rules
 1447************/
 1448
 1449/*
 1450  add_exists_rule
 1451  
 1452  Looks up for a role that links 2 individuals, if it find it, it searches a subclass axiom
 1453  in the KB that contains 'someValuesFrom(R,C)' where R is the role which links the 2 individuals
 1454  and C is a class in which the 2nd individual belongs to.
 1455  
 1456  This rule hasn't a corresponding rule in the tableau
 1457  ========================
 1458*/
 1459add_exists_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1460  get_abox(Tab0,ABox),
 1461  findClassAssertion(C,Ind2,Expl2,ABox),
 1462  (unifiable(C,someValuesFrom(_,_),_)->false;
 1463  ( %existsInKB(M,R,C),
 1464    add_tableau_rules_from_class(M,someValuesFrom(R,C)),
 1465    findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox),
 1466    and_f(M,Expl1,Expl2,Expl),
 1467    modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab)
 1468  )).
 1469
 1470add_exists_rule(M,Tab0,[C,Ind2],Tab):-
 1471  (unifiable(C,someValuesFrom(_,_),_)->false;
 1472  ( get_abox(Tab0,ABox),
 1473    findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox),
 1474    %existsInKB(M,R,C),
 1475    add_tableau_rules_from_class(M,someValuesFrom(R,C)),
 1476    findClassAssertion(C,Ind2,Expl2,ABox),
 1477    and_f(M,Expl1,Expl2,Expl),
 1478    modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab)
 1479  )).
 1480
 1481
 1482/*
 1483existsInKB(M,R,C):-
 1484  M:subClassOf(A,B),
 1485  member(someValuesFrom(R,C),[A,B]).
 1486
 1487existsInKB(M,R,C):-
 1488  M:equivalentClasses(L),
 1489  member(someValuesFrom(R,C),L).
 1490*/
 1491
 1492/* *************** */ 
 1493
 1494/*
 1495  and_rule
 1496  =================
 1497*/
 1498and_rule(M,Tab0,[intersectionOf(LC),Ind],Tab):-
 1499  get_abox(Tab0,ABox),
 1500  findClassAssertion(intersectionOf(LC),Ind,Expl,ABox),
 1501  \+ indirectly_blocked(Ind,Tab0),
 1502  scan_and_list(M,LC,Ind,Expl,Tab0,Tab,0).
 1503
 1504
 1505%----------------
 1506scan_and_list(_M,[],_Ind,_Expl,Tab,Tab,Mod):-
 1507  dif(Mod,0).
 1508
 1509scan_and_list(M,[C|T],Ind,Expl,Tab0,Tab,_Mod):-
 1510  modify_ABox(M,Tab0,C,Ind,Expl,Tab1),!,
 1511  scan_and_list(M,T,Ind,Expl,Tab1,Tab,1).
 1512
 1513scan_and_list(M,[_C|T],Ind,Expl,Tab0,Tab,Mod):-
 1514  scan_and_list(M,T,Ind,Expl,Tab0,Tab,Mod).
 1515/* ************* */
 1516
 1517/*
 1518  or_rule
 1519  ===============
 1520*/
 1521or_rule(M,Tab0,[unionOf(LC),Ind],L):- %gtrace,
 1522  get_abox(Tab0,ABox),
 1523  findClassAssertion(unionOf(LC),Ind,Expl,ABox),
 1524  \+ indirectly_blocked(Ind,Tab0), %gtrace,
 1525  %not_ind_intersected_union(Ind,LC,ABox),
 1526  % length(LC,NClasses),
 1527  get_choice_point_id(M,ID),
 1528  scan_or_list(M,LC,0,ID,Ind,Expl,Tab0,L),
 1529  dif(L,[]),
 1530  create_choice_point(M,Ind,or,unionOf(LC),LC,_),!. % last variable whould be equals to ID
 1531
 1532not_ind_intersected_union(Ind,LC,ABox):-
 1533  \+ ind_intersected_union(Ind,LC,ABox).
 1534
 1535ind_intersected_union(Ind,LC,ABox) :-
 1536  member(C,LC),
 1537  findClassAssertion(C,Ind,_,ABox),!.
 1538%---------------
 1539scan_or_list(_,[],_,_,_,_,_,[]):- !.
 1540
 1541scan_or_list(M,[C|T],N0,CP,Ind,Expl0,Tab0,[Tab|L]):-
 1542  add_choice_point(M,cpp(CP,N0),Expl0,Expl),
 1543  modify_ABox(M,Tab0,C,Ind,Expl,Tab),
 1544  N is N0 + 1,
 1545  scan_or_list(M,T,N,CP,Ind,Expl0,Tab0,L).
 1546
 1547/* **************** */
 1548
 1549/*
 1550  exists_rule
 1551  ==================
 1552*/
 1553exists_rule(M,Tab0,[someValuesFrom(R,C),Ind1],Tab):-
 1554  get_abox(Tab0,ABox0),
 1555  findClassAssertion(someValuesFrom(R,C),Ind1,Expl,ABox0),
 1556  \+ blocked(Ind1,Tab0),
 1557  \+ connected_individual(R,C,Ind1,ABox0),
 1558  new_ind(M,Ind2),
 1559  add_edge(R,Ind1,Ind2,Tab0,Tab1),
 1560  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 1561  modify_ABox(M,Tab2,C,Ind2,Expl,Tab3),
 1562  modify_ABox(M,Tab3,R,Ind1,Ind2,Expl,Tab).
 1563
 1564
 1565
 1566%---------------
 1567connected_individual(R,C,Ind1,ABox):-
 1568  findPropertyAssertion(R,Ind1,Ind2,_,ABox),
 1569  findClassAssertion(C,Ind2,_,ABox).
 1570
 1571/* ************ */
 1572
 1573/*
 1574  forall_rule
 1575  ===================
 1576*/
 1577forall_rule(M,Tab0,[allValuesFrom(R,C),Ind1],Tab):-
 1578  get_abox(Tab0,ABox),
 1579  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1580  \+ indirectly_blocked(Ind1,Tab0),
 1581  findClassAssertion(allValuesFrom(R,C),Ind1,Expl1,ABox),
 1582  and_f(M,Expl1,Expl2,Expl),
 1583  modify_ABox(M,Tab0,C,Ind2,Expl,Tab).
 1584
 1585forall_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1586  get_abox(Tab0,ABox),
 1587  findClassAssertion(allValuesFrom(R,C),Ind1,Expl1,ABox),
 1588  \+ indirectly_blocked(Ind1,Tab0),
 1589  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1590  and_f(M,Expl1,Expl2,Expl),
 1591  modify_ABox(M,Tab0,C,Ind2,Expl,Tab).
 1592
 1593/* ************** */
 1594
 1595/*
 1596  forall_plus_rule
 1597  =================
 1598*/
 1599forall_plus_rule(M,Tab0,[allValuesFrom(S,C),Ind1],Tab):-
 1600  get_abox(Tab0,ABox),
 1601  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1602  find_sub_sup_trans_role(M,R,S,Expl3),
 1603  findClassAssertion(allValuesFrom(S,C),Ind1,Expl1,ABox),
 1604  \+ indirectly_blocked(Ind1,Tab0),
 1605  and_f(M,Expl1,Expl2,ExplT),
 1606  and_f(M,ExplT,Expl3,Expl),
 1607  modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab).
 1608
 1609forall_plus_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1610  get_abox(Tab0,ABox),
 1611  findClassAssertion(allValuesFrom(S,C),Ind1,Expl1,ABox),
 1612  \+ indirectly_blocked(Ind1,Tab0),
 1613  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1614  find_sub_sup_trans_role(M,R,S,Expl3),
 1615  and_f(M,Expl1,Expl2,ExplT),
 1616  and_f(M,ExplT,Expl3,Expl),
 1617  modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab).
 1618
 1619% --------------
 1620find_sub_sup_trans_role(M,R,S,Expl):-
 1621  M:subPropertyOf(R,S),
 1622  M:transitiveProperty(R),
 1623  initial_expl(M,EExpl),
 1624  and_f_ax(M,subPropertyOf(R,S),EExpl,Expl0),
 1625  and_f_ax(M,transitive(R),Expl0,Expl).
 1626
 1627find_sub_sup_trans_role(M,R,S,Expl):-
 1628  M:subPropertyOf(R,S),
 1629  \+ M:transitiveProperty(R),
 1630  initial_expl(M,EExpl),
 1631  and_f_ax(M,subPropertyOf(R,S),EExpl,Expl).
 1632/* ************ */
 1633
 1634/*
 1635  unfold_rule
 1636  ===========
 1637*/
 1638
 1639unfold_rule(M,Tab0,[C,Ind],Tab):-
 1640  get_abox(Tab0,ABox),
 1641  findClassAssertion(C,Ind,Expl,ABox),
 1642  % usare findall(D-AX,find_sub_sup_class(M,C,D,Ax),L) e iniziare ciclo per evitare di ripetere stessi test più volte
 1643  find_sub_sup_class(M,C,D,Ax),
 1644  and_f_ax(M,Ax,Expl,AxL),
 1645  modify_ABox(M,Tab0,D,Ind,AxL,Tab1),
 1646  add_nominal(M,D,Ind,Tab1,Tab).
 1647
 1648/* -- unfold_rule
 1649      takes a class C1 in which Ind belongs, find a not atomic class C
 1650      that contains C1 (C is seen as list of classes), controls if
 1651      the individual Ind belongs to all those classes, if yes it finds a class D (if exists)
 1652      that is the superclass or an equivalent class of C and adds D to label of Ind
 1653      - for managing tableau with more than one clash -
 1654      correspond to the ce_rule
 1655   --
 1656*/
 1657unfold_rule(M,Tab0,[C1,Ind],Tab):-
 1658  find_not_atomic(M,C1,C,L),
 1659  get_abox(Tab0,ABox),
 1660  ( C = unionOf(_) -> findClassAssertion(C1,Ind,Expl,ABox)
 1661   ; find_all(M,Ind,L,ABox,Expl)),
 1662  %find_sub_sup_class(M,C,D,Ax),
 1663  %and_f_ax(M,Ax,Expl1,AxL1),
 1664  modify_ABox(M,Tab0,C,Ind,Expl,Tab1),
 1665  add_nominal(M,C,Ind,Tab1,Tab).
 1666
 1667/* -- unfold_rule
 1668 *    control propertyRange e propertyDomain
 1669 * --
 1670 */
 1671unfold_rule(M,Tab0,[P,S,O],Tab):-
 1672  get_abox(Tab0,ABox),
 1673  find_class_prop_range_domain(M,P,S,O,Ind,D,Expl,ABox),
 1674  modify_ABox(M,Tab0,D,Ind,Expl,Tab1),
 1675  add_nominal(M,D,Ind,Tab1,Tab).
 1676
 1677/*
 1678 * -- unfold_rule
 1679 *    manage the negation
 1680 * --
 1681 */
 1682unfold_rule(M,Tab0,[complementOf(C),Ind],Tab):-
 1683  get_abox(Tab0,ABox),
 1684  findClassAssertion(complementOf(C),Ind,Expl,ABox),
 1685  find_neg_class(C,D),
 1686  and_f_ax(M,complementOf(C),Expl,AxL),
 1687  modify_ABox(M,Tab0,D,Ind,AxL,Tab1),
 1688  add_nominal(M,D,Ind,Tab1,Tab).
 1689
 1690% ----------------
 1691% add_nominal
 1692
 1693add_nominal(M,D,Ind,Tab0,Tab):-
 1694  get_abox(Tab0,ABox0),
 1695  ((D = oneOf(_),
 1696    \+ member(nominal(Ind),ABox0))
 1697    ->
 1698   (
 1699     ABox1 = [nominal(Ind)|ABox0],
 1700     (member((classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),_E),ABox1)
 1701     ->
 1702     set_abox(Tab0,ABox1,Tab)
 1703     ;
 1704     (empty_expl(M,Expl),set_abox(Tab0,[(classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),Expl)|ABox1],Tab))
 1705     )
 1706   )
 1707    ;
 1708  set_abox(Tab0,ABox0,Tab)
 1709  ).
 1710
 1711% ----------------
 1712% unionOf, intersectionOf, subClassOf, negation, allValuesFrom, someValuesFrom, exactCardinality(min and max), maxCardinality, minCardinality
 1713:- multifile find_neg_class/2. 1714
 1715find_neg_class(unionOf(L),intersectionOf(NL)):-
 1716  neg_list(L,NL).
 1717
 1718find_neg_class(intersectionOf(L),unionOf(NL)):-
 1719  neg_list(L,NL).
 1720
 1721find_neg_class(subClassOf(C,D),intersectionOf(C,ND)):-
 1722  neg_class(D,ND).
 1723
 1724find_neg_class(complementOf(C),C).
 1725
 1726find_neg_class(allValuesFrom(R,C),someValuesFrom(R,NC)):-
 1727  neg_class(C,NC).
 1728
 1729find_neg_class(someValuesFrom(R,C),allValuesFrom(R,NC)):-
 1730  neg_class(C,NC).
 1731
 1732% ---------------
 1733
 1734neg_class(complementOf(C),C):- !.
 1735
 1736neg_class(C,complementOf(C)).
 1737
 1738% ---------------
 1739
 1740neg_list([],[]).
 1741
 1742neg_list([H|T],[complementOf(H)|T1]):-
 1743  neg_list(T,T1).
 1744
 1745neg_list([complementOf(H)|T],[H|T1]):-
 1746  neg_list(T,T1).
 1747
 1748% ----------------
 1749
 1750find_class_prop_range_domain(M,P,S,O,O,D,Expl,ABox):-
 1751  findPropertyAssertion(P,S,O,ExplPA,ABox),
 1752  %ind_as_list(IndL,L),
 1753  %member(Ind,L),
 1754  M:propertyRange(P,D),
 1755  and_f_ax(M,propertyRange(P,D),ExplPA,Expl).
 1756
 1757find_class_prop_range_domain(M,P,S,O,S,D,Expl,ABox):-
 1758  findPropertyAssertion(P,S,O,ExplPA,ABox),
 1759  %ind_as_list(IndL,L),
 1760  %member(Ind,L),
 1761  M:propertyDomain(P,D),
 1762  and_f_ax(M,propertyDomain(P,D),ExplPA,Expl).
 1763
 1764
 1765%-----------------
 1766:- multifile find_sub_sup_class/4. 1767
 1768% subClassOf
 1769find_sub_sup_class(M,C,D,subClassOf(C,D)):-
 1770  M:subClassOf(C,D).
 1771
 1772%equivalentClasses
 1773find_sub_sup_class(M,C,D,equivalentClasses(L)):-
 1774  M:equivalentClasses(L),
 1775  member(C,L),
 1776  member(D,L),
 1777  dif(C,D).
 1778
 1779%concept for concepts allValuesFrom
 1780find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(R,D),Ax):-
 1781  find_sub_sup_class(M,C,D,Ax),
 1782  atomic(D).
 1783
 1784%role for concepts allValuesFrom
 1785find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(S,C),subPropertyOf(R,S)):-
 1786  M:subPropertyOf(R,S).
 1787
 1788%concept for concepts someValuesFrom
 1789find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(R,D),Ax):-
 1790  find_sub_sup_class(M,C,D,Ax),
 1791  atomic(D).
 1792
 1793%role for concepts someValuesFrom
 1794find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(S,C),subPropertyOf(R,S)):-
 1795  M:subPropertyOf(R,S).
 1796
 1797
 1798/*******************
 1799 managing the concept (C subclassOf Thing)
 1800 this implementation doesn't work well in a little set of cases
 1801 TO IMPROVE!
 1802 *******************/
 1803/*
 1804find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1805  M:subClassOf(A,B),
 1806  member(C,[A,B]),!.
 1807
 1808find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1809  M:classAssertion(C,_),!.
 1810
 1811find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1812  M:equivalentClasses(L),
 1813  member(C,L),!.
 1814
 1815find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1816  M:unionOf(L),
 1817  member(C,L),!.
 1818
 1819find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1820  M:equivalentClasses(L),
 1821  member(someValuesFrom(_,C),L),!.
 1822
 1823find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1824  M:equivalentClasses(L),
 1825  member(allValuesFrom(_,C),L),!.
 1826
 1827find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1828  M:equivalentClasses(L),
 1829  member(minCardinality(_,_,C),L),!.
 1830
 1831find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1832  M:equivalentClasses(L),
 1833  member(maxCardinality(_,_,C),L),!.
 1834
 1835find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1836  M:equivalentClasses(L),
 1837  member(exactCardinality(_,_,C),L),!.
 1838
 1839*/
 1840
 1841%--------------------
 1842% looks for not atomic concepts descriptions containing class C
 1843find_not_atomic(M,C,Ax,LC):-
 1844  M:subClassOf(A,B),
 1845  find_not_atomic_int(C,[A,B],Ax,LC).
 1846
 1847find_not_atomic(M,C,Ax,LC):-
 1848  M:equivalentClasses(L),
 1849  find_not_atomic_int(C,L,Ax,LC).
 1850
 1851/*
 1852find_not_atomic(M,C,unionOf(L1),L1):-
 1853  M:subClassOf(A,B),
 1854  member(unionOf(L1),[A,B]),
 1855  member(C,L1).
 1856
 1857find_not_atomic(M,C,unionOf(L1),L1):-
 1858  M:equivalentClasses(L),
 1859  member(unionOf(L1),L),
 1860  member(C,L1).
 1861*/
 1862
 1863find_not_atomic_int(C,LC0,intersectionOf(L1),L1):-
 1864  member(intersectionOf(L1),LC0),
 1865  member(C,L1).
 1866
 1867find_not_atomic_int(C,LC0,Ax,LC):-
 1868  member(intersectionOf(L1),LC0),
 1869  find_not_atomic_int(C,L1,Ax,LC).
 1870
 1871find_not_atomic_int(C,LC0,unionOf(L1),L1):-
 1872  member(unionOf(L1),LC0),
 1873  member(C,L1).
 1874
 1875find_not_atomic_int(C,LC0,Ax,LC):-
 1876  member(unionOf(L1),LC0),
 1877  find_not_atomic_int(C,L1,Ax,LC).
 1878
 1879
 1880
 1881
 1882% -----------------------
 1883% puts together the explanations of all the concepts found by find_not_atomic/3
 1884find_all(_M,_,[],_,[]).
 1885
 1886find_all(M,Ind,[H|T],ABox,ExplT):-
 1887  findClassAssertion(H,Ind,Expl1,ABox),
 1888  find_all(M,Ind,T,ABox,Expl2),
 1889  and_f(M,Expl1,Expl2,ExplT).
 1890
 1891
 1892% ------------------------
 1893%  unfold_rule to unfold roles
 1894% ------------------------
 1895% sub properties
 1896unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1897  get_abox(Tab0,ABox),
 1898  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1899  find_sub_sup_property(M,C,D,Ax),
 1900  and_f_ax(M,Ax,Expl,AxL),
 1901  modify_ABox(M,Tab0,D,Ind1,Ind2,AxL,Tab1),
 1902  add_nominal(M,D,Ind1,Tab1,Tab2),
 1903  add_nominal(M,D,Ind2,Tab2,Tab).
 1904
 1905%inverseProperties
 1906unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1907  get_abox(Tab0,ABox),
 1908  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1909  find_inverse_property(M,C,D,Ax),
 1910  and_f_ax(M,Ax,Expl,AxL),
 1911  modify_ABox(M,Tab0,D,Ind2,Ind1,AxL,Tab1),
 1912  add_nominal(M,D,Ind1,Tab1,Tab2),
 1913  add_nominal(M,D,Ind2,Tab2,Tab).
 1914
 1915%transitiveProperties
 1916unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1917  get_abox(Tab0,ABox),
 1918  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1919  find_transitive_property(M,C,Ax),
 1920  and_f_ax(M,Ax,Expl,AxL),
 1921  findPropertyAssertion(C,Ind2,Ind3,ExplSecond,ABox),
 1922  and_f(M,AxL,ExplSecond,ExplTrans),
 1923  modify_ABox(M,Tab0,C,Ind1,Ind3,ExplTrans,Tab).
 1924
 1925%-----------------
 1926% subPropertyOf
 1927find_sub_sup_property(M,C,D,subPropertyOf(C,D)):-
 1928  M:subPropertyOf(C,D).
 1929
 1930%equivalentProperties
 1931find_sub_sup_property(M,C,D,equivalentProperties(L)):-
 1932  M:equivalentProperties(L),
 1933  member(C,L),
 1934  member(D,L),
 1935  dif(C,D).
 1936
 1937%-----------------
 1938%inverseProperties
 1939find_inverse_property(M,C,D,inverseProperties(C,D)):-
 1940  M:inverseProperties(C,D).
 1941
 1942find_inverse_property(M,C,D,inverseProperties(D,C)):-
 1943  M:inverseProperties(D,C).
 1944
 1945%inverseProperties
 1946find_inverse_property(M,C,C,symmetricProperty(C)):-
 1947  M:symmetricProperty(C).
 1948
 1949%-----------------
 1950%transitiveProperties
 1951find_transitive_property(M,C,transitiveProperty(C)):-
 1952  M:transitiveProperty(C).
 1953/* ************* */
 1954
 1955/*
 1956  ce_rule
 1957  =============
 1958*/
 1959ce_rule(M,Tab0,Tab):-
 1960  get_tabs(Tab0,(T,_,_)),
 1961  find_not_sub_sup_class(M,Ax,UnAx),
 1962  vertices(T,Inds),
 1963  apply_ce_to(M,Inds,Ax,UnAx,Tab0,Tab,C),
 1964  C @> 0.
 1965
 1966
 1967% ------------------
 1968find_not_sub_sup_class(M,subClassOf(C,D),unionOf(complementOf(C),D)):-
 1969  M:subClassOf(C,D),
 1970  \+ atomic(C).
 1971
 1972
 1973find_not_sub_sup_class(M,equivalentClasses(L),unionOf(L1)):-
 1974  M:equivalentClasses(L),
 1975  member(C,L),
 1976  \+ atomic(C),
 1977  copy_neg_c(C,L,L1).
 1978
 1979%-------------------------
 1980copy_neg_c(_,[],[]).
 1981
 1982copy_neg_c(C,[C|T],[complementOf(C)|T1]):-
 1983  !,
 1984  copy_neg_c(C,T,T1).
 1985
 1986copy_neg_c(C,[H|T],[H|T1]):-
 1987  copy_neg_c(C,T,T1).
 1988
 1989%---------------------
 1990apply_ce_to(_M,[],_,_,Tab,Tab,0).
 1991
 1992apply_ce_to(M,[Ind|T],Ax,UnAx,Tab0,Tab,C):-
 1993  \+ indirectly_blocked(Ind,Tab),
 1994  modify_ABox(M,Tab0,UnAx,Ind,[Ax],Tab1),!,
 1995  apply_ce_to(M,T,Ax,UnAx,Tab1,Tab,C0),
 1996  C is C0 + 1.
 1997
 1998apply_ce_to(M,[_Ind|T],Ax,UnAx,Tab0,Tab,C):-
 1999  apply_ce_to(M,T,Ax,UnAx,Tab0,Tab,C).
 2000
 2001/* **************** */
 2002
 2003/*
 2004  min_rule
 2005  =============
 2006*/
 2007min_rule(M,Tab0,[minCardinality(N,S),Ind1],Tab):-
 2008  get_abox(Tab0,ABox),
 2009  findClassAssertion(minCardinality(N,S),Ind1,Expl,ABox),
 2010  \+ blocked(Ind1,Tab0),
 2011  s_neighbours(M,Ind1,S,Tab0,SN),
 2012  safe_s_neigh(SN,S,Tab0,SS),
 2013  length(SS,LSS),
 2014  LSS @< N,
 2015  NoI is N-LSS,
 2016  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1),
 2017  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 2018
 2019
 2020min_rule(M,Tab0,[minCardinality(N,S,C),Ind1],Tab):-
 2021  get_abox(Tab0,ABox),
 2022  findClassAssertion(minCardinality(N,S,C),Ind1,Expl,ABox),
 2023  \+ blocked(Ind1,Tab0),
 2024  s_neighbours(M,Ind1,S,Tab0,SN),
 2025  safe_s_neigh_C(SN,S,C,Tab0,ABox,SS),
 2026  length(SS,LSS),
 2027  LSS @< N,
 2028  NoI is N-LSS,
 2029  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1),
 2030  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 2031
 2032min_rule(M,Tab0,[exactCardinality(N,S),Ind1],Tab):-
 2033  get_abox(Tab0,ABox),
 2034  findClassAssertion(exactCardinality(N,S),Ind1,Expl,ABox),
 2035  \+ blocked(Ind1,Tab0),
 2036  s_neighbours(M,Ind1,S,Tab0,SN),
 2037  safe_s_neigh(SN,S,Tab0,SS),
 2038  length(SS,LSS),
 2039  LSS @< N,
 2040  NoI is N-LSS,
 2041  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1),
 2042  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 2043
 2044
 2045min_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],Tab):-
 2046  get_abox(Tab0,ABox),
 2047  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl,ABox),
 2048  \+ blocked(Ind1,Tab0),
 2049  s_neighbours(M,Ind1,S,Tab0,SN),
 2050  safe_s_neigh_C(SN,S,C,Tab0,SS),
 2051  length(SS,LSS),
 2052  LSS @< N,
 2053  NoI is N-LSS,
 2054  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1),
 2055  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 2056
 2057min_rule(M,(ABox,Tabs),([(differentIndividuals(NI),Expl)|ABox1],Tabs1)):-
 2058  findClassAssertion(exactCardinality(N,S),Ind1,Expl,ABox),
 2059  \+ blocked(Ind1,(ABox,Tabs)),
 2060  s_neighbours(M,Ind1,S,(ABox,Tabs),SN),
 2061  safe_s_neigh(SN,S,(ABox,Tabs),SS),
 2062  length(SS,LSS),
 2063  LSS @< N,
 2064  NoI is N-LSS,
 2065  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,ABox,Tabs,ABox1,Tabs1).
 2066
 2067
 2068min_rule(M,(ABox,Tabs),([(differentIndividuals(NI),Expl)|ABox1],Tabs1)):-
 2069  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl,ABox),
 2070  \+ blocked(Ind1,(ABox,Tabs)),
 2071  s_neighbours(M,Ind1,S,(ABox,Tabs),SN),
 2072  safe_s_neigh(SN,S,(ABox,Tabs),SS),
 2073  length(SS,LSS),
 2074  LSS @< N,
 2075  NoI is N-LSS,
 2076  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,ABox,Tabs,ABox1,Tabs1).
 2077
 2078% ----------------------
 2079min_rule_neigh(_,0,_,_,_,[],Tab,Tab).
 2080
 2081min_rule_neigh(M,N,S,Ind1,Expl,[Ind2|NI],Tab0,Tab):-
 2082  N > 0,
 2083  NoI is N-1,
 2084  new_ind(M,Ind2),
 2085  add_edge(S,Ind1,Ind2,Tab0,Tab1),
 2086  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 2087  modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3),
 2088  %check_block(Ind2,Tab3),
 2089  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab3,Tab).
 2090
 2091%----------------------
 2092min_rule_neigh_C(_,0,_,_,_,_,[],Tab,Tab).
 2093
 2094min_rule_neigh_C(M,N,S,C,Ind1,Expl,[Ind2|NI],Tab0,Tab):-
 2095  N > 0,
 2096  NoI is N-1,
 2097  new_ind(M,Ind2),
 2098  add_edge(S,Ind1,Ind2,Tab0,Tab1),
 2099  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 2100  modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3),
 2101  modify_ABox(M,Tab3,C,Ind2,[propertyAssertion(S,Ind1,Ind2)|Expl],Tab4),
 2102  %check_block(Ind2,Tab4),
 2103  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab4,Tab).
 2104
 2105%---------------------
 2106safe_s_neigh([],_,_,[]):-!.
 2107
 2108safe_s_neigh([H|T],S,Tab,[H|ST]):-
 2109  safe(H,S,Tab),
 2110  safe_s_neigh(T,S,Tab,ST).
 2111
 2112safe_s_neigh_C(L,S,C,Tab,LT):-
 2113  get_abox(Tab,ABox),
 2114  safe_s_neigh_C(L,S,C,Tab,ABox,LT).
 2115
 2116safe_s_neigh_C([],_,_,_,_,_,[]):-!.
 2117
 2118safe_s_neigh_C([H|T],S,C,Tab,ABox,[H|ST]):-
 2119  safe(H,S,Tab),
 2120  findClassAssertion(C,H,_,ABox),!,
 2121  safe_s_neigh_C(T,S,C,Tab,ABox,ST).
 2122
 2123/* **************** */
 2124
 2125/*
 2126  max_rule
 2127  ================
 2128*/
 2129max_rule(M,Tab0,[maxCardinality(N,S),Ind],L):-
 2130  get_abox(Tab0,ABox),
 2131  findClassAssertion(maxCardinality(N,S),Ind,Expl0,ABox),
 2132  \+ indirectly_blocked(Ind,Tab0),
 2133  s_neighbours(M,Ind,S,Tab0,SN),
 2134  length(SN,LSS),
 2135  LSS @> N,
 2136  get_choice_point_id(M,ID),
 2137  scan_max_list(M,maxCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 2138
 2139max_rule(M,Tab0,[maxCardinality(N,S,C),Ind],L):-%gtrace,
 2140  get_abox(Tab0,ABox),
 2141  findClassAssertion(maxCardinality(N,S,C),Ind,Expl0,ABox),
 2142  \+ indirectly_blocked(Ind,Tab0),
 2143  s_neighbours(M,Ind,S,Tab0,SN),
 2144  individual_class_C(SN,C,ABox,SNC),
 2145  length(SNC,LSS),
 2146  LSS @> N,
 2147  get_choice_point_id(M,ID),%gtrace,
 2148  scan_max_list(M,maxCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 2149
 2150%---------------------
 2151
 2152max_rule(M,Tab0,[exactCardinality(N,S),Ind],L):-
 2153  get_abox(Tab0,ABox),
 2154  findClassAssertion(exactCardinality(N,S),Ind,Expl0,ABox),
 2155  \+ indirectly_blocked(Ind,Tab0),
 2156  s_neighbours(M,Ind,S,Tab0,SN),
 2157  length(SN,LSS),
 2158  LSS @> N,
 2159  get_choice_point_id(M,ID),
 2160  scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 2161
 2162max_rule(M,Tab0,[exactCardinality(N,S,C),Ind],L):-
 2163  get_abox(Tab0,ABox),
 2164  findClassAssertion(exactCardinality(N,S,C),Ind,Expl0,ABox),
 2165  \+ indirectly_blocked(Ind,Tab0),
 2166  s_neighbours(M,Ind,S,Tab0,SN),
 2167  individual_class_C(SN,C,ABox,SNC),
 2168  length(SNC,LSS),
 2169  LSS @> N,
 2170  get_choice_point_id(M,ID),%gtrace,
 2171  scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 2172
 2173max_rule(M,Tab0,[S,Ind,_],L):-
 2174  get_abox(Tab0,ABox),
 2175  findClassAssertion(exactCardinality(N,S),Ind,Expl0,ABox),
 2176  \+ indirectly_blocked(Ind,Tab0),
 2177  s_neighbours(M,Ind,S,Tab0,SN),
 2178  length(SN,LSS),
 2179  LSS @> N,
 2180  get_choice_point_id(M,ID),
 2181  scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 2182
 2183max_rule(M,Tab0,[S,Ind,_],L):-
 2184  get_abox(Tab0,ABox),
 2185  findClassAssertion(exactCardinality(N,S,C),Ind,Expl0,ABox),
 2186  \+ indirectly_blocked(Ind,Tab0),
 2187  s_neighbours(M,Ind,S,Tab0,SN),
 2188  individual_class_C(SN,C,ABox,SNC),
 2189  length(SNC,LSS),
 2190  LSS @> N,
 2191  get_choice_point_id(M,ID),%gtrace,
 2192  scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 2193
 2194%---------------------
 2195
 2196scan_max_list(M,MaxCardClass,S,C,SN,CP,Ind,Expl,Tab0,ABox,Tab_list):-
 2197  create_couples_for_merge(SN,[],Ind_couples), % MAYBE check_individuals_not_equal(M,YI,YJ,ABox), instead of dif
 2198  length(Ind_couples,NChoices),
 2199  (
 2200    NChoices @> 1 -> (FirstChoice = -1) ; (FirstChoice = 0)
 2201  ),
 2202  create_list_for_max_rule(M,Ind_couples,FirstChoice,CP,Ind,S,C,Expl,Tab0,ABox,Tab_list),
 2203  dif(Tab_list,[]),
 2204  ( dif(FirstChoice,-1) ->
 2205    create_choice_point(M,Ind,mr,MaxCardClass,Ind_couples,_)
 2206    ;
 2207    true
 2208  ). % last variable whould be equals to ID
 2209
 2210create_couples_for_merge([],Ind_couples,Ind_couples).
 2211
 2212create_couples_for_merge([H|T],Ind_couples0,Ind_couples):-
 2213  create_couples_for_merge_int(H,T,Ind_couples0,Ind_couples1),
 2214  create_couples_for_merge(T,Ind_couples1,Ind_couples).
 2215
 2216create_couples_for_merge_int(_,[],Ind_couples,Ind_couples).
 2217
 2218create_couples_for_merge_int(I,[H|T],Ind_couples0,Ind_couples):-
 2219  create_couples_for_merge_int(I,T,[I-H|Ind_couples0],Ind_couples).
 2220
 2221create_list_for_max_rule(_,[],_,_,_,_,_,_,_,_,[]).
 2222
 2223create_list_for_max_rule(M,[YI-YJ|Ind_couples],N0,CP,Ind,S,C,Expl0,Tab0,ABox,[Tab|Tab_list]):-
 2224  findPropertyAssertion(S,Ind,YI,ExplYI,ABox),
 2225  findPropertyAssertion(S,Ind,YJ,ExplYJ,ABox),
 2226  findClassAssertion(C,YI,ExplCYI,ABox),
 2227  findClassAssertion(C,YJ,ExplCYJ,ABox),
 2228  and_f(M,ExplYI,ExplYJ,ExplS0),
 2229  and_f(M,ExplS0,ExplCYI,ExplS1),
 2230  and_f(M,ExplS1,ExplCYJ,ExplC0),
 2231  and_f(M,ExplC0,Expl0,ExplT0),
 2232  (
 2233    dif(N0,-1) ->
 2234    (
 2235      add_choice_point(M,cpp(CP,N0),ExplT0,ExplT),
 2236      N is N0 + 1
 2237    ) ;
 2238    (
 2239      ExplT = ExplT0,
 2240      N = N0
 2241    )
 2242  ),
 2243  flatten([YI,YJ],LI),
 2244  merge_all_individuals(M,[(sameIndividual(LI),ExplT)],Tab0,Tab),
 2245  create_list_for_max_rule(M,Ind_couples,N,CP,Ind,S,C,Expl0,Tab0,ABox,Tab_list).
 2246
 2247/*
 2248scan_max_list(M,S,SN,CP,Ind,Expl,ABox0,Tabs0,YI-YJ,ABox,Tabs):-
 2249  member(YI,SN),
 2250  member(YJ,SN),
 2251  % generate cp
 2252  check_individuals_not_equal(M,YI,YJ,ABox0),
 2253  findPropertyAssertion(S,Ind,YI,ExplYI,ABox0),
 2254  findPropertyAssertion(S,Ind,YJ,ExplYJ,ABox0),
 2255  and_f(M,ExplYI,ExplYJ,Expl0),
 2256  and_f(M,Expl0,Expl,ExplT0),
 2257  add_choice_point(M,cpp(CP,N0),ExplT0,ExplT),
 2258  merge_all_individuals(M,[(sameIndividual([YI,YJ]),ExplT)],ABox0,Tabs0,ABox,Tabs).
 2259*/
 2260
 2261%--------------------
 2262check_individuals_not_equal(M,X,Y,ABox):-
 2263  dif(X,Y),
 2264  \+ same_ind(M,[X],Y,ABox).
 2265%--------------------
 2266individual_class_C([],_,_,[]).
 2267
 2268individual_class_C([H|T],C,ABox,[H|T1]):-
 2269  findClassAssertion(C,H,_,ABox),!,
 2270  individual_class_C(T,C,ABox,T1).
 2271
 2272individual_class_C([_H|T],C,ABox,T1):-
 2273  %\+ findClassAssertion(C,H,_,ABox),
 2274  individual_class_C(T,C,ABox,T1).
 2275/* *************** */
 2276
 2277/*
 2278  ch_rule
 2279  ================
 2280*/
 2281ch_rule(M,Tab0,[maxCardinality(N,S,C),Ind1],L):-
 2282  get_abox(Tab0,ABox),
 2283  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2284  \+ indirectly_blocked(Ind1,Tab0),
 2285  findClassAssertion(maxCardinality(N,S,C),Ind1,Expl1,ABox),
 2286  absent_c_not_c(Ind2,C,ABox),
 2287  and_f(M,Expl1,Expl2,Expl),
 2288  get_choice_point_id(M,ID),%gtrace,
 2289  neg_class(C,NC),
 2290  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2291  dif(L,[]),
 2292  create_choice_point(M,Ind2,ch,maxCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2293
 2294ch_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],L):-
 2295  get_abox(Tab0,ABox),
 2296  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2297  \+ indirectly_blocked(Ind1,Tab0),
 2298  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl1,ABox),
 2299  absent_c_not_c(Ind2,C,ABox),
 2300  and_f(M,Expl1,Expl2,Expl),
 2301  get_choice_point_id(M,ID),%gtrace,
 2302  neg_class(C,NC),
 2303  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2304  dif(L,[]),
 2305  create_choice_point(M,Ind2,ch,exactCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2306
 2307ch_rule(M,Tab0,[S,Ind1,Ind2],L):-
 2308  get_abox(Tab0,ABox),
 2309  findClassAssertion(maxCardinality(N,S,C),Ind1,Expl1,ABox),
 2310  \+ indirectly_blocked(Ind1,Tab0),
 2311  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2312  absent_c_not_c(Ind2,C,ABox),
 2313  and_f(M,Expl1,Expl2,Expl),
 2314  get_choice_point_id(M,ID),%gtrace,
 2315  neg_class(C,NC),
 2316  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2317  dif(L,[]),
 2318  create_choice_point(M,Ind2,ch,maxCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2319
 2320ch_rule(M,Tab0,[S,Ind1,Ind2],L):-
 2321  get_abox(Tab0,ABox),
 2322  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl1,ABox),
 2323  \+ indirectly_blocked(Ind1,Tab0),
 2324  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2325  absent_c_not_c(Ind2,C,ABox),
 2326  and_f(M,Expl1,Expl2,Expl),
 2327  get_choice_point_id(M,ID),%gtrace,
 2328  neg_class(C,NC),
 2329  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2330  dif(L,[]),
 2331  create_choice_point(M,Ind2,ch,exactCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2332
 2333%---------------------
 2334
 2335absent_c_not_c(Ind,C,ABox) :-
 2336  \+ is_there_c_not_c(Ind,C,ABox).
 2337
 2338is_there_c_not_c(Ind,C,ABox) :-
 2339 findClassAssertion(C,Ind,_,ABox),!.
 2340
 2341is_there_c_not_c(Ind,C,ABox) :-
 2342  neg_class(C,NC),
 2343  findClassAssertion(NC,Ind,_,ABox),!.
 2344
 2345/* *************** */
 2346
 2347/*
 2348 o_rule
 2349 ============
 2350*/
 2351
 2352o_rule(M,Tab0,[oneOf(C),X],Tab):-
 2353  get_abox(Tab0,ABox),
 2354  findClassAssertion(oneOf(C),X,ExplX,ABox),
 2355  findClassAssertion(oneOf(D),Y,ExplY,ABox),
 2356  containsCommon(C,D),
 2357  dif(X,Y),
 2358  notDifferentIndividuals(M,X,Y,ABox),
 2359  nominal(C,Tab),
 2360  ind_as_list(X,LX),
 2361  ind_as_list(Y,LY),
 2362  and_f(M,ExplX,ExplY,ExplC),
 2363  merge(M,X,Y,ExplC,Tab0,Tab),
 2364  flatten([LX,LY],LI0),
 2365  sort(LI0,LI),
 2366  absent(sameIndividual(LI),ExplC,ABox).
 2367
 2368containsCommon(L1,L2):-
 2369  member(X,L1),
 2370  member(X,L2),!.
 2371% -------------------
 2372
 2373/* ************* */
 2374
 2375/***********
 2376  utility for sameIndividual
 2377************/
 2378
 2379ind_as_list(sameIndividual(L),L):-
 2380  retract_sameIndividual(L),!.
 2381
 2382ind_as_list(X,[X]):-
 2383  atomic(X).
 2384
 2385list_as_sameIndividual(L0,sameIndividual(L)):-
 2386  list_as_sameIndividual_int(L0,L1),
 2387  sort(L1,L).
 2388
 2389list_as_sameIndividual_int([],[]).
 2390
 2391list_as_sameIndividual_int([sameIndividual(L0)|T0],L):-
 2392  !,
 2393  append(L0,T0,L1),
 2394  list_as_sameIndividual_int(L1,L).
 2395
 2396list_as_sameIndividual_int([H|T0],[H|T]):-
 2397  list_as_sameIndividual_int(T0,T).
 2398
 2399
 2400find_same(H,ABox,L,Expl):-
 2401  find((sameIndividual(L),Expl),ABox),
 2402  member(X,L),
 2403  member(X,H),!.
 2404
 2405find_same(_H,_ABox,[],[]).
 2406
 2407
 2408/*
 2409 retract_sameIndividual(L)
 2410 ==========
 2411*/
 2412retract_sameIndividual(sameIndividual(L)):-
 2413  !,
 2414  retract_sameIndividual(L).
 2415
 2416retract_sameIndividual(L):-
 2417  get_trill_current_module(N),
 2418  retract(N:sameIndividual(L)).
 2419
 2420retract_sameIndividual(L):-
 2421  get_trill_current_module(N),
 2422  \+ retract(N:sameIndividual(L)).
 2423/* ****** */
 2424
 2425/*
 2426 * nominal/2, blockable/2, blocked/2, indirectly_blocked/2 and safe/3
 2427 *
 2428 */
 2429
 2430nominal(Inds,Tab):-
 2431  get_abox(Tab,ABox),
 2432  find((nominal(Ind)),ABox),
 2433  member(Ind,Inds).
 2434
 2435% ----------------
 2436
 2437blockable(Ind,Tab):-
 2438  get_abox(Tab,ABox),
 2439  ( find((nominal(Ind)),ABox)
 2440    ->
 2441    false
 2442    ;
 2443    true ).
 2444
 2445% ---------------
 2446
 2447blocked(Ind,Tab):-
 2448  check_block(Ind,Tab).
 2449
 2450/*
 2451
 2452  control for blocking an individual
 2453
 2454*/
 2455
 2456check_block(Ind,Tab):-
 2457  blockable(Ind,Tab),
 2458  get_tabs(Tab,(T,_,_)),
 2459  transpose_ugraph(T,T1),
 2460  ancestor_nt(Ind,T1,A),
 2461  neighbours(Ind,T1,N),
 2462  check_block1(Ind,A,N,Tab),!.
 2463
 2464check_block(Ind,Tab):-
 2465  blockable(Ind,Tab),
 2466  get_tabs(Tab,(T,_,_)),
 2467  transpose_ugraph(T,T1),
 2468  neighbours(Ind,T1,N),
 2469  check_block2(N,Tab),!.
 2470
 2471
 2472check_block1(Indx,A,N,Tab):-
 2473  member(Indx0,N),
 2474  member(Indy,A),
 2475  member(Indy0,A),
 2476  get_tabs(Tab,(T,RBN,_)),
 2477  neighbours(Indy,T,N2),
 2478  member(Indy0,N2),
 2479  rb_lookup((Indx0,Indx),V,RBN),
 2480  rb_lookup((Indy0,Indy),V2,RBN),
 2481  member(R,V),
 2482  member(R,V2),
 2483  get_abox(Tab,ABox),
 2484  same_label(Indx,Indy0,ABox),
 2485  same_label(Indx0,Indy,ABox),
 2486  all_node_blockable(Indx0,Indy0,Tab),!.
 2487
 2488%check_block2([],_).
 2489
 2490check_block2([H|Tail],Tab):-
 2491  blocked(H,Tab),
 2492  check_block2(Tail,Tab).
 2493
 2494%---------------
 2495indirectly_blocked(Ind,Tab):-
 2496  get_tabs(Tab,(T,_RBN,_RBR)),
 2497  transpose_ugraph(T,T1),
 2498  neighbours(Ind,T1,N),
 2499  member(A,N),
 2500  blocked(A,Tab),!.
 2501
 2502%---------------------
 2503/*
 2504  An R-neighbour y of a node x is safe if
 2505  (i)  x is blockable or
 2506  (ii) x is a nominal node and y is not blocked.
 2507*/
 2508
 2509safe(Ind,R,Tab):-
 2510  get_tabs(Tab,(_,_,RBR)),
 2511  rb_lookup(R,V,RBR),
 2512  get_parent(X,Ind,V),
 2513  blockable(X,Tab),!.
 2514
 2515safe(Ind,R,Tab):-
 2516  get_tabs(Tab,(_,_,RBR)),
 2517  rb_lookup(R,V,RBR),
 2518  get_parent(X,Ind,V),
 2519  nominal(X,Tab),!,
 2520  \+ blocked(Ind,Tab).
 2521
 2522get_parent(X,Ind,[(X,Ind)|_T]):-!.
 2523
 2524get_parent(X,Ind,[(X,LI)|_T]):-
 2525  is_list(LI),
 2526  member(Ind,LI),!.
 2527
 2528get_parent(X,Ind,[_|T]):-
 2529  get_parent(X,Ind,T).
 2530
 2531
 2532/* ***** */
 2533
 2534/*
 2535 writel
 2536 write a list one element at each line
 2537 ==========
 2538*/
 2539writel([]):-!.
 2540
 2541writel([T|C]):-
 2542  write(T),nl,
 2543  writel(C).
 2544
 2545/*
 2546 writeABox
 2547 ==========
 2548*/
 2549writeABox(Tab):-
 2550  get_abox(Tab,ABox),
 2551  writel(ABox).
 2552
 2553
 2554/*
 2555  build_abox
 2556  ===============
 2557*/
 2558
 2559add_owlThing_ind(M,Tab0,Ind,Tab):-
 2560  prepare_nom_list(M,[Ind],NomListOut),
 2561  add_all_to_tableau(M,NomListOut,Tab0,Tab).
 2562
 2563add_owlThing_list(M,Tab0,Tab):- % TODO
 2564  get_tabs(Tab0,(T,_,_)),
 2565  vertices(T,NomListIn),
 2566  prepare_nom_list(M,NomListIn,NomListOut),
 2567  add_all_to_tableau(M,NomListOut,Tab0,Tab).
 2568
 2569%--------------
 2570
 2571prepare_nom_list(_,[],[]):-!.
 2572
 2573prepare_nom_list(M,[literal(_)|T],T1):-!,
 2574  prepare_nom_list(M,T,T1).
 2575
 2576prepare_nom_list(M,[H|T],[(classAssertion('http://www.w3.org/2002/07/owl#Thing',H),Expl)|T1]):-!,
 2577  initial_expl(M,Expl),
 2578  prepare_nom_list(M,T,T1).
 2579%--------------
 2580
 2581
 2582/* merge nodes in (ABox,Tabs) */
 2583
 2584merge_all_individuals(_,[],Tab,Tab):-!.
 2585
 2586merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):-
 2587  get_abox(Tab0,ABox0),
 2588  find_same(H,ABox0,L,ExplL),
 2589  dif(L,[]),!,
 2590  merge_all1(M,H,Expl,L,Tab0,Tab1),
 2591  flatten([H,L],HL0),
 2592  sort(HL0,HL),
 2593  list_as_sameIndividual(HL,SI), %TODO
 2594  %flatten([H,L],L0),
 2595  %sort(L0,SI),
 2596  and_f(M,Expl,ExplL,ExplT),
 2597  add_to_tableau(Tab1,(SI,ExplT),Tab2),
 2598  remove_from_tableau(Tab2,(sameIndividual(L),ExplL),Tab3),
 2599  retract_sameIndividual(L),
 2600  merge_all_individuals(M,T,Tab3,Tab).
 2601
 2602merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):-
 2603  %get_abox(Tab0,ABox0),
 2604  %find_same(H,ABox0,L,_),
 2605  %L==[],!,
 2606  merge_all2(M,H,Expl,Tab0,Tab1),
 2607  add_to_tableau(Tab1,(sameIndividual(H),Expl),Tab2),
 2608  merge_all_individuals(M,T,Tab2,Tab).
 2609
 2610merge_all1(_M,[],_,_,Tab,Tab).
 2611
 2612merge_all1(M,[H|T],Expl,L,Tab0,Tab):-
 2613  \+ member(H,L),
 2614  merge(M,H,L,Expl,Tab0,Tab1),
 2615  merge_all1(M,T,Expl,[H|L],Tab1,Tab).
 2616
 2617merge_all1(M,[H|T],Expl,L,Tab0,Tab):-
 2618  member(H,L),
 2619  merge_all1(M,T,Expl,L,Tab0,Tab).
 2620
 2621
 2622
 2623merge_all2(M,[X,Y|T],Expl,Tab0,Tab):-
 2624  merge(M,X,Y,Expl,Tab0,Tab1),
 2625  merge_all1(M,T,Expl,[X,Y],Tab1,Tab).
 2626
 2627
 2628
 2629/*
 2630  creation of the query anon individual
 2631
 2632*/
 2633query_ind(trillan(0)).
 2634
 2635/*
 2636  creation of a new individual
 2637
 2638*/
 2639new_ind(M,trillan(I)):-
 2640  retract(M:trillan_idx(I)),
 2641  I1 is I+1,
 2642  assert(M:trillan_idx(I1)).
 2643
 2644/*
 2645  same label for two individuals
 2646
 2647*/
 2648
 2649same_label(X,Y,ABox):-
 2650  \+ different_label(X,Y,ABox),
 2651  !.
 2652
 2653/*
 2654  different label in two individuals
 2655
 2656*/
 2657
 2658different_label(X,Y,ABox):-
 2659  findClassAssertion(C,X,_,ABox),
 2660  \+ findClassAssertion(C,Y,_,ABox).
 2661
 2662different_label(X,Y,ABox):-
 2663  findClassAssertion(C,Y,_,ABox),
 2664  \+ findClassAssertion(C,X,_,ABox).
 2665
 2666
 2667/*
 2668  all nodes in path from X to Y are blockable?
 2669
 2670*/
 2671
 2672all_node_blockable(X,Y,Tab):-
 2673  get_tabs(Tab,(T,_,_)),
 2674  graph_min_path(X,Y,T,P),
 2675  all_node_blockable1(P,Tab).
 2676
 2677all_node_blockable1([],_).
 2678
 2679all_node_blockable1([H|Tail],Tab):-
 2680  blockable(H,Tab),
 2681  all_node_blockable1(Tail,Tab).
 2682
 2683/*
 2684  find a path in the graph
 2685  returns only one of the shortest path (if there are 2 paths that have same length, it returns only one of them)
 2686*/
 2687/*
 2688% It may enter in infinite loop when there is a loop in the graph
 2689graph_min_path(X,Y,T,P):-
 2690  findall(Path, graph_min_path1(X,Y,T,Path), Ps),
 2691  min_length(Ps,P).
 2692
 2693graph_min_path1(X,Y,T,[X,Y]):-
 2694  member(X-L,T),
 2695  member(Y,L).
 2696
 2697graph_min_path1(X,Y,T,[X|P]):-
 2698  member(X-L,T),
 2699  member(Z,L),
 2700  graph_min_path1(Z,Y,T,P).
 2701
 2702min_length([H],H).
 2703
 2704min_length([H|T],MP):-
 2705  min_length(T,P),
 2706  length(H,N),
 2707  length(P,NP),
 2708  (N<NP ->
 2709     MP= H
 2710   ;
 2711     MP= P).
 2712*/
 2713
 2714graph_min_path(X,Y,T,P):-
 2715  edges(T, Es),
 2716  aggregate_all(min(Length,Path),graph_min_path1(X,Y,Es,Length,Path),min(_L,P)).
 2717
 2718
 2719graph_min_path1(X, Y, Es, N, Path) :- 
 2720  graph_min_path1_int(X, Y, Es, [], Path),
 2721  length(Path, N).
 2722
 2723graph_min_path1_int(X, Y, Es, Seen, [X]) :-
 2724  \+ memberchk(X, Seen),
 2725  member(X-Y, Es).
 2726graph_min_path1_int(X, Z, Es, Seen, [X|T]) :-
 2727  \+ memberchk(X, Seen),
 2728  member(X-Y, Es),
 2729  graph_min_path1_int(Y, Z, Es, [X|Seen], T),
 2730  \+ memberchk(X, T).
 2731
 2732/*
 2733 find all ancestor of a node
 2734
 2735*/
 2736ancestor(Ind,T,AN):-
 2737  transpose_ugraph(T,T1),
 2738  findall(Y,connection(Ind,T1,Y),AN).
 2739  %ancestor1([Ind],T1,[],AN).
 2740
 2741ancestor_nt(Ind,TT,AN):-
 2742  findall(Y,connection(Ind,TT,Y),AN).
 2743
 2744ancestor1([],_,A,A).
 2745
 2746ancestor1([Ind|Tail],T,A,AN):-
 2747  neighbours(Ind,T,AT),
 2748  add_all_n(AT,Tail,Tail1),
 2749  add_all_n(A,AT,A1),
 2750  ancestor1(Tail1,T,A1,AN).
 2751
 2752:- table connection/3. 2753connection(X, T, Y) :-
 2754  neighbours(X,T,AT),
 2755  member(Y,AT).
 2756
 2757connection(X, T, Y) :-
 2758  connection(X, T, Z),
 2759  connection(Z, T, Y).
 2760
 2761
 2762%-----------------
 2763/*
 2764
 2765 add_all_n(L1,L2,LO)
 2766 add in L2 all item of L1 without duplicates
 2767
 2768*/
 2769
 2770add_all_n([],A,A).
 2771
 2772add_all_n([H|T],A,AN):-
 2773  \+ member(H,A),
 2774  add_all_n(T,[H|A],AN).
 2775
 2776add_all_n([H|T],A,AN):-
 2777  member(H,A),
 2778  add_all_n(T,A,AN).
 2779/* *************** */
 2780
 2781
 2782
 2783/*
 2784  find all S neighbours (S is a role)
 2785*/
 2786s_neighbours(M,Ind1,S,Tab,SN):- %gtrace,
 2787  get_tabs(Tab,(_,_,RBR)),
 2788  rb_lookup(S,VN,RBR),!,
 2789  s_neighbours1(Ind1,VN,SN0),
 2790  flatten(SN0,SN1),
 2791  get_abox(Tab,ABox),
 2792  s_neighbours2(M,SN1,SN1,SN,ABox),!.
 2793
 2794s_neighbours(_,_Ind1,_S,_Tab,[]). % :-
 2795%  get_tabs(Tab,(_,_,RBR)),
 2796%  \+ rb_lookup(S,_VN,RBR).
 2797
 2798s_neighbours1(_,[],[]).
 2799
 2800s_neighbours1(Ind1,[(Ind1,Y)|T],[Y|T1]):-
 2801  s_neighbours1(Ind1,T,T1).
 2802
 2803s_neighbours1(Ind1,[(X,_Y)|T],T1):-
 2804  dif(X,Ind1),
 2805  s_neighbours1(Ind1,T,T1).
 2806  
 2807s_neighbours2(_,_,[],[],_).
 2808
 2809s_neighbours2(M,SN,[H|T],[H|T1],ABox):-
 2810  s_neighbours2(M,SN,T,T1,ABox),
 2811  not_same_ind(M,T1,H,ABox),!.
 2812
 2813s_neighbours2(M,SN,[_H|T],T1,ABox):-
 2814  s_neighbours2(M,SN,T,T1,ABox).
 2815  %same_ind(M,T1,H,ABox).
 2816
 2817
 2818%-----------------
 2819
 2820not_same_ind(M,SN,H,_ABox):-
 2821  M:differentIndividuals(SI),
 2822  member(H,SI),
 2823  member(H2,SI),
 2824  member(H2,SN),
 2825  dif(H,H2),!.
 2826
 2827not_same_ind(_,SN,H,ABox):-
 2828  find((differentIndividuals(SI),_),ABox),
 2829  member(H,SI),
 2830  member(H2,SI),
 2831  member(H2,SN),
 2832  dif(H,H2),!.
 2833
 2834not_same_ind(M,SN,H,ABox):-
 2835  \+ same_ind(M,SN,H,ABox),!.
 2836
 2837same_ind(M,SN,H,_ABox):-
 2838  M:sameIndividual(SI),
 2839  member(H,SI),
 2840  member(H2,SI),
 2841  member(H2,SN),
 2842  dif(H,H2).
 2843
 2844same_ind(_,SN,H,ABox):-
 2845  find((sameIndividual(SI),_),ABox),
 2846  member(H,SI),
 2847  member(H2,SI),
 2848  member(H2,SN),
 2849  dif(H,H2).
 2850
 2851/* ************* */
 2852
 2853/*
 2854 s_predecessors
 2855 ==============
 2856 find all S-predecessor of Ind
 2857*/
 2858
 2859s_predecessors(M,Ind1,S,Tab,SN):-
 2860  get_tabs(Tab,(_,_,RBR)),
 2861  rb_lookup(S,VN,RBR),
 2862  s_predecessors1(Ind1,VN,SN1),
 2863  get_abox(Tab,ABox),
 2864  s_predecessors2(M,SN1,SN,ABox).
 2865
 2866s_predecessors(_M,_Ind1,S,(_ABox,(_,_,RBR)),[]):-
 2867  \+ rb_lookup(S,_VN,RBR).
 2868
 2869s_predecessors1(_,[],[]).
 2870
 2871s_predecessors1(Ind1,[(Y,Ind1)|T],[Y|T1]):-
 2872  s_predecessors1(Ind1,T,T1).
 2873
 2874s_predecessors1(Ind1,[(_X,Y)|T],T1):-
 2875  dif(Y,Ind1),
 2876  s_predecessors1(Ind1,T,T1).
 2877
 2878s_predecessors2(_M,[],[],_).
 2879
 2880s_predecessors2(M,[H|T],[H|T1],ABox):-
 2881  s_predecessors2(M,T,T1,ABox),
 2882  \+ same_ind(M,T1,H,ABox).
 2883
 2884s_predecessors2(M,[H|T],T1,ABox):-
 2885  s_predecessors2(M,T,T1,ABox),
 2886  same_ind(M,T1,H,ABox).
 2887
 2888/* ********** */
 2889
 2890/* *************
 2891   
 2892Probability computation
 2893   Old version
 2894
 2895   ************* */
 2896
 2897/*
 2898build_formula([],[],Var,Var).
 2899
 2900build_formula([D|TD],TF,VarIn,VarOut):-
 2901        build_term(D,[],[],VarIn,Var1),!,
 2902        build_formula(TD,TF,Var1,VarOut).
 2903
 2904build_formula([D|TD],[F|TF],VarIn,VarOut):-
 2905        build_term(D,[],F,VarIn,Var1),
 2906        build_formula(TD,TF,Var1,VarOut).
 2907
 2908build_term([],F,F,Var,Var).
 2909
 2910build_term([(Ax,S)|TC],F0,F,VarIn,VarOut):-!,
 2911  (p_x(Ax,_)->
 2912    (nth0_eq(0,NVar,VarIn,(Ax,S))->
 2913      Var1=VarIn
 2914    ;
 2915      append(VarIn,[(Ax,S)],Var1),
 2916      length(VarIn,NVar)
 2917    ),
 2918    build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2919  ;
 2920    (p(Ax,_)->
 2921      (nth0_eq(0,NVar,VarIn,(Ax,[]))->
 2922        Var1=VarIn
 2923      ;
 2924        append(VarIn,[(Ax,[])],Var1),
 2925        length(VarIn,NVar)
 2926      ),
 2927      build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2928    ;
 2929      build_term(TC,F0,F,VarIn,VarOut)
 2930    )
 2931  ).
 2932
 2933build_term([Ax|TC],F0,F,VarIn,VarOut):-!,
 2934  (p(Ax,_)->
 2935    (nth0_eq(0,NVar,VarIn,(Ax,[]))->
 2936      Var1=VarIn
 2937    ;
 2938      append(VarIn,[(Ax,[])],Var1),
 2939      length(VarIn,NVar)
 2940    ),
 2941    build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2942  ;
 2943    build_term(TC,F0,F,VarIn,VarOut)
 2944  ).
 2945*/
 2946
 2947/* nth0_eq(PosIn,PosOut,List,El) takes as input a List,
 2948an element El and an initial position PosIn and returns in PosOut
 2949the position in the List that contains an element exactly equal to El
 2950*/
 2951
 2952/*
 2953nth0_eq(N,N,[H|_T],El):-
 2954        H==El,!.
 2955
 2956nth0_eq(NIn,NOut,[_H|T],El):-
 2957        N1 is NIn+1,
 2958        nth0_eq(N1,NOut,T,El).
 2959
 2960*/
 2961/* var2numbers converts a list of couples (Rule,Substitution) into a list
 2962of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer
 2963starting from 0 */
 2964/*
 2965var2numbers([],_N,[]).
 2966
 2967var2numbers([(R,_S)|T],N,[[N,2,[Prob,Prob1,0.3,0.7]]|TNV]):-
 2968        (p(R,_);p_x(R,_)),
 2969        compute_prob_ax(R,Prob),!,
 2970        Prob1 is 1-Prob,
 2971        N1 is N+1,
 2972        var2numbers(T,N1,TNV).
 2973
 2974
 2975compute_prob_ax(R,Prob):-
 2976  findall(P, p(R,P),Probs),
 2977  compute_prob_ax1(Probs,Prob).
 2978
 2979compute_prob_ax1([Prob],Prob):-!.
 2980
 2981compute_prob_ax1([Prob1,Prob2],Prob):-!,
 2982  Prob is Prob1+Prob2-(Prob1*Prob2).
 2983
 2984compute_prob_ax1([Prob1 | T],Prob):-
 2985  compute_prob_ax1(T,Prob0),
 2986  Prob is Prob1 + Prob0 - (Prob1*Prob0).
 2987
 2988*/
 2989
 2990/**********************
 2991
 2992 Probability Computation
 2993
 2994***********************/
 2995
 2996:- thread_local
 2997	%get_var_n/5,
 2998        rule_n/1,
 2999        na/2,
 3000        v/3. 3001
 3002%rule_n(0).
 3003
 3004compute_prob(M,Explanations,Prob):-
 3005  retractall(v(_,_,_)),
 3006  retractall(na(_,_)),
 3007  retractall(rule_n(_)),
 3008  assert(rule_n(0)),
 3009  %findall(1,M:annotationAssertion('http://ml.unife.it/disponte#probability',_,_),NAnnAss),length(NAnnAss,NV),
 3010  get_bdd_environment(M,Env),
 3011  build_bdd(M,Env,Explanations,BDD),
 3012  ret_prob(Env,BDD,Prob),
 3013  clean_environment(M,Env), !.
 3014
 3015compute_prob_single_explanation(M,Expl,Prob):-
 3016  ret_prob(M,Expl,1.0,Prob).
 3017
 3018ret_prob(_,[],Prob,Prob):-!.
 3019
 3020ret_prob(M,[Ax|T],Prob0,Prob):-
 3021  compute_prob_ax(M,Ax,Prob1),!,
 3022  Prob2 is Prob0 * Prob1,
 3023  ret_prob(M,T,Prob2,Prob).
 3024
 3025ret_prob(M,[_|T],Prob0,Prob):-
 3026  ret_prob(M,T,Prob0,Prob).
 3027
 3028
 3029get_var_n(Env,R,S,Probs,V):-
 3030  (
 3031    v(R,S,V) ->
 3032      true
 3033    ;
 3034      %length(Probs,L),
 3035      add_var(Env,Probs,R,V),
 3036      assert(v(R,S,V))
 3037  ).
 3038
 3039
 3040get_prob_ax(M,(Ax,_Ind),N,Prob):- !,
 3041  compute_prob_ax(M,Ax,Prob),
 3042  ( na(Ax,N) ->
 3043      true
 3044    ;
 3045      rule_n(N),
 3046      assert(na(Ax,N)),
 3047      retract(rule_n(N)),
 3048      N1 is N + 1,
 3049      assert(rule_n(N1))
 3050  ).
 3051
 3052get_prob_ax(M,Ax,N,Prob):- !,
 3053  compute_prob_ax(M,Ax,Prob),
 3054  ( na(Ax,N) ->
 3055      true
 3056    ;
 3057      rule_n(N),
 3058      assert(na(Ax,N)),
 3059      retract(rule_n(N)),
 3060      N1 is N + 1,
 3061      assert(rule_n(N1))
 3062  ).
 3063
 3064
 3065/*
 3066prob_number(ProbAT,ProbA):-
 3067  atom_number(ProbAT,ProbAC),
 3068  ProbAC==1,!,
 3069  Epsilon is 10**(-10),
 3070  ProbA is ProbAC - Epsilon.
 3071
 3072prob_number(ProbAT,ProbA):-
 3073  atom_number(ProbAT,ProbAC),
 3074  ProbAC==1.0,!,
 3075  Epsilon is 10**(-10),
 3076  ProbA is ProbAC - Epsilon.
 3077*/
 3078
 3079prob_number(ProbAT,ProbA):-
 3080  atom_number(ProbAT,ProbA).
 3081
 3082compute_prob_ax(M,Ax,Prob):-%gtrace,
 3083  findall(ProbA,(disponte_iri(DisponteIri),M:annotationAssertion(DisponteIri,Ax,literal(ProbAT)),prob_number(ProbAT,ProbA)),Probs),
 3084  compute_prob_ax1(Probs,Prob).
 3085
 3086compute_prob_ax1([Prob],Prob):-!.
 3087
 3088compute_prob_ax1([Prob1,Prob2],Prob):-!,
 3089  Prob is Prob1+Prob2-(Prob1*Prob2).
 3090
 3091compute_prob_ax1([Prob1 | T],Prob):-
 3092  compute_prob_ax1(T,Prob0),
 3093  Prob is Prob1 + Prob0 - (Prob1*Prob0).
 3094
 3095/************************/
 3096
 3097unload_all_algorithms :-
 3098  unload_file(library(trill_internal)),
 3099  unload_file(library(trillp_internal)),
 3100  unload_file(library(tornado_internal)).
 3101
 3102set_algorithm(M:trill):-
 3103  unload_all_algorithms,
 3104  consult(library(trill_internal)),
 3105  clean_up(M),!.
 3106
 3107set_algorithm(M:trillp):-
 3108  unload_all_algorithms,
 3109  consult(library(trillp_internal)),
 3110  clean_up(M),!.
 3111
 3112set_algorithm(M:tornado):-
 3113  unload_all_algorithms,
 3114  consult(library(tornado_internal)),
 3115  clean_up(M),!.