trill

This module performs reasoning over probabilistic description logic knowledge bases. It reads probabilistic knowledge bases in RDF format or in Prolog format, a functional-like sintax based on definitions of Thea library, and answers queries by finding the set of explanations or computing the probability.

[1] http://vangelisv.github.io/thea/

See https://github.com/rzese/trill/blob/master/doc/manual.pdf or http://ds.ing.unife.it/~rzese/software/trill/manual.html for details.

author
- Riccardo Zese
version
- 6.0.2
license
- Artistic License 2.0
   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                 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,
   26                 load_kb/1, load_owl_kb/1, load_owl_kb_from_string/1, init_trill/1,
   27                 set_tableau_expansion_rules/2] ).   28
   29:- meta_predicate sub_class(:,+).   30:- meta_predicate sub_class(:,+,-).   31:- meta_predicate sub_class(:,+,-,+).   32:- meta_predicate all_sub_class(:,+,-).   33:- meta_predicate prob_sub_class(:,+,-).   34:- meta_predicate instanceOf(:,+).   35:- meta_predicate instanceOf(:,+,-).   36:- meta_predicate instanceOf(:,+,-,+).   37:- meta_predicate all_instanceOf(:,+,-).   38:- meta_predicate prob_instanceOf(:,+,-).   39:- meta_predicate property_value(:,+,+).   40:- meta_predicate property_value(:,+,+,-).   41:- meta_predicate property_value(:,+,+,-,+).   42:- meta_predicate all_property_value(:,+,+,-).   43:- meta_predicate prob_property_value(:,+,+,-).   44:- meta_predicate unsat(:).   45:- meta_predicate unsat(:,-).   46:- meta_predicate unsat(:,-,+).   47:- meta_predicate all_unsat(:,-).   48:- meta_predicate prob_unsat(:,-).   49:- meta_predicate inconsistent_theory(:).   50:- meta_predicate inconsistent_theory(:,+).   51:- meta_predicate all_inconsistent_theory(:).   52:- meta_predicate prob_inconsistent_theory(:).   53:- meta_predicate axiom(:).   54:- meta_predicate kb_prefixes(:).   55:- meta_predicate add_kb_prefix(:,+).   56:- meta_predicate add_kb_prefixes(:).   57:- meta_predicate add_axiom(:).   58:- meta_predicate add_axioms(:).   59:- meta_predicate remove_kb_prefix(:,+).   60:- meta_predicate remove_kb_prefix(:).   61:- meta_predicate remove_axiom(:).   62:- meta_predicate remove_axioms(:).   63:- meta_predicate load_kb(+).   64:- meta_predicate load_owl_kb(+).   65:- meta_predicate load_owl_kb_from_string(+).   66:- meta_predicate set_algorithm(:).   67:- meta_predicate init_trill(+).   68:- meta_predicate set_tableau_expansion_rules(:,+).   69
   70:- use_module(library(lists)).   71:- use_module(library(ugraphs)).   72:- use_module(library(rbtrees)).   73:- use_module(library(dif)).   74:- use_module(library(pengines)).   75:- use_module(library(sandbox)).   76:- use_module(library(aggregate)).   77
   78:- reexport(library(bddem)).   79
   80:- style_check(-discontiguous).   81
   82%:- table ancestor1/4.
   83:- table blocked/2.   84
   85/********************************
   86  SETTINGS
   87*********************************/
   88:- multifile setting_trill_default/2.   89
   90/********************************
   91  LOAD KNOWLEDGE BASE
   92*********************************/
 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. /
  100load_kb(FileName):-
  101  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. /
  109load_owl_kb(FileName):-
  110  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. /
  118load_owl_kb_from_string(String):-
  119  load_owl_from_string(String).
  120
  121/*****************************/
  122
  123/*****************************
  124  UTILITY PREDICATES
  125******************************/
  126%defined in utility_translation
  127:- multifile add_kb_prefix/2, add_kb_prefixes/1, add_axiom/1, add_axioms/1,
  128             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. /
  191:- multifile axiom/1.  192/*axiom(M:Axiom):-
  193  M:ns4query(NSList),
  194  expand_all_ns(M,[Axiom],NSList,[AxiomEx]),
  195  M:axiom(AxiomEx).*/
  196
  197:- 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. /
  205set_tableau_expansion_rules(M:DetRules,NondetRules):-
  206  retractall(M:setting_trill(det_rules,_)),
  207  retractall(M:setting_trill(nondet_rules,_)),
  208  assert(M:setting_trill(det_rules,DetRules)),
  209  assert(M:setting_trill(nondet_rules,NondetRules)).
  210
  211/*****************************
  212  MESSAGES
  213******************************/
  214:- multifile prolog:message/1.  215
  216prolog:message(iri_not_exists(IRIs)) -->
  217  [ 'IRIs not existent or wrong argument: ~w' -[IRIs] ].
  218
  219prolog:message(inconsistent) -->
  220  [ 'Inconsistent ABox' ].
  221
  222prolog:message(consistent) -->
  223  [ 'Consistent ABox' ].
  224
  225prolog:message(wrong_number_max_expl) -->
  226  [ 'max_expl option can take integer values or "all"' ].
  227
  228prolog:message(timeout_reached) -->
  229  [ 'Timeout reached' ].
  230
  231/*****************************
  232  QUERY OPTIONS
  233******************************/
 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:

*/

  247query_option(OptList,Option,Value):-
  248  Opt=..[Option,Value],
  249  memberchk(Opt,OptList).
  250
  251/****************************
  252  QUERY PREDICATES
  253*****************************/
  254
  255execute_query(M,QueryType,QueryArgsNC,Expl,QueryOptions):-
  256  check_query_args(M,QueryType,QueryArgsNC,QueryArgs,QueryArgsNotPresent),
  257  ( dif(QueryArgsNotPresent,[]) ->
  258    (print_message(warning,iri_not_exists(QueryArgsNotPresent)),!,false) ; true
  259  ),
  260  set_up_reasoner(M),
  261  find_explanations(M,QueryType,QueryArgs,Expl,QueryOptions),
  262  ( query_option(QueryOptions,return_prob,Prob) ->
  263    (
  264      compute_prob_and_close(M,Expl,Prob),
  265      (query_option(QueryOptions,return_single_prob,false) -> true ; !)
  266    ) ; true
  267  ).
  268
  269
  270% Execution monitor
  271find_explanations(M,QueryType,QueryArgs,Expl,QueryOptions):-
  272  % TODO call_with_time_limit
  273  ( query_option(QueryOptions,assert_abox,AssertABox) -> Opt=[assert_abox(AssertABox)] ; Opt=[]),
  274  ( query_option(QueryOptions,max_expl,N) -> 
  275    MonitorNExpl = N
  276    ; 
  277    ( ( query_option(QueryOptions,return_prob,_) -> MonitorNExpl=all ; MonitorNExpl=bt) ) % if return_prob is present and no max_expl force to find all the explanations
  278  ),
  279  ( query_option(QueryOptions,time_limit,MonitorTimeLimit) ->
  280    find_n_explanations_time_limit(M,QueryType,QueryArgs,Expl,MonitorNExpl,MonitorTimeLimit,Opt)
  281    ;
  282    find_n_explanations(M,QueryType,QueryArgs,Expl,MonitorNExpl,Opt)
  283  ).
  284
  285find_n_explanations_time_limit(M,QueryType,QueryArgs,Expl,MonitorNExpl,MonitorTimeLimit,Opt):-
  286  retractall(M:setting_trill(timeout,_)),
  287  get_time(Start),
  288  Timeout is Start + MonitorTimeLimit,
  289  assert(M:setting_trill(timeout,Timeout)),
  290  find_n_explanations(M,QueryType,QueryArgs,Expl,MonitorNExpl,Opt),
  291  get_time(End),
  292  (End<Timeout -> true ; print_message(warning,timeout_reached)).
  293
  294
  295
  296find_single_explanation(M,QueryType,QueryArgs,Expl,Opt):-
  297  build_abox(M,Tableau,QueryType,QueryArgs), % will expand the KB without the query
  298  (absence_of_clashes(Tableau) ->  % TODO if QueryType is inconsistent no check
  299    (
  300      add_q(M,QueryType,Tableau,QueryArgs,Tableau0),
  301      set_up_tableau(M),
  302      findall(Tableau1,expand_queue(M,Tableau0,Tableau1),L),
  303      (query_option(Opt,assert_abox,true) -> (writeln('Asserting ABox...'), M:assert(final_abox(L)), writeln('Done. Asserted in final_abox/1...')) ; true),
  304      find_expls(M,L,QueryArgs,Expl1),
  305      check_and_close(M,Expl1,Expl)
  306    )
  307  ;
  308    print_message(warning,inconsistent),!,false
  309  ).
  310
  311/*************
  312 
  313  Monitor predicates
  314
  315**************/
  316
  317check_time_monitor(M):-
  318  M:setting_trill(timeout,Timeout),!,
  319  get_time(Now),
  320  Timeout<Now. % I must stop
  321
  322/* *************** */
  323
  324set_up_reasoner(M):-
  325  set_up(M),
  326  retractall(M:exp_found(_,_)),
  327  retractall(M:exp_found(_,_,_)),
  328  retractall(M:trillan_idx(_)),
  329  assert(M:trillan_idx(1)).
  330
  331set_up_tableau(M):-
  332  % TO CHANGE move to KB loading
  333  %setting_trill_default(det_rules,DetRules),
  334  %setting_trill_default(nondet_rules,NondetRules),
  335  %set_tableau_expansion_rules(M:DetRules,NondetRules). 
  336  prune_tableau_rules(M).
  337
  338% instanceOf
  339add_q(M,io,Tableau0,[ClassEx,IndEx],Tableau):- !,
  340  neg_class(ClassEx,NClassEx),
  341  add_q(M,Tableau0,classAssertion(NClassEx,IndEx),Tableau1),
  342  add_clash_to_tableau(M,Tableau1,NClassEx-IndEx,Tableau2),
  343  update_expansion_queue_in_tableau(M,NClassEx,IndEx,Tableau2,Tableau).
  344
  345% property_value
  346add_q(M,pv,Tableau0,[PropEx,Ind1Ex,Ind2Ex],Tableau):-!,
  347  neg_class(PropEx,NPropEx), %use of neg_class to negate property
  348  add_q(M,Tableau0,propertyAssertion(NPropEx,Ind1Ex,Ind2Ex),Tableau1),
  349  add_clash_to_tableau(M,Tableau1,NPropEx-Ind1Ex-Ind2Ex,Tableau2),
  350  update_expansion_queue_in_tableau(M,NPropEx,Ind1Ex,Ind2Ex,Tableau2,Tableau).
  351
  352
  353% sub_class
  354add_q(M,sc,Tableau0,[SubClassEx,SupClassEx],Tableau):- !,
  355  neg_class(SupClassEx,NSupClassEx),
  356  query_ind(QInd),
  357  add_q(M,Tableau0,classAssertion(intersectionOf([SubClassEx,NSupClassEx]),QInd),Tableau1),
  358  utility_translation:add_kb_atoms(M,class,[intersectionOf([SubClassEx,NSupClassEx])]), % This is necessary to correctly prune expansion rules
  359  add_owlThing_ind(M,Tableau1,QInd,Tableau2),
  360  add_clash_to_tableau(M,Tableau2,intersectionOf([SubClassEx,NSupClassEx])-QInd,Tableau3),
  361  update_expansion_queue_in_tableau(M,intersectionOf([SubClassEx,NSupClassEx]),QInd,Tableau3,Tableau).
  362
  363% unsat
  364add_q(M,un,Tableau0,['unsat',ClassEx],Tableau):- !,
  365  query_ind(QInd),
  366  add_q(M,Tableau0,classAssertion(ClassEx,QInd),Tableau1),
  367  add_owlThing_ind(M,Tableau1,QInd,Tableau2),
  368  add_clash_to_tableau(M,Tableau2,ClassEx-QInd,Tableau3),
  369  update_expansion_queue_in_tableau(M,ClassEx,QInd,Tableau3,Tableau).
  370
  371% inconsistent_theory
  372add_q(_,it,Tableau,['inconsistent','kb'],Tableau):- !. % Do nothing
  373
  374/*
  375  Auxiliary predicates to extract the det of individuals connected to the query
  376*/
  377
  378% Find the individuals directly connected to the given one
  379gather_connected_individuals(M,Ind,ConnectedInds):-
  380  find_successors(M,Ind,SuccInds),
  381  find_predecessors(M,Ind,PredInds),
  382  append(SuccInds,PredInds,ConnectedInds).
  383
  384find_successors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,Ind,ConnectedInd)), List).
  385find_predecessors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,ConnectedInd,Ind)), List).
  386
  387intersect([H|_], List) :- member(H, List), !.
  388intersect([_|T], List) :- intersect(T, List).
  389
  390% Recursively gather all the connected individuals, i.e., isolate the relevant fragment of the KB.
  391%scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet).
  392scan_connected_individuals(_,[],_,IndividualsSet0,IndividualsSet):-
  393  sort(IndividualsSet0,IndividualsSet).
  394
  395scan_connected_individuals(M,[H|IndividualsToCheck],IndividualsChecked,IndividualsSet0,IndividualsSet):-
  396  memberchk(H,IndividualsChecked),!,
  397  scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet).
  398
  399
  400scan_connected_individuals(M,[H|IndividualsToCheck0],IndividualsChecked,IndividualsSet0,IndividualsSet):-
  401  gather_connected_individuals(M,H,NewIndividualsToCheck),
  402  append(IndividualsSet0,NewIndividualsToCheck,IndividualsSet1),
  403  append(IndividualsToCheck0,NewIndividualsToCheck,IndividualsToCheck),
  404  scan_connected_individuals(M,IndividualsToCheck,[H|IndividualsChecked],IndividualsSet1,IndividualsSet).
  405
  406
  407% Builds the list of individuals conneted given the query type
  408collect_individuals(M,io,[_,IndEx],IndividualsSet):-
  409  scan_connected_individuals(M,[IndEx],[],[IndEx],IndividualsSet).
  410
  411collect_individuals(M,pv,[_,Ind1Ex,Ind2Ex],IndividualsSet):-
  412  scan_connected_individuals(M,[Ind1Ex,Ind2Ex],[],[Ind1Ex,Ind2Ex],IndividualsSet).
  413
  414collect_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.
  415  query_ind(QInd).
  416
  417collect_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.
  418  query_ind(QInd).
  419
  420collect_individuals(_,it,['inconsistent','kb'],[]):-!.
  421
  422/*
  423  check the KB atoms to consider only the necessary expansion rules, pruning the useless ones
  424*/
  425prune_tableau_rules(M):-
  426  M:kb_atom(KBA),
  427  Classes=KBA.class,
  428  setting_trill_default(det_rules,DetRules),
  429  prune_tableau_rules(Classes,DetRules,PrunedDetRules),
  430  setting_trill_default(nondet_rules,NondetRules),
  431  prune_tableau_rules(Classes,NondetRules,PrunedNondetRules),
  432  set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules).
  433
  434add_tableau_rules_from_class(M,someValuesFrom(_,_)):-
  435  M:setting_trill(det_rules,Rules),
  436  memberchk(exists_rule,Rules),!.
  437
  438add_tableau_rules_from_class(M,C):-
  439  M:kb_atom(KBA),
  440  Classes=KBA.class,
  441  setting_trill_default(det_rules,DetRules),
  442  prune_tableau_rules([C|Classes],DetRules,PrunedDetRules),
  443  setting_trill_default(nondet_rules,NondetRules),
  444  prune_tableau_rules([C|Classes],NondetRules,PrunedNondetRules),
  445  set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules).
  446
  447% o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule,or_rule,max_rule,ch_rule
  448prune_tableau_rules(_,[],[]).
  449
  450prune_tableau_rules(KBA,[o_rule|TR],[o_rule|PTR]):-
  451  memberchk(oneOf(_),KBA),!,
  452  prune_tableau_rules(KBA,TR,PTR).
  453
  454prune_tableau_rules(KBA,[and_rule|TR],[and_rule|PTR]):-
  455  memberchk(intersectionOf(_),KBA),!,
  456  prune_tableau_rules(KBA,TR,PTR).
  457
  458prune_tableau_rules(KBA,[unfold_rule|TR],[unfold_rule|PTR]):-
  459  !,
  460  prune_tableau_rules(KBA,TR,PTR).
  461
  462prune_tableau_rules(KBA,[add_exists_rule|TR],[add_exists_rule|PTR]):-
  463  !,
  464  prune_tableau_rules(KBA,TR,PTR).
  465
  466prune_tableau_rules(KBA,[forall_rule|TR],[forall_rule|PTR]):-
  467  memberchk(allValuesFrom(_,_),KBA),!,
  468  prune_tableau_rules(KBA,TR,PTR).
  469
  470prune_tableau_rules(KBA,[forall_plus_rule|TR],[forall_plus_rule|PTR]):-
  471  memberchk(allValuesFrom(_,_),KBA),!,
  472  prune_tableau_rules(KBA,TR,PTR).
  473
  474prune_tableau_rules(KBA,[exists_rule|TR],[exists_rule|PTR]):-
  475  memberchk(someValuesFrom(_,_),KBA),!,
  476  prune_tableau_rules(KBA,TR,PTR).
  477
  478prune_tableau_rules(KBA,[min_rule|TR],[min_rule|PTR]):-
  479  (memberchk(minCardinality(_,_),KBA); memberchk(minCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  480  prune_tableau_rules(KBA,TR,PTR).
  481
  482prune_tableau_rules(KBA,[or_rule|TR],[or_rule|PTR]):-
  483  memberchk(unionOf(_),KBA),!,
  484  prune_tableau_rules(KBA,TR,PTR).
  485
  486prune_tableau_rules(KBA,[max_rule|TR],[max_rule|PTR]):-
  487  (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  488  prune_tableau_rules(KBA,TR,PTR).
  489
  490
  491prune_tableau_rules(KBA,[ch_rule|TR],[ch_rule|PTR]):-
  492  (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!,
  493  prune_tableau_rules(KBA,TR,PTR).
  494
  495prune_tableau_rules(KBA,[_|TR],PTR):-
  496  prune_tableau_rules(KBA,TR,PTR).
  497
  498/***********
  499  Queries
  500  - with and without explanations -
  501 ***********/
 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. */
  512instanceOf(M:Class,Ind,Expl,Opt):-
  513  execute_query(M,io,[Class,Ind],Expl,Opt),
  514  is_expl(M,Expl).
 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. /
  526instanceOf(M:Class,Ind,Expl):-
  527  instanceOf(M:Class,Ind,Expl,[]),
  528  is_expl(M,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. /
  539all_instanceOf(M:Class,Ind,Expl):-
  540  execute_query(M,io,[Class,Ind],Expl,[max_expl(all)]),
  541  is_expl(M,Expl).
 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. /
  550instanceOf(M:Class,Ind):-
  551  execute_query(M,io,[Class,Ind],Expl,[max_expl(1)]),!,
  552  is_expl(M,Expl).
 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 settings for the execution of the query. Settings can be:

/

  566property_value(M:Prop, Ind1, Ind2,Expl,Opt):-
  567  execute_query(M,pv,[Prop, Ind1, Ind2],Expl,Opt),
  568  is_expl(M,Expl).
 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. /
  578property_value(M:Prop, Ind1, Ind2,Expl):-
  579  property_value(M:Prop, Ind1, Ind2,Expl,[]),
  580  is_expl(M,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. /
  590all_property_value(M:Prop, Ind1, Ind2,Expl):-
  591  execute_query(M,pv,[Prop, Ind1, Ind2],Expl,[max_expl(all)]),
  592  is_expl(M,Expl).
 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. /
  600property_value(M:Prop, Ind1, Ind2):-
  601  execute_query(M,pv,[Prop, Ind1, Ind2],Expl,[max_expl(1)]),!,
  602  is_expl(M,Expl).
 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 settings for the execution of the query. Settings can be:

/

  617sub_class(M:Class,SupClass,Expl,Opt):-
  618  execute_query(M,sc,[Class,SupClass],Expl,Opt),
  619  is_expl(M,Expl).
 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. /
  630sub_class(M:Class,SupClass,Expl):-
  631  sub_class(M:Class,SupClass,Expl,[]),
  632  is_expl(M,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. /
  643all_sub_class(M:Class,SupClass,Expl):-
  644  execute_query(M,sc,[Class,SupClass],Expl,[max_expl(all)]),
  645  is_expl(M,Expl).
 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. /
  653sub_class(M:Class,SupClass):-
  654  execute_query(M,sc,[Class,SupClass],Expl,[max_expl(1)]),!,
  655  is_expl(M,Expl).
 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 settings for the execution of the query. Settings can be:

/

  669unsat(M:Concept,Expl,Opt):-
  670  execute_query(M,un,[Concept],Expl,Opt),
  671  is_expl(M,Expl).
 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. /
  681unsat(M:Concept,Expl):-
  682  unsat(M:Concept,Expl,[]),
  683  is_expl(M,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. /
  693all_unsat(M:Concept,Expl):-
  694  execute_query(M,un,[Concept],Expl,[max_expl(all)]),
  695  is_expl(M,Expl).
 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. /
  703unsat(M:Concept):-
  704  execute_query(M,un,[Concept],Expl,[max_expl(1)]),!,
  705  is_expl(M,Expl).
 inconsistent_theory(:Expl:list, ++Opt:list)
This predicate returns one explanation for the inconsistency of the loaded knowledge base. Opt is a list containing settings for the execution of the query. Settings can be:

/

  716inconsistent_theory(M:Expl,Opt):-
  717  execute_query(M,it,[],Expl,Opt),
  718  is_expl(M,Expl).
 inconsistent_theory(:Expl:list)
This predicate returns one explanation for the inconsistency of the loaded knowledge base. /
  725inconsistent_theory(M:Expl):-
  726  inconsistent_theory(M:Expl,[]),
  727  is_expl(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. /
  736all_inconsistent_theory(M:Expl):-
  737  execute_query(M,it,[],Expl,[max_expl(all)]),
  738  is_expl(M,Expl).
 inconsistent_theory
This predicate returns true if the loaded knowledge base is inconsistent, otherwise it fails. /
  745inconsistent_theory:-
  746  get_trill_current_module(M),
  747  execute_query(M,it,[],Expl,[max_expl(1)]),!,
  748  is_expl(M,Expl).
 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. /
  757prob_instanceOf(M:Class,Ind,Prob):-
  758  instanceOf(M:Class,Ind,_,[return_prob(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. /
  766prob_property_value(M:Prop, Ind1, Ind2,Prob):-
  767  property_value(M:Prop, Ind1, Ind2,_,[return_prob(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. /
  776prob_sub_class(M:Class,SupClass,Prob):-
  777  sub_class(M:Class,SupClass,_,[return_prob(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. /
  786prob_unsat(M:Concept,Prob):-
  787  unsat(M:Concept,_,[return_prob(Prob)]).
 prob_inconsistent_theory(:Prob:double) is det
If the knowledge base is inconsistent, this predicate returns the probability of the inconsistency. /
  794prob_inconsistent_theory(M:Prob):-
  795  inconsistent_theory(M:_,[return_prob(Prob)]).
  796
  797/***********
  798  Utilities for queries
  799 ***********/
  800
  801% adds the query into the ABox
  802add_q(M,Tableau0,Query,Tableau):-
  803  query_empty_expl(M,Expl),
  804  add_to_tableau(Tableau0,(Query,Expl),Tableau1),
  805  create_tabs([(Query,Expl)],Tableau1,Tableau).
  806
  807
  808% initialize an empty explanation for the query with the query placeholder 'qp' in teh choicepoint list
  809query_empty_expl(M,Expl):-%gtrace,
  810  empty_expl(M,EExpl),
  811  add_choice_point(M,qp,EExpl,Expl).
  812
  813
  814% expands query arguments using prefixes and checks their existence in the kb
  815% returns the non-present arguments
  816check_query_args(M,QT,QA,QAEx,NotEx):-
  817  from_query_type_to_args_type(QT,AT),
  818  check_query_args_int(M,AT,QA,QAExT,NotEx),!,
  819  ( length(QA,1) -> 
  820    QAEx = ['unsat'|QAExT]
  821    ;
  822    ( length(QA,0) -> QAEx = ['inconsistent','kb'] ; QAEx = QAExT)
  823  ).
  824
  825from_query_type_to_args_type(io,[class,ind]):- !.
  826from_query_type_to_args_type(pv,[prop,ind,ind]):- !.
  827from_query_type_to_args_type(sc,[class,class]):- !.
  828from_query_type_to_args_type(un,[class]):- !.
  829from_query_type_to_args_type(it,[]):- !.
  830
  831check_query_args_int(_,_,[],[],[]).
  832
  833check_query_args_int(M,[ATH|ATT],[H|T],[HEx|TEx],NotEx):-
  834  check_query_args(M,[ATH],[H],[HEx]),!,
  835  check_query_args_int(M,ATT,T,TEx,NotEx).
  836
  837check_query_args_int(M,[_|ATT],[H|T],TEx,[H|NotEx]):-
  838  check_query_args_int(M,ATT,T,TEx,NotEx).
  839
  840% expands query arguments using prefixes and checks their existence in the kb
  841check_query_args(M,AT,L,LEx) :-
  842  M:ns4query(NSList),
  843  expand_all_ns(M,L,NSList,false,LEx), %from utility_translation module
  844  check_query_args_presence(M,AT,LEx).
  845
  846check_query_args_presence(_M,_AT,[]):-!.
  847
  848check_query_args_presence(M,[class|ATT],['http://www.w3.org/2002/07/owl#Thing'|T]) :-
  849  check_query_args_presence(M,ATT,T).
  850
  851check_query_args_presence(M,[AT|ATT],[H|T]) :-
  852  nonvar(H),
  853  atomic(H),!,
  854  find_atom_in_axioms(M,AT,H),%!,
  855  check_query_args_presence(M,ATT,T).
  856
  857check_query_args_presence(M,[AT|ATT],[H|T]) :-
  858  nonvar(H),
  859  \+ atomic(H),!,
  860  H =.. [CE|L],
  861  flatten(L,L1),
  862  from_expression_to_args_type(CE,AT,L1,ATs),
  863  check_query_args_presence(M,ATs,L1),
  864  check_query_args_presence(M,ATT,T).
  865
  866/*
  867check_query_args_presence(M,[_|T]):-
  868  check_query_args_presence(M,T).
  869*/
  870
  871% looks for presence of atoms in kb's axioms
  872find_atom_in_axioms(M,class,H):-
  873  M:kb_atom(L1),
  874  ( member(H,L1.class) ),!.
  875
  876find_atom_in_axioms(M,ind,H):-
  877  M:kb_atom(L1),
  878  ( member(H,L1.individual) ; member(H,L1.datatype) ),!.
  879
  880find_atom_in_axioms(M,prop,H):-
  881  M:kb_atom(L1),
  882  ( member(H,L1.objectProperty) ; member(H,L1.dataProperty) ; member(H,L1.annotationProperty) ),!.
  883
  884find_atom_in_axioms(_,num,H):-
  885  integer(H),!.
  886
  887from_expression_to_args_type(complementOf,class,_,[class]) :- !.
  888from_expression_to_args_type(someValuesFrom,class,_,[prop,class]) :- !.
  889from_expression_to_args_type(allValuesFrom,class,_,[prop,class]) :- !.
  890from_expression_to_args_type(hasValue,class,_,[prop,ind]) :- !.
  891from_expression_to_args_type(hasSelf,class,_,[prop]) :- !.
  892from_expression_to_args_type(minCardinality,class,[_,_,_],[num,prop,class]) :- !.
  893from_expression_to_args_type(minCardinality,class,[_,_],[num,prop]) :- !.
  894from_expression_to_args_type(maxCardinality,class,[_,_,_],[num,prop,class]) :- !.
  895from_expression_to_args_type(maxCardinality,class,[_,_],[num,prop]) :- !.
  896from_expression_to_args_type(exactCardinality,class,[_,_,_],[num,prop,class]) :- !.
  897from_expression_to_args_type(exactCardinality,class,[_,_],[num,prop]) :- !.
  898from_expression_to_args_type(inverseOf,prop,_,[prop]) :- !.
  899from_expression_to_args_type(ExprList,AT,L1,ATs):-
  900  is_expr_list(ExprList,AT,ListType),!,
  901  create_list(ListType,L1,ATs).
  902
  903
  904is_expr_list(intersectionOf,class,class).
  905is_expr_list(unionOf,class,class).
  906is_expr_list(oneOf,class,ind).
  907is_expr_list(propertyChain,prop,prop).
  908
  909create_list([],_,[]).
  910
  911create_list([_|T],AT,[AT|ATT]):-
  912  create_list(T,AT,ATT).
  913
  914
  915
  916
  917
  918
  919
  920/****************************/
  921
  922/**************
  923  FIND FUNCTIONS
  924***************/
  925
  926findClassAssertion(C,Ind,Expl1,ABox):-
  927  (
  928    is_list(Ind) ->
  929    (
  930      find((classAssertion(C,sameIndividual(Ind)),Expl1),ABox)
  931    ) ;
  932    (
  933      find((classAssertion(C,Ind),Expl1),ABox)
  934    )
  935  ).
  936
  937findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox):-
  938	(
  939    is_list(Ind1) ->
  940    (
  941      Ind1S=sameIndividual(Ind1)
  942    ) ;
  943    (
  944      Ind1S=Ind1
  945    )
  946  ),
  947  (
  948    is_list(Ind2) ->
  949    (
  950      Ind2S=sameIndividual(Ind2)
  951    ) ;
  952    (
  953      Ind2S=Ind2
  954    )
  955  ),
  956  find((propertyAssertion(R,Ind1S,Ind2S),Expl1),ABox).
  957
  958
  959/****************************
  960  TABLEAU ALGORITHM
  961****************************/
  962
  963/*
  964find_clash(M,(ABox0,Tabs0),Expl2):-
  965  apply_rules((ABox0,Tabs0),(ABox,Tabs)),
  966  clash(M,(ABox,Tabs),Expl).
  967*/
  968
  969%-------------
  970% clash managing
  971% previous version, manages only one clash at time
  972% need some tricks in some rules for managing the cases of more than one clash
  973% TO IMPROVE!
  974%------------
  975:- multifile clash/4.  976
  977clash(M,owlnothing,Tab,Expl):-
  978  get_abox(Tab,ABox),
  979  %write('clash 6'),nl,
  980  findClassAssertion4OWLNothing(M,ABox,Expl).
  981
  982clash(M,C-Ind,Tab,Expl):-
  983  get_abox(Tab,ABox),
  984  %write('clash 1'),nl,
  985  findClassAssertion(C,Ind,Expl1,ABox),
  986  neg_class(C,NegC),
  987  findClassAssertion(NegC,Ind,Expl2,ABox),
  988  and_f(M,Expl1,Expl2,Expl).
  989
  990clash(M,sameIndividual(LS),Tab,Expl):-
  991  get_abox(Tab,ABox),
  992  %write('clash 2.a'),nl,
  993  findSameIndividual(LS,(sameIndividual(LSABox),Expl1),ABox),
  994  find((differentIndividuals(LD),Expl2),ABox),
  995  member(X,LSABox),
  996  member(Y,LSABox),
  997  member(X,LD),
  998  member(Y,LD),
  999  dif(X,Y),
 1000  and_f(M,Expl1,Expl2,Expl).
 1001
 1002clash(M,differentIndividuals(LS),Tab,Expl):-
 1003  get_abox(Tab,ABox),
 1004  %write('clash 2.b'),nl,
 1005  findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl1),ABox),
 1006  find((sameIndividual(LD),Expl2),ABox),
 1007  member(X,LSABox),
 1008  member(Y,LSABox),
 1009  member(X,LD),
 1010  member(Y,LD),
 1011  dif(X,Y),
 1012  and_f(M,Expl1,Expl2,Expl).
 1013
 1014clash(M,C-sameIndividual(L1),Tab,Expl):-
 1015  get_abox(Tab,ABox),
 1016  %write('clash 3'),nl,
 1017  findClassAssertion(C,sameIndividual(L1),Expl1,ABox),
 1018  neg_class(C,NegC),
 1019  findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox),
 1020  samemember(L1,L2),!,
 1021  and_f(M,Expl1,Expl2,Expl).
 1022
 1023samemember(L1,L2):-
 1024  member(X,L1),
 1025  member(X,L2),!.
 1026
 1027clash(M,C-Ind1,Tab,Expl):-
 1028  get_abox(Tab,ABox),
 1029  %write('clash 4'),nl,
 1030  findClassAssertion(C,Ind1,Expl1,ABox),
 1031  neg_class(C,NegC),
 1032  findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox),
 1033  member(Ind1,L2),
 1034  and_f(M,Expl1,Expl2,Expl).
 1035
 1036clash(M,C-sameIndividual(L1),Tab,Expl):-
 1037  get_abox(Tab,ABox),
 1038  %write('clash 5'),nl,
 1039  findClassAssertion(C,sameIndividual(L1),Expl1,ABox),
 1040  neg_class(C,NegC),
 1041  findClassAssertion(NegC,Ind2,Expl2,ABox),
 1042  member(Ind2,L1),
 1043  and_f(M,Expl1,Expl2,Expl).
 1044
 1045clash(M,C1-Ind,Tab,Expl):-
 1046  get_abox(Tab,ABox),
 1047  %write('clash 7'),nl,
 1048  M:disjointClasses(L), % TODO use hierarchy
 1049  member(C1,L),
 1050  member(C2,L),
 1051  dif(C1,C2),
 1052  findClassAssertion(C1,Ind,Expl1,ABox),
 1053  findClassAssertion(C2,Ind,Expl2,ABox),
 1054  and_f(M,Expl1,Expl2,ExplT),
 1055  and_f_ax(M,disjointClasses(L),ExplT,Expl).
 1056
 1057clash(M,C1-Ind,Tab,Expl):-
 1058  get_abox(Tab,ABox),
 1059  %write('clash 8'),nl,
 1060  M:disjointUnion(Class,L), % TODO use hierarchy
 1061  member(C1,L),
 1062  member(C2,L),
 1063  dif(C1,C2),
 1064  findClassAssertion(C1,Ind,Expl1,ABox),
 1065  findClassAssertion(C2,Ind,Expl2,ABox),
 1066  and_f(M,Expl1,Expl2,ExplT),
 1067  and_f_ax(M,disjointUnion(Class,L),ExplT,Expl).
 1068
 1069clash(M,P-Ind1-Ind2,Tab,Expl):-
 1070  get_abox(Tab,ABox),
 1071  %write('clash 11'),nl,
 1072  findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox),
 1073  neg_class(P,NegP), % use of neg_class with a property
 1074  findPropertyAssertion(NegP,Ind1,Ind2,Expl2,ABox),
 1075  and_f(M,Expl1,Expl2,Expl).
 1076
 1077
 1078/*
 1079clash(M,Tab,Expl):-
 1080  %write('clash 9'),nl,
 1081  findClassAssertion(maxCardinality(N,S,C),Ind,Expl1,ABox),
 1082  s_neighbours(M,Ind,S,Tab,SN),
 1083  get_abox(Tab,ABox),
 1084  individual_class_C(SN,C,ABox,SNC),
 1085  length(SNC,LSS),
 1086  LSS @> N,
 1087  make_expl(M,Ind,S,SNC,Expl1,ABox,Expl).
 1088
 1089clash(M,Tab,Expl):-
 1090  %write('clash 10'),nl,
 1091  findClassAssertion(maxCardinality(N,S),Ind,Expl1,ABox),
 1092  s_neighbours(M,Ind,S,Tab,SN),
 1093  length(SN,LSS),
 1094  LSS @> N,
 1095  make_expl(Ind,S,SN,Expl1,ABox,Expl).
 1096
 1097
 1098% --------------
 1099
 1100make_expl(_,_,_,[],Expl,_,Expl).
 1101
 1102make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):-
 1103  findPropertyAssertion(S,Ind,H,Expl2,ABox),
 1104  and_f(M,Expl2,Expl0,Expl1),
 1105  make_expl(M,Ind,S,T,Expl1,ABox,Expl).
 1106*/
 1107
 1108findSameIndividual(LS,(sameIndividual(LSABox),Expl),ABox):-
 1109  find((sameIndividual(LSABox),Expl),ABox),
 1110  all_members(LS,LSABox).
 1111
 1112findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl),ABox):-
 1113  find((differentIndividuals(LSABox),Expl),ABox),
 1114  all_members(LS,LSABox).
 1115
 1116all_members(LS,LSABox):-
 1117  member(H1,LS),
 1118  member(H2,LS),
 1119  dif(H1,H2),
 1120  member(H1,LSABox),
 1121  member(H2,LSABox),!.
 1122
 1123
 1124
 1125:- multifile check_clash/3. 1126
 1127check_clash(_,'http://www.w3.org/2002/07/owl#Nothing'-_,_):-
 1128  %write('clash 6'),nl,
 1129  !.
 1130
 1131check_clash(_,C-Ind,Tab):-
 1132  get_abox(Tab,ABox),
 1133  %write('clash 1'),nl,
 1134  neg_class(C,NegC),
 1135  findClassAssertion(NegC,Ind,_,ABox),!.
 1136  
 1137check_clash(_,sameIndividual(LS),Tab):-
 1138  get_abox(Tab,ABox),
 1139  %write('clash 2.a'),nl,
 1140  find((differentIndividuals(LD),_Expl2),ABox),
 1141  member(X,LS),
 1142  member(Y,LS),
 1143  member(X,LD),
 1144  member(Y,LD),
 1145  dif(X,Y),!.
 1146  
 1147check_clash(_,differentIndividuals(LS),Tab):-
 1148  get_abox(Tab,ABox),
 1149  %write('clash 2.b'),nl,
 1150  find((sameIndividual(LD),_Expl2),ABox),
 1151  member(X,LS),
 1152  member(Y,LS),
 1153  member(X,LD),
 1154  member(Y,LD),
 1155  dif(X,Y),!.
 1156  
 1157check_clash(_,C-sameIndividual(L1),Tab):-
 1158  get_abox(Tab,ABox),
 1159  %write('clash 3'),nl,
 1160  neg_class(C,NegC),
 1161  findClassAssertion(NegC,sameIndividual(L2),_Expl2,ABox),
 1162  member(X,L1),
 1163  member(X,L2),!.
 1164  
 1165check_clash(_,C-Ind1,Tab):-
 1166  get_abox(Tab,ABox),
 1167  %write('clash 4'),nl,
 1168  neg_class(C,NegC),
 1169  findClassAssertion(NegC,sameIndividual(L2),_Expl2,ABox),
 1170  member(Ind1,L2),!.
 1171  
 1172check_clash(_,C-sameIndividual(L1),Tab):-
 1173  get_abox(Tab,ABox),
 1174  %write('clash 5'),nl,
 1175  neg_class(C,NegC),
 1176  findClassAssertion(NegC,Ind2,_,ABox),
 1177  member(Ind2,L1),!.
 1178  
 1179check_clash(M,C1-Ind,Tab):-
 1180  get_abox(Tab,ABox),
 1181  %write('clash 7'),nl,
 1182  M:disjointClasses(L), % TODO use hierarchy
 1183  member(C1,L),
 1184  member(C2,L),
 1185  dif(C1,C2),
 1186  findClassAssertion(C2,Ind,_,ABox),!.
 1187  
 1188check_clash(M,C1-Ind,Tab):-
 1189  get_abox(Tab,ABox),
 1190  %write('clash 8'),nl,
 1191  M:disjointUnion(_Class,L), % TODO use hierarchy
 1192  member(C1,L),
 1193  member(C2,L),
 1194  dif(C1,C2),
 1195  findClassAssertion(C2,Ind,_,ABox),!.
 1196
 1197check_clash(_,P-Ind1-Ind2,Tab):-
 1198  get_abox(Tab,ABox),
 1199  %write('clash 11'),nl,
 1200  neg_class(P,NegP),  % use of neg_class with a property
 1201  findPropertyAssertion(NegP,Ind1,Ind2,_,ABox),!.
 1202
 1203% -------------
 1204% rules application
 1205% -------------
 1206expand_queue(M,Tab,Tab):-
 1207  test_end_expand_queue(M,Tab),!.
 1208
 1209expand_queue(M,Tab0,Tab):-
 1210  extract_from_expansion_queue(Tab0,EA,Tab1),!,
 1211  apply_all_rules(M,Tab1,EA,Tab2),
 1212  % update_queue(M,T,NewExpQueue),
 1213  expand_queue(M,Tab2,Tab).
 1214
 1215
 1216test_end_expand_queue(M,_):-
 1217  check_time_monitor(M),!.
 1218
 1219test_end_expand_queue(_,Tab):-
 1220  expansion_queue_is_empty(Tab).
 1221
 1222%expand_queue(M,ABox0,[_EA|T],ABox):-
 1223%  expand_queue(M,ABox0,T,ABox).
 1224
 1225apply_all_rules(M,Tab0,EA,Tab):-
 1226  M:setting_trill(det_rules,Rules),
 1227  apply_det_rules(M,Rules,Tab0,EA,Tab1),
 1228  (test_end_apply_rule(M,Tab0,Tab1) ->
 1229  Tab=Tab1;
 1230  apply_all_rules(M,Tab1,EA,Tab)).
 1231
 1232apply_det_rules(M,_,Tab,_,Tab):-
 1233  check_time_monitor(M),!.
 1234
 1235apply_det_rules(M,[],Tab0,EA,Tab):-
 1236  M:setting_trill(nondet_rules,Rules),
 1237  apply_nondet_rules(M,Rules,Tab0,EA,Tab).
 1238
 1239apply_det_rules(M,[H|_],Tab0,EA,Tab):-
 1240  %C=..[H,Tab,Tab1],
 1241  call(H,M,Tab0,EA,Tab),!.
 1242
 1243apply_det_rules(M,[_|T],Tab0,EA,Tab):-
 1244  apply_det_rules(M,T,Tab0,EA,Tab).
 1245
 1246
 1247apply_nondet_rules(M,_,Tab,_,Tab):-
 1248  check_time_monitor(M),!.
 1249
 1250apply_nondet_rules(_,[],Tab,_EA,Tab).
 1251
 1252apply_nondet_rules(M,[H|_],Tab0,EA,Tab):-
 1253  %C=..[H,Tab,L],
 1254  call(H,M,Tab0,EA,L),!,
 1255  member(Tab,L),
 1256  dif(Tab0,Tab).
 1257
 1258apply_nondet_rules(M,[_|T],Tab0,EA,Tab):-
 1259  apply_nondet_rules(M,T,Tab0,EA,Tab).
 1260
 1261
 1262test_end_apply_rule(M,_,_):-
 1263  check_time_monitor(M),!.
 1264
 1265test_end_apply_rule(_,Tab0,Tab1):-
 1266  same_tableau(Tab0,Tab1).
 1267
 1268/*
 1269apply_all_rules(M,Tab0,Tab):-
 1270  apply_nondet_rules([or_rule,max_rule],
 1271                  Tab0,Tab1),
 1272  (Tab0=Tab1 ->
 1273  Tab=Tab1;
 1274  apply_all_rules(M,Tab1,Tab)).
 1275
 1276apply_det_rules([],Tab,Tab).
 1277apply_det_rules([H|_],Tab0,Tab):-
 1278  %C=..[H,Tab,Tab1],
 1279  once(call(H,Tab0,Tab)).
 1280apply_det_rules([_|T],Tab0,Tab):-
 1281  apply_det_rules(T,Tab0,Tab).
 1282apply_nondet_rules([],Tab0,Tab):-
 1283  apply_det_rules([o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule],Tab0,Tab).
 1284apply_nondet_rules([H|_],Tab0,Tab):-
 1285  %C=..[H,Tab,L],
 1286  once(call(H,Tab0,L)),
 1287  member(Tab,L),
 1288  dif(Tab0,Tab).
 1289apply_nondet_rules([_|T],Tab0,Tab):-
 1290  apply_nondet_rules(T,Tab0,Tab).
 1291*/
 1292
 1293
 1294/***********
 1295  rules
 1296************/
 1297
 1298/*
 1299  add_exists_rule
 1300  
 1301  Looks up for a role that links 2 individuals, if it find it, it searches a subclass axiom
 1302  in the KB that contains 'someValuesFrom(R,C)' where R is the role which links the 2 individuals
 1303  and C is a class in which the 2nd individual belongs to.
 1304  
 1305  This rule hasn't a corresponding rule in the tableau
 1306  ========================
 1307*/
 1308add_exists_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1309  get_abox(Tab0,ABox),
 1310  findClassAssertion(C,Ind2,Expl2,ABox),
 1311  (unifiable(C,someValuesFrom(_,_),_)->false;
 1312  ( %existsInKB(M,R,C),
 1313    add_tableau_rules_from_class(M,someValuesFrom(R,C)),
 1314    findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox),
 1315    and_f(M,Expl1,Expl2,Expl),
 1316    modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab)
 1317  )).
 1318
 1319add_exists_rule(M,Tab0,[C,Ind2],Tab):-
 1320  (unifiable(C,someValuesFrom(_,_),_)->false;
 1321  ( get_abox(Tab0,ABox),
 1322    findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox),
 1323    %existsInKB(M,R,C),
 1324    add_tableau_rules_from_class(M,someValuesFrom(R,C)),
 1325    findClassAssertion(C,Ind2,Expl2,ABox),
 1326    and_f(M,Expl1,Expl2,Expl),
 1327    modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab)
 1328  )).
 1329
 1330
 1331/*
 1332existsInKB(M,R,C):-
 1333  M:subClassOf(A,B),
 1334  member(someValuesFrom(R,C),[A,B]).
 1335
 1336existsInKB(M,R,C):-
 1337  M:equivalentClasses(L),
 1338  member(someValuesFrom(R,C),L).
 1339*/
 1340
 1341/* *************** */ 
 1342
 1343/*
 1344  and_rule
 1345  =================
 1346*/
 1347and_rule(M,Tab0,[intersectionOf(LC),Ind],Tab):-
 1348  get_abox(Tab0,ABox),
 1349  findClassAssertion(intersectionOf(LC),Ind,Expl,ABox),
 1350  \+ indirectly_blocked(Ind,Tab0),
 1351  scan_and_list(M,LC,Ind,Expl,Tab0,Tab,0).
 1352
 1353
 1354%----------------
 1355scan_and_list(_M,[],_Ind,_Expl,Tab,Tab,Mod):-
 1356  dif(Mod,0).
 1357
 1358scan_and_list(M,[C|T],Ind,Expl,Tab0,Tab,_Mod):-
 1359  modify_ABox(M,Tab0,C,Ind,Expl,Tab1),!,
 1360  scan_and_list(M,T,Ind,Expl,Tab1,Tab,1).
 1361
 1362scan_and_list(M,[_C|T],Ind,Expl,Tab0,Tab,Mod):-
 1363  scan_and_list(M,T,Ind,Expl,Tab0,Tab,Mod).
 1364/* ************* */
 1365
 1366/*
 1367  or_rule
 1368  ===============
 1369*/
 1370or_rule(M,Tab0,[unionOf(LC),Ind],L):- 
 1371  get_abox(Tab0,ABox),
 1372  findClassAssertion(unionOf(LC),Ind,Expl,ABox),
 1373  \+ indirectly_blocked(Ind,Tab0),
 1374  %not_ind_intersected_union(Ind,LC,ABox),
 1375  % length(LC,NClasses),
 1376  get_choice_point_id(M,ID),
 1377  scan_or_list(M,LC,0,ID,Ind,Expl,Tab0,L),
 1378  dif(L,[]),
 1379  create_choice_point(M,Ind,or,unionOf(LC),LC,_),!. % last variable whould be equals to ID
 1380
 1381not_ind_intersected_union(Ind,LC,ABox):-
 1382  \+ ind_intersected_union(Ind,LC,ABox).
 1383
 1384ind_intersected_union(Ind,LC,ABox) :-
 1385  member(C,LC),
 1386  findClassAssertion(C,Ind,_,ABox),!.
 1387%---------------
 1388scan_or_list(_,[],_,_,_,_,_,[]):- !.
 1389
 1390scan_or_list(M,[C|T],N0,CP,Ind,Expl0,Tab0,[Tab|L]):-
 1391  add_choice_point(M,cpp(CP,N0),Expl0,Expl),
 1392  modify_ABox(M,Tab0,C,Ind,Expl,Tab),
 1393  N is N0 + 1,
 1394  scan_or_list(M,T,N,CP,Ind,Expl0,Tab0,L).
 1395
 1396/* **************** */
 1397
 1398/*
 1399  exists_rule
 1400  ==================
 1401*/
 1402exists_rule(M,Tab0,[someValuesFrom(R,C),Ind1],Tab):-
 1403  get_abox(Tab0,ABox0),
 1404  findClassAssertion(someValuesFrom(R,C),Ind1,Expl,ABox0),
 1405  \+ blocked(Ind1,Tab0),
 1406  \+ connected_individual(R,C,Ind1,ABox0),
 1407  new_ind(M,Ind2),
 1408  add_edge(R,Ind1,Ind2,Tab0,Tab1),
 1409  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 1410  modify_ABox(M,Tab2,C,Ind2,Expl,Tab3),
 1411  modify_ABox(M,Tab3,R,Ind1,Ind2,Expl,Tab).
 1412
 1413
 1414
 1415%---------------
 1416connected_individual(R,C,Ind1,ABox):-
 1417  findPropertyAssertion(R,Ind1,Ind2,_,ABox),
 1418  findClassAssertion(C,Ind2,_,ABox).
 1419
 1420/* ************ */
 1421
 1422/*
 1423  forall_rule
 1424  ===================
 1425*/
 1426forall_rule(M,Tab0,[allValuesFrom(R,C),Ind1],Tab):-
 1427  get_abox(Tab0,ABox),
 1428  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1429  \+ indirectly_blocked(Ind1,Tab0),
 1430  findClassAssertion(allValuesFrom(R,C),Ind1,Expl1,ABox),
 1431  and_f(M,Expl1,Expl2,Expl),
 1432  modify_ABox(M,Tab0,C,Ind2,Expl,Tab).
 1433
 1434forall_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1435  get_abox(Tab0,ABox),
 1436  findClassAssertion(allValuesFrom(R,C),Ind1,Expl1,ABox),
 1437  \+ indirectly_blocked(Ind1,Tab0),
 1438  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1439  and_f(M,Expl1,Expl2,Expl),
 1440  modify_ABox(M,Tab0,C,Ind2,Expl,Tab).
 1441
 1442/* ************** */
 1443
 1444/*
 1445  forall_plus_rule
 1446  =================
 1447*/
 1448forall_plus_rule(M,Tab0,[allValuesFrom(S,C),Ind1],Tab):-
 1449  get_abox(Tab0,ABox),
 1450  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1451  find_sub_sup_trans_role(M,R,S,Expl3),
 1452  findClassAssertion(allValuesFrom(S,C),Ind1,Expl1,ABox),
 1453  \+ indirectly_blocked(Ind1,Tab0),
 1454  and_f(M,Expl1,Expl2,ExplT),
 1455  and_f(M,ExplT,Expl3,Expl),
 1456  modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab).
 1457
 1458forall_plus_rule(M,Tab0,[R,Ind1,Ind2],Tab):-
 1459  get_abox(Tab0,ABox),
 1460  findClassAssertion(allValuesFrom(S,C),Ind1,Expl1,ABox),
 1461  \+ indirectly_blocked(Ind1,Tab0),
 1462  findPropertyAssertion(R,Ind1,Ind2,Expl2,ABox),
 1463  find_sub_sup_trans_role(M,R,S,Expl3),
 1464  and_f(M,Expl1,Expl2,ExplT),
 1465  and_f(M,ExplT,Expl3,Expl),
 1466  modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab).
 1467
 1468% --------------
 1469find_sub_sup_trans_role(M,R,S,Expl):-
 1470  M:subPropertyOf(R,S),
 1471  M:transitiveProperty(R),
 1472  initial_expl(M,EExpl),
 1473  and_f_ax(M,subPropertyOf(R,S),EExpl,Expl0),
 1474  and_f_ax(M,transitive(R),Expl0,Expl).
 1475
 1476find_sub_sup_trans_role(M,R,S,Expl):-
 1477  M:subPropertyOf(R,S),
 1478  \+ M:transitiveProperty(R),
 1479  initial_expl(M,EExpl),
 1480  and_f_ax(M,subPropertyOf(R,S),EExpl,Expl).
 1481/* ************ */
 1482
 1483/*
 1484  unfold_rule
 1485  ===========
 1486*/
 1487
 1488unfold_rule(M,Tab0,[C,Ind],Tab):-
 1489  get_abox(Tab0,ABox),
 1490  findClassAssertion(C,Ind,Expl,ABox),
 1491  find_sub_sup_class(M,C,D,Ax),
 1492  and_f_ax(M,Ax,Expl,AxL),
 1493  modify_ABox(M,Tab0,D,Ind,AxL,Tab1),
 1494  add_nominal(M,D,Ind,Tab1,Tab).
 1495
 1496/* -- unfold_rule
 1497      takes a class C1 in which Ind belongs, find a not atomic class C
 1498      that contains C1 (C is seen as list of classes), controls if
 1499      the individual Ind belongs to all those classes, if yes it finds a class D (if exists)
 1500      that is the superclass or an equivalent class of C and adds D to label of Ind
 1501      - for managing tableau with more than one clash -
 1502      correspond to the ce_rule
 1503   --
 1504*/
 1505unfold_rule(M,Tab0,[C1,Ind],Tab):-
 1506  find_not_atomic(M,C1,C,L),
 1507  get_abox(Tab0,ABox),
 1508  ( C = unionOf(_) -> findClassAssertion(C1,Ind,Expl,ABox)
 1509   ; find_all(M,Ind,L,ABox,Expl)),
 1510  %find_sub_sup_class(M,C,D,Ax),
 1511  %and_f_ax(M,Ax,Expl1,AxL1),
 1512  modify_ABox(M,Tab0,C,Ind,Expl,Tab1),
 1513  add_nominal(M,C,Ind,Tab1,Tab).
 1514
 1515/* -- unfold_rule
 1516 *    control propertyRange e propertyDomain
 1517 * --
 1518 */
 1519unfold_rule(M,Tab0,[P,S,O],Tab):-
 1520  get_abox(Tab0,ABox),
 1521  find_class_prop_range_domain(M,P,S,O,Ind,D,Expl,ABox),
 1522  modify_ABox(M,Tab0,D,Ind,Expl,Tab1),
 1523  add_nominal(M,D,Ind,Tab1,Tab).
 1524
 1525/*
 1526 * -- unfold_rule
 1527 *    manage the negation
 1528 * --
 1529 */
 1530unfold_rule(M,Tab0,[complementOf(C),Ind],Tab):-
 1531  get_abox(Tab0,ABox),
 1532  findClassAssertion(complementOf(C),Ind,Expl,ABox),
 1533  find_neg_class(C,D),
 1534  and_f_ax(M,complementOf(C),Expl,AxL),
 1535  modify_ABox(M,Tab0,D,Ind,AxL,Tab1),
 1536  add_nominal(M,D,Ind,Tab1,Tab).
 1537
 1538% ----------------
 1539% add_nominal
 1540
 1541add_nominal(M,D,Ind,Tab0,Tab):-
 1542  get_abox(Tab0,ABox0),
 1543  ((D = oneOf(_),
 1544    \+ member(nominal(Ind),ABox0))
 1545    ->
 1546   (
 1547     ABox1 = [nominal(Ind)|ABox0],
 1548     (member((classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),_E),ABox1)
 1549     ->
 1550     set_abox(Tab0,ABox1,Tab)
 1551     ;
 1552     (empty_expl(M,Expl),set_abox(Tab0,[(classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),Expl)|ABox1],Tab))
 1553     )
 1554   )
 1555    ;
 1556  set_abox(Tab0,ABox0,Tab)
 1557  ).
 1558
 1559% ----------------
 1560% unionOf, intersectionOf, subClassOf, negation, allValuesFrom, someValuesFrom, exactCardinality(min and max), maxCardinality, minCardinality
 1561:- multifile find_neg_class/2. 1562
 1563find_neg_class(unionOf(L),intersectionOf(NL)):-
 1564  neg_list(L,NL).
 1565
 1566find_neg_class(intersectionOf(L),unionOf(NL)):-
 1567  neg_list(L,NL).
 1568
 1569find_neg_class(subClassOf(C,D),intersectionOf(C,ND)):-
 1570  neg_class(D,ND).
 1571
 1572find_neg_class(complementOf(C),C).
 1573
 1574find_neg_class(allValuesFrom(R,C),someValuesFrom(R,NC)):-
 1575  neg_class(C,NC).
 1576
 1577find_neg_class(someValuesFrom(R,C),allValuesFrom(R,NC)):-
 1578  neg_class(C,NC).
 1579
 1580% ---------------
 1581
 1582neg_class(complementOf(C),C):- !.
 1583
 1584neg_class(C,complementOf(C)).
 1585
 1586% ---------------
 1587
 1588neg_list([],[]).
 1589
 1590neg_list([H|T],[complementOf(H)|T1]):-
 1591  neg_list(T,T1).
 1592
 1593neg_list([complementOf(H)|T],[H|T1]):-
 1594  neg_list(T,T1).
 1595
 1596% ----------------
 1597
 1598find_class_prop_range_domain(M,P,S,O,O,D,Expl,ABox):-
 1599  findPropertyAssertion(P,S,O,ExplPA,ABox),
 1600  %ind_as_list(IndL,L),
 1601  %member(Ind,L),
 1602  M:propertyRange(P,D),
 1603  and_f_ax(M,propertyRange(P,D),ExplPA,Expl).
 1604
 1605find_class_prop_range_domain(M,P,S,O,S,D,Expl,ABox):-
 1606  findPropertyAssertion(P,S,O,ExplPA,ABox),
 1607  %ind_as_list(IndL,L),
 1608  %member(Ind,L),
 1609  M:propertyDomain(P,D),
 1610  and_f_ax(M,propertyDomain(P,D),ExplPA,Expl).
 1611
 1612
 1613%-----------------
 1614:- multifile find_sub_sup_class/4. 1615
 1616% subClassOf
 1617find_sub_sup_class(M,C,D,subClassOf(C,D)):-
 1618  M:subClassOf(C,D).
 1619
 1620%equivalentClasses
 1621find_sub_sup_class(M,C,D,equivalentClasses(L)):-
 1622  M:equivalentClasses(L),
 1623  member(C,L),
 1624  member(D,L),
 1625  dif(C,D).
 1626
 1627%concept for concepts allValuesFrom
 1628find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(R,D),Ax):-
 1629  find_sub_sup_class(M,C,D,Ax),
 1630  atomic(D).
 1631
 1632%role for concepts allValuesFrom
 1633find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(S,C),subPropertyOf(R,S)):-
 1634  M:subPropertyOf(R,S).
 1635
 1636%concept for concepts someValuesFrom
 1637find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(R,D),Ax):-
 1638  find_sub_sup_class(M,C,D,Ax),
 1639  atomic(D).
 1640
 1641%role for concepts someValuesFrom
 1642find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(S,C),subPropertyOf(R,S)):-
 1643  M:subPropertyOf(R,S).
 1644
 1645
 1646/*******************
 1647 managing the concept (C subclassOf Thing)
 1648 this implementation doesn't work well in a little set of cases
 1649 TO IMPROVE!
 1650 *******************/
 1651/*
 1652find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1653  M:subClassOf(A,B),
 1654  member(C,[A,B]),!.
 1655
 1656find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1657  M:classAssertion(C,_),!.
 1658
 1659find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1660  M:equivalentClasses(L),
 1661  member(C,L),!.
 1662
 1663find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1664  M:unionOf(L),
 1665  member(C,L),!.
 1666
 1667find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1668  M:equivalentClasses(L),
 1669  member(someValuesFrom(_,C),L),!.
 1670
 1671find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1672  M:equivalentClasses(L),
 1673  member(allValuesFrom(_,C),L),!.
 1674
 1675find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1676  M:equivalentClasses(L),
 1677  member(minCardinality(_,_,C),L),!.
 1678
 1679find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1680  M:equivalentClasses(L),
 1681  member(maxCardinality(_,_,C),L),!.
 1682
 1683find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):-
 1684  M:equivalentClasses(L),
 1685  member(exactCardinality(_,_,C),L),!.
 1686
 1687*/
 1688
 1689%--------------------
 1690% looks for not atomic concepts descriptions containing class C
 1691find_not_atomic(M,C,Ax,LC):-
 1692  M:subClassOf(A,B),
 1693  find_not_atomic_int(C,[A,B],Ax,LC).
 1694
 1695find_not_atomic(M,C,Ax,LC):-
 1696  M:equivalentClasses(L),
 1697  find_not_atomic_int(C,L,Ax,LC).
 1698
 1699/*
 1700find_not_atomic(M,C,unionOf(L1),L1):-
 1701  M:subClassOf(A,B),
 1702  member(unionOf(L1),[A,B]),
 1703  member(C,L1).
 1704
 1705find_not_atomic(M,C,unionOf(L1),L1):-
 1706  M:equivalentClasses(L),
 1707  member(unionOf(L1),L),
 1708  member(C,L1).
 1709*/
 1710
 1711find_not_atomic_int(C,LC0,intersectionOf(L1),L1):-
 1712  member(intersectionOf(L1),LC0),
 1713  member(C,L1).
 1714
 1715find_not_atomic_int(C,LC0,Ax,LC):-
 1716  member(intersectionOf(L1),LC0),
 1717  find_not_atomic_int(C,L1,Ax,LC).
 1718
 1719find_not_atomic_int(C,LC0,unionOf(L1),L1):-
 1720  member(unionOf(L1),LC0),
 1721  member(C,L1).
 1722
 1723find_not_atomic_int(C,LC0,Ax,LC):-
 1724  member(unionOf(L1),LC0),
 1725  find_not_atomic_int(C,L1,Ax,LC).
 1726
 1727
 1728
 1729
 1730% -----------------------
 1731% puts together the explanations of all the concepts found by find_not_atomic/3
 1732find_all(_M,_,[],_,[]).
 1733
 1734find_all(M,Ind,[H|T],ABox,ExplT):-
 1735  findClassAssertion(H,Ind,Expl1,ABox),
 1736  find_all(M,Ind,T,ABox,Expl2),
 1737  and_f(M,Expl1,Expl2,ExplT).
 1738
 1739
 1740% ------------------------
 1741%  unfold_rule to unfold roles
 1742% ------------------------
 1743% sub properties
 1744unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1745  get_abox(Tab0,ABox),
 1746  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1747  find_sub_sup_property(M,C,D,Ax),
 1748  and_f_ax(M,Ax,Expl,AxL),
 1749  modify_ABox(M,Tab0,D,Ind1,Ind2,AxL,Tab1),
 1750  add_nominal(M,D,Ind1,Tab1,Tab2),
 1751  add_nominal(M,D,Ind2,Tab2,Tab).
 1752
 1753%inverseProperties
 1754unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1755  get_abox(Tab0,ABox),
 1756  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1757  find_inverse_property(M,C,D,Ax),
 1758  and_f_ax(M,Ax,Expl,AxL),
 1759  modify_ABox(M,Tab0,D,Ind2,Ind1,AxL,Tab1),
 1760  add_nominal(M,D,Ind1,Tab1,Tab2),
 1761  add_nominal(M,D,Ind2,Tab2,Tab).
 1762
 1763%transitiveProperties
 1764unfold_rule(M,Tab0,[C,Ind1,Ind2],Tab):-
 1765  get_abox(Tab0,ABox),
 1766  findPropertyAssertion(C,Ind1,Ind2,Expl,ABox),
 1767  find_transitive_property(M,C,Ax),
 1768  and_f_ax(M,Ax,Expl,AxL),
 1769  findPropertyAssertion(C,Ind2,Ind3,ExplSecond,ABox),
 1770  and_f(M,AxL,ExplSecond,ExplTrans),
 1771  modify_ABox(M,Tab0,C,Ind1,Ind3,ExplTrans,Tab).
 1772
 1773%-----------------
 1774% subPropertyOf
 1775find_sub_sup_property(M,C,D,subPropertyOf(C,D)):-
 1776  M:subPropertyOf(C,D).
 1777
 1778%equivalentProperties
 1779find_sub_sup_property(M,C,D,equivalentProperties(L)):-
 1780  M:equivalentProperties(L),
 1781  member(C,L),
 1782  member(D,L),
 1783  dif(C,D).
 1784
 1785%-----------------
 1786%inverseProperties
 1787find_inverse_property(M,C,D,inverseProperties(C,D)):-
 1788  M:inverseProperties(C,D).
 1789
 1790find_inverse_property(M,C,D,inverseProperties(D,C)):-
 1791  M:inverseProperties(D,C).
 1792
 1793%inverseProperties
 1794find_inverse_property(M,C,C,symmetricProperty(C)):-
 1795  M:symmetricProperty(C).
 1796
 1797%-----------------
 1798%transitiveProperties
 1799find_transitive_property(M,C,transitiveProperty(C)):-
 1800  M:transitiveProperty(C).
 1801/* ************* */
 1802
 1803/*
 1804  ce_rule
 1805  =============
 1806*/
 1807ce_rule(M,Tab0,Tab):-
 1808  get_tabs(Tab0,(T,_,_)),
 1809  find_not_sub_sup_class(M,Ax,UnAx),
 1810  vertices(T,Inds),
 1811  apply_ce_to(M,Inds,Ax,UnAx,Tab0,Tab,C),
 1812  C @> 0.
 1813
 1814
 1815% ------------------
 1816find_not_sub_sup_class(M,subClassOf(C,D),unionOf(complementOf(C),D)):-
 1817  M:subClassOf(C,D),
 1818  \+ atomic(C).
 1819
 1820
 1821find_not_sub_sup_class(M,equivalentClasses(L),unionOf(L1)):-
 1822  M:equivalentClasses(L),
 1823  member(C,L),
 1824  \+ atomic(C),
 1825  copy_neg_c(C,L,L1).
 1826
 1827%-------------------------
 1828copy_neg_c(_,[],[]).
 1829
 1830copy_neg_c(C,[C|T],[complementOf(C)|T1]):-
 1831  !,
 1832  copy_neg_c(C,T,T1).
 1833
 1834copy_neg_c(C,[H|T],[H|T1]):-
 1835  copy_neg_c(C,T,T1).
 1836
 1837%---------------------
 1838apply_ce_to(_M,[],_,_,Tab,Tab,0).
 1839
 1840apply_ce_to(M,[Ind|T],Ax,UnAx,Tab0,Tab,C):-
 1841  \+ indirectly_blocked(Ind,Tab),
 1842  modify_ABox(M,Tab0,UnAx,Ind,[Ax],Tab1),!,
 1843  apply_ce_to(M,T,Ax,UnAx,Tab1,Tab,C0),
 1844  C is C0 + 1.
 1845
 1846apply_ce_to(M,[_Ind|T],Ax,UnAx,Tab0,Tab,C):-
 1847  apply_ce_to(M,T,Ax,UnAx,Tab0,Tab,C).
 1848
 1849/* **************** */
 1850
 1851/*
 1852  min_rule
 1853  =============
 1854*/
 1855min_rule(M,Tab0,[minCardinality(N,S),Ind1],Tab):-
 1856  get_abox(Tab0,ABox),
 1857  findClassAssertion(minCardinality(N,S),Ind1,Expl,ABox),
 1858  \+ blocked(Ind1,Tab0),
 1859  s_neighbours(M,Ind1,S,Tab0,SN),
 1860  safe_s_neigh(SN,S,Tab0,SS),
 1861  length(SS,LSS),
 1862  LSS @< N,
 1863  NoI is N-LSS,
 1864  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1),
 1865  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 1866
 1867
 1868min_rule(M,Tab0,[minCardinality(N,S,C),Ind1],Tab):-
 1869  get_abox(Tab0,ABox),
 1870  findClassAssertion(minCardinality(N,S,C),Ind1,Expl,ABox),
 1871  \+ blocked(Ind1,Tab0),
 1872  s_neighbours(M,Ind1,S,Tab0,SN),
 1873  safe_s_neigh_C(SN,S,C,Tab0,ABox,SS),
 1874  length(SS,LSS),
 1875  LSS @< N,
 1876  NoI is N-LSS,
 1877  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1),
 1878  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 1879
 1880min_rule(M,Tab0,[exactCardinality(N,S),Ind1],Tab):-
 1881  get_abox(Tab0,ABox),
 1882  findClassAssertion(exactCardinality(N,S),Ind1,Expl,ABox),
 1883  \+ blocked(Ind1,Tab0),
 1884  s_neighbours(M,Ind1,S,Tab0,SN),
 1885  safe_s_neigh(SN,S,Tab0,SS),
 1886  length(SS,LSS),
 1887  LSS @< N,
 1888  NoI is N-LSS,
 1889  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1),
 1890  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 1891
 1892
 1893min_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],Tab):-
 1894  get_abox(Tab0,ABox),
 1895  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl,ABox),
 1896  \+ blocked(Ind1,Tab0),
 1897  s_neighbours(M,Ind1,S,Tab0,SN),
 1898  safe_s_neigh_C(SN,S,C,Tab0,SS),
 1899  length(SS,LSS),
 1900  LSS @< N,
 1901  NoI is N-LSS,
 1902  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1),
 1903  modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab).
 1904
 1905min_rule(M,(ABox,Tabs),([(differentIndividuals(NI),Expl)|ABox1],Tabs1)):-
 1906  findClassAssertion(exactCardinality(N,S),Ind1,Expl,ABox),
 1907  \+ blocked(Ind1,(ABox,Tabs)),
 1908  s_neighbours(M,Ind1,S,(ABox,Tabs),SN),
 1909  safe_s_neigh(SN,S,(ABox,Tabs),SS),
 1910  length(SS,LSS),
 1911  LSS @< N,
 1912  NoI is N-LSS,
 1913  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,ABox,Tabs,ABox1,Tabs1).
 1914
 1915
 1916min_rule(M,(ABox,Tabs),([(differentIndividuals(NI),Expl)|ABox1],Tabs1)):-
 1917  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl,ABox),
 1918  \+ blocked(Ind1,(ABox,Tabs)),
 1919  s_neighbours(M,Ind1,S,(ABox,Tabs),SN),
 1920  safe_s_neigh(SN,S,(ABox,Tabs),SS),
 1921  length(SS,LSS),
 1922  LSS @< N,
 1923  NoI is N-LSS,
 1924  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,ABox,Tabs,ABox1,Tabs1).
 1925
 1926% ----------------------
 1927min_rule_neigh(_,0,_,_,_,[],Tab,Tab).
 1928
 1929min_rule_neigh(M,N,S,Ind1,Expl,[Ind2|NI],Tab0,Tab):-
 1930  N > 0,
 1931  NoI is N-1,
 1932  new_ind(M,Ind2),
 1933  add_edge(S,Ind1,Ind2,Tab0,Tab1),
 1934  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 1935  modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3),
 1936  %check_block(Ind2,Tab3),
 1937  min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab3,Tab).
 1938
 1939%----------------------
 1940min_rule_neigh_C(_,0,_,_,_,_,[],Tab,Tab).
 1941
 1942min_rule_neigh_C(M,N,S,C,Ind1,Expl,[Ind2|NI],Tab0,Tab):-
 1943  N > 0,
 1944  NoI is N-1,
 1945  new_ind(M,Ind2),
 1946  add_edge(S,Ind1,Ind2,Tab0,Tab1),
 1947  add_owlThing_ind(M,Tab1,Ind2,Tab2),
 1948  modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3),
 1949  modify_ABox(M,Tab3,C,Ind2,[propertyAssertion(S,Ind1,Ind2)|Expl],Tab4),
 1950  %check_block(Ind2,Tab4),
 1951  min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab4,Tab).
 1952
 1953%---------------------
 1954safe_s_neigh([],_,_,[]):-!.
 1955
 1956safe_s_neigh([H|T],S,Tab,[H|ST]):-
 1957  safe(H,S,Tab),
 1958  safe_s_neigh(T,S,Tab,ST).
 1959
 1960safe_s_neigh_C(L,S,C,Tab,LT):-
 1961  get_abox(Tab,ABox),
 1962  safe_s_neigh_C(L,S,C,Tab,ABox,LT).
 1963
 1964safe_s_neigh_C([],_,_,_,_,_,[]):-!.
 1965
 1966safe_s_neigh_C([H|T],S,C,Tab,ABox,[H|ST]):-
 1967  safe(H,S,Tab),
 1968  findClassAssertion(C,H,_,ABox),!,
 1969  safe_s_neigh_C(T,S,C,Tab,ABox,ST).
 1970
 1971/* **************** */
 1972
 1973/*
 1974  max_rule
 1975  ================
 1976*/
 1977max_rule(M,Tab0,[maxCardinality(N,S),Ind],L):-
 1978  get_abox(Tab0,ABox),
 1979  findClassAssertion(maxCardinality(N,S),Ind,Expl0,ABox),
 1980  \+ indirectly_blocked(Ind,Tab0),
 1981  s_neighbours(M,Ind,S,Tab0,SN),
 1982  length(SN,LSS),
 1983  LSS @> N,
 1984  get_choice_point_id(M,ID),
 1985  scan_max_list(M,maxCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 1986
 1987max_rule(M,Tab0,[maxCardinality(N,S,C),Ind],L):-
 1988  get_abox(Tab0,ABox),
 1989  findClassAssertion(maxCardinality(N,S,C),Ind,Expl0,ABox),
 1990  \+ indirectly_blocked(Ind,Tab0),
 1991  s_neighbours(M,Ind,S,Tab0,SN),
 1992  individual_class_C(SN,C,ABox,SNC),
 1993  length(SNC,LSS),
 1994  LSS @> N,
 1995  get_choice_point_id(M,ID),%gtrace,
 1996  scan_max_list(M,maxCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 1997
 1998%---------------------
 1999
 2000max_rule(M,Tab0,[exactCardinality(N,S),Ind],L):-
 2001  get_abox(Tab0,ABox),
 2002  findClassAssertion(exactCardinality(N,S),Ind,Expl0,ABox),
 2003  \+ indirectly_blocked(Ind,Tab0),
 2004  s_neighbours(M,Ind,S,Tab0,SN),
 2005  length(SN,LSS),
 2006  LSS @> N,
 2007  get_choice_point_id(M,ID),
 2008  scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 2009
 2010max_rule(M,Tab0,[exactCardinality(N,S,C),Ind],L):-
 2011  get_abox(Tab0,ABox),
 2012  findClassAssertion(exactCardinality(N,S,C),Ind,Expl0,ABox),
 2013  \+ indirectly_blocked(Ind,Tab0),
 2014  s_neighbours(M,Ind,S,Tab0,SN),
 2015  individual_class_C(SN,C,ABox,SNC),
 2016  length(SNC,LSS),
 2017  LSS @> N,
 2018  get_choice_point_id(M,ID),%gtrace,
 2019  scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 2020
 2021  max_rule(M,Tab0,[S,Ind,_],L):-
 2022    get_abox(Tab0,ABox),
 2023    findClassAssertion(exactCardinality(N,S),Ind,Expl0,ABox),
 2024    \+ indirectly_blocked(Ind,Tab0),
 2025    s_neighbours(M,Ind,S,Tab0,SN),
 2026    length(SN,LSS),
 2027    LSS @> N,
 2028    get_choice_point_id(M,ID),
 2029    scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 
 2030  
 2031  max_rule(M,Tab0,[S,Ind,_],L):-
 2032    get_abox(Tab0,ABox),
 2033    findClassAssertion(exactCardinality(N,S,C),Ind,Expl0,ABox),
 2034    \+ indirectly_blocked(Ind,Tab0),
 2035    s_neighbours(M,Ind,S,Tab0,SN),
 2036    individual_class_C(SN,C,ABox,SNC),
 2037    length(SNC,LSS),
 2038    LSS @> N,
 2039    get_choice_point_id(M,ID),%gtrace,
 2040    scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID
 2041
 2042%---------------------
 2043
 2044scan_max_list(M,MaxCardClass,S,C,SN,CP,Ind,Expl,Tab0,ABox,Tab_list):-
 2045  create_couples_for_merge(SN,[],Ind_couples), % MAYBE check_individuals_not_equal(M,YI,YJ,ABox), instead of dif
 2046  length(Ind_couples,NChoices),
 2047  (
 2048    NChoices @> 1 -> (FirstChoice = -1) ; (FirstChoice = 0)
 2049  ),
 2050  create_list_for_max_rule(M,Ind_couples,FirstChoice,CP,Ind,S,C,Expl,Tab0,ABox,Tab_list),
 2051  dif(Tab_list,[]),
 2052  create_choice_point(M,Ind,mr,MaxCardClass,Ind_couples,_). % last variable whould be equals to ID
 2053
 2054create_couples_for_merge([],Ind_couples,Ind_couples).
 2055
 2056create_couples_for_merge([H|T],Ind_couples0,Ind_couples):-
 2057  create_couples_for_merge_int(H,T,Ind_couples0,Ind_couples1),
 2058  create_couples_for_merge(T,Ind_couples1,Ind_couples).
 2059
 2060create_couples_for_merge_int(_,[],Ind_couples,Ind_couples).
 2061
 2062create_couples_for_merge_int(I,[H|T],Ind_couples0,Ind_couples):-
 2063  create_couples_for_merge_int(I,T,[I-H|Ind_couples0],Ind_couples).
 2064
 2065create_list_for_max_rule(_,[],_,_,_,_,_,_,_,_,[]).
 2066
 2067create_list_for_max_rule(M,[YI-YJ|Ind_couples],N0,CP,Ind,S,C,Expl0,Tab0,ABox,[Tab|Tab_list]):-
 2068  findPropertyAssertion(S,Ind,YI,ExplYI,ABox),
 2069  findPropertyAssertion(S,Ind,YJ,ExplYJ,ABox),
 2070  findClassAssertion(C,YI,ExplCYI,ABox),
 2071  findClassAssertion(C,YJ,ExplCYJ,ABox),
 2072  and_f(M,ExplYI,ExplYJ,ExplS0),
 2073  and_f(M,ExplS0,ExplCYI,ExplS1),
 2074  and_f(M,ExplS1,ExplCYJ,ExplC0),
 2075  and_f(M,ExplC0,Expl0,ExplT0),
 2076  (
 2077    dif(N0,-1) ->
 2078    (
 2079      add_choice_point(M,cpp(CP,N0),ExplT0,ExplT),
 2080      N is N0 + 1
 2081    ) ;
 2082    (
 2083      ExplT = ExplT0,
 2084      N = N0
 2085    )
 2086  ),
 2087  flatten([YI,YJ],LI),
 2088  merge_all_individuals(M,[(sameIndividual(LI),ExplT)],Tab0,Tab),
 2089  create_list_for_max_rule(M,Ind_couples,N,CP,Ind,S,C,Expl0,Tab0,ABox,Tab_list).
 2090
 2091/*
 2092scan_max_list(M,S,SN,CP,Ind,Expl,ABox0,Tabs0,YI-YJ,ABox,Tabs):-
 2093  member(YI,SN),
 2094  member(YJ,SN),
 2095  % generate cp
 2096  check_individuals_not_equal(M,YI,YJ,ABox0),
 2097  findPropertyAssertion(S,Ind,YI,ExplYI,ABox0),
 2098  findPropertyAssertion(S,Ind,YJ,ExplYJ,ABox0),
 2099  and_f(M,ExplYI,ExplYJ,Expl0),
 2100  and_f(M,Expl0,Expl,ExplT0),
 2101  add_choice_point(M,cpp(CP,N0),ExplT0,ExplT),
 2102  merge_all_individuals(M,[(sameIndividual([YI,YJ]),ExplT)],ABox0,Tabs0,ABox,Tabs).
 2103*/
 2104
 2105%--------------------
 2106check_individuals_not_equal(M,X,Y,ABox):-
 2107  dif(X,Y),
 2108  \+ same_ind(M,[X],Y,ABox).
 2109%--------------------
 2110individual_class_C([],_,_,[]).
 2111
 2112individual_class_C([H|T],C,ABox,[H|T1]):-
 2113  findClassAssertion(C,H,_,ABox),!,
 2114  individual_class_C(T,C,ABox,T1).
 2115
 2116individual_class_C([_H|T],C,ABox,T1):-
 2117  %\+ findClassAssertion(C,H,_,ABox),
 2118  individual_class_C(T,C,ABox,T1).
 2119/* *************** */
 2120
 2121/*
 2122  ch_rule
 2123  ================
 2124*/
 2125ch_rule(M,Tab0,[maxCardinality(N,S,C),Ind1],L):-
 2126  get_abox(Tab0,ABox),
 2127  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2128  \+ indirectly_blocked(Ind1,Tab0),
 2129  findClassAssertion(maxCardinality(N,S,C),Ind1,Expl1,ABox),
 2130  absent_c_not_c(Ind2,C,ABox),
 2131  and_f(M,Expl1,Expl2,Expl),
 2132  get_choice_point_id(M,ID),%gtrace,
 2133  neg_class(C,NC),
 2134  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2135  dif(L,[]),
 2136  create_choice_point(M,Ind2,ch,maxCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2137
 2138ch_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],L):-
 2139  get_abox(Tab0,ABox),
 2140  findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2141  \+ indirectly_blocked(Ind1,Tab0),
 2142  findClassAssertion(exactCardinality(N,S,C),Ind1,Expl1,ABox),
 2143  absent_c_not_c(Ind2,C,ABox),
 2144  and_f(M,Expl1,Expl2,Expl),
 2145  get_choice_point_id(M,ID),%gtrace,
 2146  neg_class(C,NC),
 2147  scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2148  dif(L,[]),
 2149  create_choice_point(M,Ind2,ch,exactCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2150
 2151  ch_rule(M,Tab0,[S,Ind1,Ind2],L):-
 2152    get_abox(Tab0,ABox),
 2153    findClassAssertion(maxCardinality(N,S,C),Ind1,Expl1,ABox),
 2154    \+ indirectly_blocked(Ind1,Tab0),
 2155    findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2156    absent_c_not_c(Ind2,C,ABox),
 2157    and_f(M,Expl1,Expl2,Expl),
 2158    get_choice_point_id(M,ID),%gtrace,
 2159    neg_class(C,NC),
 2160    scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2161    dif(L,[]),
 2162    create_choice_point(M,Ind2,ch,maxCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2163  
 2164  ch_rule(M,Tab0,[S,Ind1,Ind2],L):-
 2165    get_abox(Tab0,ABox),
 2166    findClassAssertion(exactCardinality(N,S,C),Ind1,Expl1,ABox),
 2167    \+ indirectly_blocked(Ind1,Tab0),
 2168    findPropertyAssertion(S,Ind1,Ind2,Expl2,ABox),
 2169    absent_c_not_c(Ind2,C,ABox),
 2170    and_f(M,Expl1,Expl2,Expl),
 2171    get_choice_point_id(M,ID),%gtrace,
 2172    neg_class(C,NC),
 2173    scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L),
 2174    dif(L,[]),
 2175    create_choice_point(M,Ind2,ch,exactCardinality(N,S,C),[C,NC],_),!. % last variable whould be equals to ID
 2176
 2177%---------------------
 2178
 2179absent_c_not_c(Ind,C,ABox) :-
 2180  \+ is_there_c_not_c(Ind,C,ABox).
 2181
 2182is_there_c_not_c(Ind,C,ABox) :-
 2183 findClassAssertion(C,Ind,_,ABox),!.
 2184
 2185is_there_c_not_c(Ind,C,ABox) :-
 2186  neg_class(C,NC),
 2187  findClassAssertion(NC,Ind,_,ABox),!.
 2188
 2189/* *************** */
 2190
 2191/*
 2192 o_rule
 2193 ============
 2194*/
 2195
 2196o_rule(M,Tab0,[oneOf(C),X],Tab):-
 2197  get_abox(Tab0,ABox),
 2198  findClassAssertion(oneOf(C),X,ExplX,ABox),
 2199  findClassAssertion(oneOf(D),Y,ExplY,ABox),
 2200  containsCommon(C,D),
 2201  dif(X,Y),
 2202  notDifferentIndividuals(M,X,Y,ABox),
 2203  nominal(C,Tab),
 2204  ind_as_list(X,LX),
 2205  ind_as_list(Y,LY),
 2206  and_f(M,ExplX,ExplY,ExplC),
 2207  merge(M,X,Y,ExplC,Tab0,Tab),
 2208  flatten([LX,LY],LI0),
 2209  sort(LI0,LI),
 2210  absent(sameIndividual(LI),ExplC,ABox).
 2211
 2212containsCommon(L1,L2):-
 2213  member(X,L1),
 2214  member(X,L2),!.
 2215% -------------------
 2216
 2217/* ************* */
 2218
 2219/***********
 2220  utility for sameIndividual
 2221************/
 2222
 2223ind_as_list(sameIndividual(L),L):-
 2224  retract_sameIndividual(L),!.
 2225
 2226ind_as_list(X,[X]):-
 2227  atomic(X).
 2228
 2229list_as_sameIndividual(L0,sameIndividual(L)):-
 2230  list_as_sameIndividual_int(L0,L1),
 2231  sort(L1,L).
 2232
 2233list_as_sameIndividual_int([],[]).
 2234
 2235list_as_sameIndividual_int([sameIndividual(L0)|T0],L):-
 2236  !,
 2237  append(L0,T0,L1),
 2238  list_as_sameIndividual_int(L1,L).
 2239
 2240list_as_sameIndividual_int([H|T0],[H|T]):-
 2241  list_as_sameIndividual_int(T0,T).
 2242
 2243
 2244find_same(H,ABox,sameIndividual(L),Expl):-
 2245  find((sameIndividual(L),Expl),ABox),
 2246  member(X,L),
 2247  member(X,H),!.
 2248
 2249find_same(_H,_ABox,[],[]).
 2250
 2251
 2252/*
 2253 retract_sameIndividual(L)
 2254 ==========
 2255*/
 2256retract_sameIndividual(sameIndividual(L)):-
 2257  !,
 2258  retract_sameIndividual(L).
 2259
 2260retract_sameIndividual(L):-
 2261  get_trill_current_module(N),
 2262  retract(N:sameIndividual(L)).
 2263
 2264retract_sameIndividual(L):-
 2265  get_trill_current_module(N),
 2266  \+ retract(N:sameIndividual(L)).
 2267/* ****** */
 2268
 2269/*
 2270 * nominal/2, blockable/2, blocked/2, indirectly_blocked/2 and safe/3
 2271 *
 2272 */
 2273
 2274nominal(Inds,Tab):-
 2275  get_abox(Tab,ABox),
 2276  find((nominal(Ind)),ABox),
 2277  member(Ind,Inds).
 2278
 2279% ----------------
 2280
 2281blockable(Ind,Tab):-
 2282  get_abox(Tab,ABox),
 2283  ( find((nominal(Ind)),ABox)
 2284    ->
 2285    false
 2286    ;
 2287    true ).
 2288
 2289% ---------------
 2290
 2291blocked(Ind,Tab):-
 2292  check_block(Ind,Tab).
 2293
 2294/*
 2295
 2296  control for blocking an individual
 2297
 2298*/
 2299
 2300check_block(Ind,Tab):-
 2301  blockable(Ind,Tab),
 2302  get_tabs(Tab,(T,_,_)),
 2303  transpose_ugraph(T,T1),
 2304  ancestor_nt(Ind,T1,A),
 2305  neighbours(Ind,T1,N),
 2306  check_block1(Ind,A,N,Tab),!.
 2307
 2308check_block(Ind,Tab):-
 2309  blockable(Ind,Tab),
 2310  get_tabs(Tab,(T,_,_)),
 2311  transpose_ugraph(T,T1),
 2312  neighbours(Ind,T1,N),
 2313  check_block2(N,Tab),!.
 2314
 2315
 2316check_block1(Indx,A,N,Tab):-
 2317  member(Indx0,N),
 2318  member(Indy,A),
 2319  member(Indy0,A),
 2320  get_tabs(Tab,(T,RBN,_)),
 2321  neighbours(Indy,T,N2),
 2322  member(Indy0,N2),
 2323  rb_lookup((Indx0,Indx),V,RBN),
 2324  rb_lookup((Indy0,Indy),V2,RBN),
 2325  member(R,V),
 2326  member(R,V2),
 2327  get_abox(Tab,ABox),
 2328  same_label(Indx,Indy0,ABox),
 2329  same_label(Indx0,Indy,ABox),
 2330  all_node_blockable(Indx0,Indy0,Tab),!.
 2331
 2332%check_block2([],_).
 2333
 2334check_block2([H|Tail],Tab):-
 2335  blocked(H,Tab),
 2336  check_block2(Tail,Tab).
 2337
 2338%---------------
 2339indirectly_blocked(Ind,Tab):-
 2340  get_tabs(Tab,(T,_RBN,_RBR)),
 2341  transpose_ugraph(T,T1),
 2342  neighbours(Ind,T1,N),
 2343  member(A,N),
 2344  blocked(A,Tab),!.
 2345
 2346%---------------------
 2347/*
 2348  An R-neighbour y of a node x is safe if
 2349  (i)  x is blockable or
 2350  (ii) x is a nominal node and y is not blocked.
 2351*/
 2352
 2353safe(Ind,R,Tab):-
 2354  get_tabs(Tab,(_,_,RBR)),
 2355  rb_lookup(R,V,RBR),
 2356  get_parent(X,Ind,V),
 2357  blockable(X,Tab),!.
 2358
 2359safe(Ind,R,Tab):-
 2360  get_tabs(Tab,(_,_,RBR)),
 2361  rb_lookup(R,V,RBR),
 2362  get_parent(X,Ind,V),
 2363  nominal(X,Tab),!,
 2364  \+ blocked(Ind,Tab).
 2365
 2366get_parent(X,Ind,[(X,Ind)|_T]):-!.
 2367
 2368get_parent(X,Ind,[(X,LI)|_T]):-
 2369  is_list(LI),
 2370  member(Ind,LI),!.
 2371
 2372get_parent(X,Ind,[_|T]):-
 2373  get_parent(X,Ind,T).
 2374
 2375
 2376/* ***** */
 2377
 2378/*
 2379 writel
 2380 write a list one element at each line
 2381 ==========
 2382*/
 2383writel([]):-!.
 2384
 2385writel([T|C]):-
 2386  write(T),nl,
 2387  writel(C).
 2388
 2389/*
 2390 writeABox
 2391 ==========
 2392*/
 2393writeABox(Tab):-
 2394  get_abox(Tab,ABox),
 2395  writel(ABox).
 2396
 2397
 2398/*
 2399  build_abox
 2400  ===============
 2401*/
 2402
 2403%---------------
 2404subProp(M,SubProperty,Property,Subject,Object):-
 2405  M:subPropertyOf(SubProperty,Property),M:propertyAssertion(SubProperty,Subject,Object).
 2406
 2407%--------------
 2408
 2409add_owlThing_ind(M,Tab0,Ind,Tab):-
 2410  prepare_nom_list(M,[Ind],NomListOut),
 2411  add_all_to_tableau(M,NomListOut,Tab0,Tab).
 2412
 2413add_owlThing_list(M,Tab0,Tab):- % TODO
 2414  get_tabs(Tab0,(T,_,_)),
 2415  vertices(T,NomListIn),
 2416  prepare_nom_list(M,NomListIn,NomListOut),
 2417  add_all_to_tableau(M,NomListOut,Tab0,Tab).
 2418
 2419%--------------
 2420
 2421prepare_nom_list(_,[],[]).
 2422
 2423prepare_nom_list(M,[literal(_)|T],T1):-!,
 2424  prepare_nom_list(M,T,T1).
 2425
 2426prepare_nom_list(M,[H|T],[(classAssertion('http://www.w3.org/2002/07/owl#Thing',H),Expl)|T1]):-
 2427  initial_expl(M,Expl),
 2428  prepare_nom_list(M,T,T1).
 2429%--------------
 2430
 2431
 2432/* merge nodes in (ABox,Tabs) */
 2433
 2434merge_all_individuals(_,[],Tab,Tab).
 2435
 2436merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):-
 2437  get_abox(Tab0,ABox0),
 2438  find_same(H,ABox0,L,ExplL),
 2439  dif(L,[]),!,
 2440  merge_all1(M,H,Expl,L,Tab0,Tab1),
 2441  list_as_sameIndividual([H,L],SI), %TODO
 2442  %flatten([H,L],L0),
 2443  %sort(L0,SI),
 2444  and_f(M,Expl,ExplL,ExplT),
 2445  add_to_tableau(Tab1,(SI,ExplT),Tab2),
 2446  remove_from_tableau(Tab2,(sameIndividual(L),ExplL),Tab3),
 2447  retract_sameIndividual(L),
 2448  merge_all_individuals(M,T,Tab3,Tab).
 2449
 2450merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):-
 2451  %get_abox(Tab0,ABox0),
 2452  %find_same(H,ABox0,L,_),
 2453  %L==[],!,
 2454  merge_all2(M,H,Expl,Tab0,Tab1),
 2455  add_to_tableau(Tab1,(sameIndividual(H),Expl),Tab2),
 2456  merge_all_individuals(M,T,Tab2,Tab).
 2457
 2458merge_all1(_M,[],_,_,Tab,Tab).
 2459
 2460merge_all1(M,[H|T],Expl,L,Tab0,Tab):-
 2461  \+ member(H,L),
 2462  merge(M,H,L,Expl,Tab0,Tab1),
 2463  merge_all1(M,T,Expl,[H|L],Tab1,Tab).
 2464
 2465merge_all1(M,[H|T],Expl,L,Tab0,Tab):-
 2466  member(H,L),
 2467  merge_all1(M,T,Expl,L,Tab0,Tab).
 2468
 2469
 2470
 2471merge_all2(M,[X,Y|T],Expl,Tab0,Tab):-
 2472  merge(M,X,Y,Expl,Tab0,Tab1),
 2473  merge_all1(M,T,Expl,[X,Y],Tab1,Tab).
 2474
 2475
 2476
 2477/*
 2478  creation of the query anon individual
 2479
 2480*/
 2481query_ind(trillan(0)).
 2482
 2483/*
 2484  creation of a new individual
 2485
 2486*/
 2487new_ind(M,trillan(I)):-
 2488  retract(M:trillan_idx(I)),
 2489  I1 is I+1,
 2490  assert(M:trillan_idx(I1)).
 2491
 2492/*
 2493  same label for two individuals
 2494
 2495*/
 2496
 2497same_label(X,Y,ABox):-
 2498  \+ different_label(X,Y,ABox),
 2499  !.
 2500
 2501/*
 2502  different label in two individuals
 2503
 2504*/
 2505
 2506different_label(X,Y,ABox):-
 2507  findClassAssertion(C,X,_,ABox),
 2508  \+ findClassAssertion(C,Y,_,ABox).
 2509
 2510different_label(X,Y,ABox):-
 2511  findClassAssertion(C,Y,_,ABox),
 2512  \+ findClassAssertion(C,X,_,ABox).
 2513
 2514
 2515/*
 2516  all nodes in path from X to Y are blockable?
 2517
 2518*/
 2519
 2520all_node_blockable(X,Y,Tab):-
 2521  get_tabs(Tab,(T,_,_)),
 2522  graph_min_path(X,Y,T,P),
 2523  all_node_blockable1(P,Tab).
 2524
 2525all_node_blockable1([],_).
 2526
 2527all_node_blockable1([H|Tail],Tab):-
 2528  blockable(H,Tab),
 2529  all_node_blockable1(Tail,Tab).
 2530
 2531/*
 2532  find a path in the graph
 2533  returns only one of the shortest path (if there are 2 paths that have same length, it returns only one of them)
 2534*/
 2535/*
 2536% It may enter in infinite loop when there is a loop in the graph
 2537graph_min_path(X,Y,T,P):-
 2538  findall(Path, graph_min_path1(X,Y,T,Path), Ps),
 2539  min_length(Ps,P).
 2540
 2541graph_min_path1(X,Y,T,[X,Y]):-
 2542  member(X-L,T),
 2543  member(Y,L).
 2544
 2545graph_min_path1(X,Y,T,[X|P]):-
 2546  member(X-L,T),
 2547  member(Z,L),
 2548  graph_min_path1(Z,Y,T,P).
 2549
 2550min_length([H],H).
 2551
 2552min_length([H|T],MP):-
 2553  min_length(T,P),
 2554  length(H,N),
 2555  length(P,NP),
 2556  (N<NP ->
 2557     MP= H
 2558   ;
 2559     MP= P).
 2560*/
 2561
 2562graph_min_path(X,Y,T,P):-
 2563  edges(T, Es),
 2564  aggregate_all(min(Length,Path),graph_min_path1(X,Y,Es,Length,Path),min(_L,P)).
 2565
 2566
 2567graph_min_path1(X, Y, Es, N, Path) :- 
 2568  graph_min_path1_int(X, Y, Es, [], Path),
 2569  length(Path, N).
 2570
 2571graph_min_path1_int(X, Y, Es, Seen, [X]) :-
 2572  \+ memberchk(X, Seen),
 2573  member(X-Y, Es).
 2574graph_min_path1_int(X, Z, Es, Seen, [X|T]) :-
 2575  \+ memberchk(X, Seen),
 2576  member(X-Y, Es),
 2577  graph_min_path1_int(Y, Z, Es, [X|Seen], T),
 2578  \+ memberchk(X, T).
 2579
 2580/*
 2581 find all ancestor of a node
 2582
 2583*/
 2584ancestor(Ind,T,AN):-
 2585  transpose_ugraph(T,T1),
 2586  findall(Y,connection(Ind,T1,Y),AN).
 2587  %ancestor1([Ind],T1,[],AN).
 2588
 2589ancestor_nt(Ind,TT,AN):-
 2590  findall(Y,connection(Ind,TT,Y),AN).
 2591
 2592ancestor1([],_,A,A).
 2593
 2594ancestor1([Ind|Tail],T,A,AN):-
 2595  neighbours(Ind,T,AT),
 2596  add_all_n(AT,Tail,Tail1),
 2597  add_all_n(A,AT,A1),
 2598  ancestor1(Tail1,T,A1,AN).
 2599
 2600:- table connection/3. 2601connection(X, T, Y) :-
 2602  neighbours(X,T,AT),
 2603  member(Y,AT).
 2604
 2605connection(X, T, Y) :-
 2606  connection(X, T, Z),
 2607  connection(Z, T, Y).
 2608
 2609
 2610%-----------------
 2611/*
 2612
 2613 add_all_n(L1,L2,LO)
 2614 add in L2 all item of L1 without duplicates
 2615
 2616*/
 2617
 2618add_all_n([],A,A).
 2619
 2620add_all_n([H|T],A,AN):-
 2621  \+ member(H,A),
 2622  add_all_n(T,[H|A],AN).
 2623
 2624add_all_n([H|T],A,AN):-
 2625  member(H,A),
 2626  add_all_n(T,A,AN).
 2627/* *************** */
 2628
 2629
 2630
 2631/*
 2632  find all S neighbours (S is a role)
 2633*/
 2634s_neighbours(M,Ind1,S,Tab,SN):- %gtrace,
 2635  get_tabs(Tab,(_,_,RBR)),
 2636  rb_lookup(S,VN,RBR),!,
 2637  s_neighbours1(Ind1,VN,SN0),
 2638  flatten(SN0,SN1),
 2639  get_abox(Tab,ABox),
 2640  s_neighbours2(M,SN1,SN1,SN,ABox),!.
 2641
 2642s_neighbours(_,_Ind1,_S,_Tab,[]). % :-
 2643%  get_tabs(Tab,(_,_,RBR)),
 2644%  \+ rb_lookup(S,_VN,RBR).
 2645
 2646s_neighbours1(_,[],[]).
 2647
 2648s_neighbours1(Ind1,[(Ind1,Y)|T],[Y|T1]):-
 2649  s_neighbours1(Ind1,T,T1).
 2650
 2651s_neighbours1(Ind1,[(X,_Y)|T],T1):-
 2652  dif(X,Ind1),
 2653  s_neighbours1(Ind1,T,T1).
 2654  
 2655s_neighbours2(_,_,[],[],_).
 2656
 2657s_neighbours2(M,SN,[H|T],[H|T1],ABox):-
 2658  s_neighbours2(M,SN,T,T1,ABox),
 2659  not_same_ind(M,T1,H,ABox),!.
 2660
 2661s_neighbours2(M,SN,[_H|T],T1,ABox):-
 2662  s_neighbours2(M,SN,T,T1,ABox).
 2663  %same_ind(M,T1,H,ABox).
 2664
 2665
 2666%-----------------
 2667
 2668not_same_ind(M,SN,H,_ABox):-
 2669  M:differentIndividuals(SI),
 2670  member(H,SI),
 2671  member(H2,SI),
 2672  member(H2,SN),
 2673  dif(H,H2),!.
 2674
 2675not_same_ind(_,SN,H,ABox):-
 2676  find((differentIndividuals(SI),_),ABox),
 2677  member(H,SI),
 2678  member(H2,SI),
 2679  member(H2,SN),
 2680  dif(H,H2),!.
 2681
 2682not_same_ind(M,SN,H,ABox):-
 2683  \+ same_ind(M,SN,H,ABox),!.
 2684
 2685same_ind(M,SN,H,_ABox):-
 2686  M:sameIndividual(SI),
 2687  member(H,SI),
 2688  member(H2,SI),
 2689  member(H2,SN),
 2690  dif(H,H2).
 2691
 2692same_ind(_,SN,H,ABox):-
 2693  find((sameIndividual(SI),_),ABox),
 2694  member(H,SI),
 2695  member(H2,SI),
 2696  member(H2,SN),
 2697  dif(H,H2).
 2698
 2699/* ************* */
 2700
 2701/*
 2702 s_predecessors
 2703 ==============
 2704 find all S-predecessor of Ind
 2705*/
 2706
 2707s_predecessors(M,Ind1,S,Tab,SN):-
 2708  get_tabs(Tab,(_,_,RBR)),
 2709  rb_lookup(S,VN,RBR),
 2710  s_predecessors1(Ind1,VN,SN1),
 2711  get_abox(Tab,ABox),
 2712  s_predecessors2(M,SN1,SN,ABox).
 2713
 2714s_predecessors(_M,_Ind1,S,(_ABox,(_,_,RBR)),[]):-
 2715  \+ rb_lookup(S,_VN,RBR).
 2716
 2717s_predecessors1(_,[],[]).
 2718
 2719s_predecessors1(Ind1,[(Y,Ind1)|T],[Y|T1]):-
 2720  s_predecessors1(Ind1,T,T1).
 2721
 2722s_predecessors1(Ind1,[(_X,Y)|T],T1):-
 2723  dif(Y,Ind1),
 2724  s_predecessors1(Ind1,T,T1).
 2725
 2726s_predecessors2(_M,[],[],_).
 2727
 2728s_predecessors2(M,[H|T],[H|T1],ABox):-
 2729  s_predecessors2(M,T,T1,ABox),
 2730  \+ same_ind(M,T1,H,ABox).
 2731
 2732s_predecessors2(M,[H|T],T1,ABox):-
 2733  s_predecessors2(M,T,T1,ABox),
 2734  same_ind(M,T1,H,ABox).
 2735
 2736/* ********** */
 2737
 2738/* *************
 2739   
 2740Probability computation
 2741   Old version
 2742
 2743   ************* */
 2744
 2745/*
 2746build_formula([],[],Var,Var).
 2747
 2748build_formula([D|TD],TF,VarIn,VarOut):-
 2749        build_term(D,[],[],VarIn,Var1),!,
 2750        build_formula(TD,TF,Var1,VarOut).
 2751
 2752build_formula([D|TD],[F|TF],VarIn,VarOut):-
 2753        build_term(D,[],F,VarIn,Var1),
 2754        build_formula(TD,TF,Var1,VarOut).
 2755
 2756build_term([],F,F,Var,Var).
 2757
 2758build_term([(Ax,S)|TC],F0,F,VarIn,VarOut):-!,
 2759  (p_x(Ax,_)->
 2760    (nth0_eq(0,NVar,VarIn,(Ax,S))->
 2761      Var1=VarIn
 2762    ;
 2763      append(VarIn,[(Ax,S)],Var1),
 2764      length(VarIn,NVar)
 2765    ),
 2766    build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2767  ;
 2768    (p(Ax,_)->
 2769      (nth0_eq(0,NVar,VarIn,(Ax,[]))->
 2770        Var1=VarIn
 2771      ;
 2772        append(VarIn,[(Ax,[])],Var1),
 2773        length(VarIn,NVar)
 2774      ),
 2775      build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2776    ;
 2777      build_term(TC,F0,F,VarIn,VarOut)
 2778    )
 2779  ).
 2780
 2781build_term([Ax|TC],F0,F,VarIn,VarOut):-!,
 2782  (p(Ax,_)->
 2783    (nth0_eq(0,NVar,VarIn,(Ax,[]))->
 2784      Var1=VarIn
 2785    ;
 2786      append(VarIn,[(Ax,[])],Var1),
 2787      length(VarIn,NVar)
 2788    ),
 2789    build_term(TC,[[NVar,0]|F0],F,Var1,VarOut)
 2790  ;
 2791    build_term(TC,F0,F,VarIn,VarOut)
 2792  ).
 2793*/
 2794
 2795/* nth0_eq(PosIn,PosOut,List,El) takes as input a List,
 2796an element El and an initial position PosIn and returns in PosOut
 2797the position in the List that contains an element exactly equal to El
 2798*/
 2799
 2800/*
 2801nth0_eq(N,N,[H|_T],El):-
 2802        H==El,!.
 2803
 2804nth0_eq(NIn,NOut,[_H|T],El):-
 2805        N1 is NIn+1,
 2806        nth0_eq(N1,NOut,T,El).
 2807
 2808*/
 2809/* var2numbers converts a list of couples (Rule,Substitution) into a list
 2810of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer
 2811starting from 0 */
 2812/*
 2813var2numbers([],_N,[]).
 2814
 2815var2numbers([(R,_S)|T],N,[[N,2,[Prob,Prob1,0.3,0.7]]|TNV]):-
 2816        (p(R,_);p_x(R,_)),
 2817        compute_prob_ax(R,Prob),!,
 2818        Prob1 is 1-Prob,
 2819        N1 is N+1,
 2820        var2numbers(T,N1,TNV).
 2821
 2822
 2823compute_prob_ax(R,Prob):-
 2824  findall(P, p(R,P),Probs),
 2825  compute_prob_ax1(Probs,Prob).
 2826
 2827compute_prob_ax1([Prob],Prob):-!.
 2828
 2829compute_prob_ax1([Prob1,Prob2],Prob):-!,
 2830  Prob is Prob1+Prob2-(Prob1*Prob2).
 2831
 2832compute_prob_ax1([Prob1 | T],Prob):-
 2833  compute_prob_ax1(T,Prob0),
 2834  Prob is Prob1 + Prob0 - (Prob1*Prob0).
 2835
 2836*/
 2837
 2838/**********************
 2839
 2840 Probability Computation
 2841
 2842***********************/
 2843
 2844:- thread_local
 2845	%get_var_n/5,
 2846        rule_n/1,
 2847        na/2,
 2848        v/3. 2849
 2850%rule_n(0).
 2851
 2852compute_prob(M,Expl,Prob):-
 2853  retractall(v(_,_,_)),
 2854  retractall(na(_,_)),
 2855  retractall(rule_n(_)),
 2856  assert(rule_n(0)),
 2857  %findall(1,M:annotationAssertion('http://ml.unife.it/disponte#probability',_,_),NAnnAss),length(NAnnAss,NV),
 2858  get_bdd_environment(M,Env),
 2859  build_bdd(M,Env,Expl,BDD),
 2860  ret_prob(Env,BDD,Prob),
 2861  clean_environment(M,Env), !.
 2862
 2863get_var_n(Env,R,S,Probs,V):-
 2864  (
 2865    v(R,S,V) ->
 2866      true
 2867    ;
 2868      %length(Probs,L),
 2869      add_var(Env,Probs,R,V),
 2870      assert(v(R,S,V))
 2871  ).
 2872
 2873
 2874get_prob_ax(M,(Ax,_Ind),N,Prob):- !,
 2875  compute_prob_ax(M,Ax,Prob),
 2876  ( na(Ax,N) ->
 2877      true
 2878    ;
 2879      rule_n(N),
 2880      assert(na(Ax,N)),
 2881      retract(rule_n(N)),
 2882      N1 is N + 1,
 2883      assert(rule_n(N1))
 2884  ).
 2885get_prob_ax(M,Ax,N,Prob):- !,
 2886  compute_prob_ax(M,Ax,Prob),
 2887  ( na(Ax,N) ->
 2888      true
 2889    ;
 2890      rule_n(N),
 2891      assert(na(Ax,N)),
 2892      retract(rule_n(N)),
 2893      N1 is N + 1,
 2894      assert(rule_n(N1))
 2895  ).
 2896
 2897compute_prob_ax(M,Ax,Prob):-
 2898  findall(ProbA,(M:annotationAssertion('https://sites.google.com/a/unife.it/ml/disponte#probability',Ax,literal(ProbAT)),atom_number(ProbAT,ProbA)),ProbsOld), % Retro-compatibility
 2899  findall(ProbA,(M:annotationAssertion('http://ml.unife.it/disponte#probability',Ax,literal(ProbAT)),atom_number(ProbAT,ProbA)),ProbsNew),
 2900  append(ProbsNew, ProbsOld, Probs),
 2901  compute_prob_ax1(Probs,Prob).
 2902
 2903compute_prob_ax1([Prob],Prob):-!.
 2904
 2905compute_prob_ax1([Prob1,Prob2],Prob):-!,
 2906  Prob is Prob1+Prob2-(Prob1*Prob2).
 2907
 2908compute_prob_ax1([Prob1 | T],Prob):-
 2909  compute_prob_ax1(T,Prob0),
 2910  Prob is Prob1 + Prob0 - (Prob1*Prob0).
 2911
 2912/************************/
 2913
 2914unload_all_algorithms :-
 2915  unload_file(library(trill_internal)),
 2916  unload_file(library(trillp_internal)),
 2917  unload_file(library(tornado_internal)).
 2918
 2919set_algorithm(M:trill):-
 2920  unload_all_algorithms,
 2921  consult(library(trill_internal)),
 2922  clean_up(M),!.
 2923
 2924set_algorithm(M:trillp):-
 2925  unload_all_algorithms,
 2926  consult(library(trillp_internal)),
 2927  clean_up(M),!.
 2928
 2929set_algorithm(M:tornado):-
 2930  unload_all_algorithms,
 2931  consult(library(tornado_internal)),
 2932  clean_up(M),!.
 2933
 2934init_trill(Alg):-
 2935  utility_translation:get_module(M),
 2936  set_algorithm(M:Alg),
 2937  set_up(M),
 2938  utility_translation:set_up_kb_loading(M),
 2939  trill:add_kb_prefixes(M:[('disponte'='http://ml.unife.it/disponte#'),('owl'='http://www.w3.org/2002/07/owl#')]).
 2940
 2941/**************/
 2942/*get_trill_current_module('utility_translation'):-
 2943  pengine_self(_Name),!.*/
 2944%get_trill_current_module(Name):-
 2945%  pengine_self(Name),!.
 2946%get_trill_current_module('utility_translation'):- !.
 2947get_trill_current_module(M):-
 2948  utility_translation:get_module(M).
 2949/**************/
 2950
 2951:- multifile sandbox:safe_primitive/1. 2952
 2953sandbox:safe_primitive(trill:get_var_n(_,_,_,_,_)).
 2954
 2955
 2956
 2957
 2958
 2959% ==========================================================================================================
 2960% TABLEAU MANAGER
 2961% ==========================================================================================================
 2962
 2963% ======================================================================
 2964% As Dict
 2965% ======================================================================
 2966
 2967/* getters and setters for Tableau */
 2968
 2969get_abox(Tab,ABox):-
 2970  ABox = Tab.abox.
 2971
 2972set_abox(Tab0,ABox,Tab):-
 2973  Tab = Tab0.put(abox,ABox).
 2974
 2975get_tabs(Tab,Tabs):-
 2976  Tabs = Tab.tabs.
 2977
 2978set_tabs(Tab0,Tabs,Tab):-
 2979  Tab = Tab0.put(tabs,Tabs).
 2980
 2981get_clashes(Tab,Clashes):-
 2982  Clashes = Tab.clashes.
 2983
 2984set_clashes(Tab0,Clashes,Tab):-
 2985  Tab = Tab0.put(clashes,Clashes).
 2986
 2987absence_of_clashes(Tab):-
 2988  get_clashes(Tab,Clashes),
 2989  Clashes=[].
 2990
 2991get_expansion_queue(Tab,ExpansionQueue):-
 2992  ExpansionQueue = Tab.expq.
 2993
 2994set_expansion_queue(Tab0,ExpansionQueue,Tab):-
 2995  Tab = Tab0.put(expq,ExpansionQueue).
 2996
 2997extract_from_expansion_queue(Tab0,EA,Tab):-
 2998  get_expansion_queue(Tab0,EQ0),
 2999  extract_from_expansion_queue_int(EQ0,EA,EQ),
 3000  set_expansion_queue(Tab0,EQ,Tab).
 3001
 3002extract_from_expansion_queue_int([[],[EA|T]],EA,[[],T]).
 3003
 3004extract_from_expansion_queue_int([[EA|T],NonDetQ],EA,[T,NonDetQ]).
 3005
 3006expansion_queue_is_empty(Tab):-
 3007  get_expansion_queue(Tab,EQ),
 3008  empty_expansion_queue(EQ).
 3009
 3010empty_expansion_queue([[],[]]).
 3011
 3012same_tableau(Tab1,Tab2):-
 3013  get_abox(Tab1,ABox),
 3014  get_abox(Tab2,ABox),
 3015  get_tabs(Tab1,Tabs),
 3016  get_tabs(Tab2,Tabs).
 3017
 3018/* initializers */
 new_tabelau(-EmptyTableaus:dict)
Initialize an empty tableau. /
 3025new_tableau(tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}):-
 3026  new_abox(ABox),
 3027  new_tabs(Tabs),
 3028  empty_expansion_queue(ExpansionQueue).
 init_tabelau(+ABox:abox, +Tabs:tableau, -InitializedTableaus:dict)
Initialize a tableau with the lements given in input. /
 3036init_tableau(ABox,Tabs,tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}):-
 3037  empty_expansion_queue(ExpansionQueue).
 init_tabelau(+ABox:abox, +Tabs:tableau, +ExpansionQueue:expansion_queue, -InitializedTableaus:dict)
Initialize a tableau with the lements given in input. /
 3044init_tableau(ABox,Tabs,ExpansionQueue,tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}).
 3045
 3046
 3047% ======================================================================
 3048% As List (missing Expansion Queue!)
 3049% ======================================================================
 3050/*
 3051
 3052get_abox([ABox,_,_],ABox).
 3053
 3054set_abox([_,Tabs,C],ABox,[ABox,Tabs,C]).
 3055
 3056get_tabs([_,Tabs,_],Tabs).
 3057
 3058set_tabs([ABox,_,C],Tabs,[ABox,Tabs,C]).
 3059
 3060get_clashes([_,_,Clashes],Clashes).
 3061
 3062set_clashes([ABox,Tabs,_],Clashes,[ABox,Tabs,Clashes]).
 3063
 3064
 3065
 3066new_tableau([ABox,Tabs,[]]):-
 3067  new_abox(ABox),
 3068  new_tabs(Tabs).
 3069
 3070
 3071
 3072init_tableau(ABox,Tabs,[ABox,Tabs,[]]).
 3073
 3074*/
 3075
 3076
 3077
 3078% ===================================
 3079% ABOX
 3080% ===================================
 3081
 3082/* abox as a list */
 3083
 3084new_abox([]).
 3085
 3086 
 3087/* add El to ABox */
 3088add_to_tableau(Tableau0,El,Tableau):-
 3089  get_abox(Tableau0,ABox0),
 3090  add_to_abox(ABox0,El,ABox),
 3091  set_abox(Tableau0,ABox,Tableau).
 3092
 3093remove_from_tableau(Tableau0,El,Tableau):-
 3094  get_abox(Tableau0,ABox0),
 3095  remove_from_abox(ABox0,El,ABox),
 3096  set_abox(Tableau0,ABox,Tableau).
 3097
 3098add_clash_to_tableau(M,Tableau0,ToCheck,Tableau):-
 3099  check_clash(M,ToCheck,Tableau0),!,
 3100  get_clashes(Tableau0,Clashes0),
 3101  add_to_clashes(Clashes0,ToCheck,Clashes),
 3102  set_clashes(Tableau0,Clashes,Tableau).
 3103
 3104add_clash_to_tableau(_,Tableau,_,Tableau).
 3105
 3106assign(L,L).
 3107/*
 3108  find & control (not find)
 3109*/
 3110find(El,ABox):-
 3111  member(El,ABox).
 3112
 3113control(El,ABox):-
 3114  \+ find(El,ABox).
 3115
 3116/* end of abox a s list */
 3117
 3118/* abox as a red-black tree */
 3119/*new_abox(T):-
 3120  rb_new(T).
 3121
 3122add(A,(Ass,Ex),A1):-
 3123  rb_insert(A,(Ass,Ex),[],A1).
 3124
 3125find((Ass,Ex),A):-
 3126  rb_lookup((Ass,Ex),_,A).
 3127*/
 3128/* end of abox as a rb tree */
 3129
 3130
 3131add_to_abox(ABox,El,[El|ABox]).
 3132
 3133remove_from_abox(ABox0,El,ABox):-
 3134  delete(ABox0,El,ABox).
 3135
 3136
 3137add_to_clashes(Clashes,'http://www.w3.org/2002/07/owl#Nothing'-_,[owlnothing|Clashes]):-!.
 3138
 3139add_to_clashes(Clashes,El,[El|Clashes]).
 3140
 3141remove_from_abox(Clashes0,El,Clashes):-
 3142  delete(Clashes0,El,Clashes).
 3143
 3144/*
 3145  add_all_to_tableau(M,L1,L2,LO).
 3146  add in L2 all item of L1
 3147*/
 3148add_all_to_tableau(M,L,Tableau0,Tableau):-
 3149  get_abox(Tableau0,ABox0),
 3150  get_clashes(Tableau0,Clashes0),
 3151  add_all_to_abox_and_clashes(M,L,Tableau0,ABox0,ABox,Clashes0,Clashes),
 3152  set_abox(Tableau0,ABox,Tableau1),
 3153  set_clashes(Tableau1,Clashes,Tableau).
 3154
 3155add_all_to_abox_and_clashes(_,[],_,A,A,C,C).
 3156
 3157add_all_to_abox_and_clashes(M,[(classAssertion(Class,I),Expl)|T],Tab0,A0,A,C0,C):-
 3158  check_clash(M,Class-I,Tab0),!,
 3159  add_to_abox(A0,(classAssertion(Class,I),Expl),A1),
 3160  add_to_clashes(C0,Class-I,C1),
 3161  set_abox(Tab0,A1,Tab),
 3162  add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
 3163
 3164add_all_to_abox_and_clashes(M,[(sameIndividual(LI),Expl)|T],Tab0,A0,A,C0,C):-
 3165  check_clash(M,sameIndividual(LI),Tab0),!,
 3166  add_to_abox(A0,(sameIndividual(LI),Expl),A1),
 3167  add_to_clashes(C0,sameIndividual(LI),C1),
 3168  set_abox(Tab0,A1,Tab),
 3169  add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
 3170
 3171add_all_to_abox_and_clashes(M,[(differentIndividuals(LI),Expl)|T],Tab0,A0,A,C0,C):-
 3172  check_clash(M,differentIndividuals(LI),Tab0),!,
 3173  add_to_abox(A0,(differentIndividuals(LI),Expl),A1),
 3174  add_to_clashes(C0,differentIndividuals(LI),C1),
 3175  set_abox(Tab0,A1,Tab),
 3176  add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
 3177
 3178add_all_to_abox_and_clashes(M,[H|T],Tab0,A0,A,C0,C):-
 3179  add_to_abox(A0,H,A1),
 3180  set_abox(Tab0,A1,Tab),
 3181  add_all_to_abox_and_clashes(M,T,Tab,A1,A,C0,C).
 3182
 3183add_all_to_abox([],A,A).
 3184
 3185add_all_to_abox([H|T],A0,A):-
 3186  add_to_abox(A0,H,A1),
 3187  add_all_to_abox(T,A1,A).
 3188
 3189/* ************** */
 3190
 3191
 3192
 3193% ===================================
 3194% EXPANSION QUEUE
 3195% ===================================
 3196
 3197
 3198
 3199% ------------
 3200% Utility for rule application
 3201% ------------
 3202update_expansion_queue_in_tableau(M,C,Ind,Tab0,Tab):-
 3203  get_expansion_queue(Tab0,ExpansionQueue0),
 3204  update_expansion_queue(M,C,Ind,ExpansionQueue0,ExpansionQueue),
 3205  set_expansion_queue(Tab0,ExpansionQueue,Tab).
 3206
 3207update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab0,Tab):-
 3208  get_expansion_queue(Tab0,ExpansionQueue0),
 3209  update_expansion_queue(M,P,Ind1,Ind2,ExpansionQueue0,ExpansionQueue),
 3210  set_expansion_queue(Tab0,ExpansionQueue,Tab).
 3211
 3212
 3213
 3214update_expansion_queue(_,unionOf(L),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
 3215  delete(NDQ0,[unionOf(L),Ind],NDQ1),
 3216  append(NDQ1,[[unionOf(L),Ind]],NDQ).
 3217
 3218update_expansion_queue(_,maxCardinality(N,S,C),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
 3219  delete(NDQ0,[maxCardinality(N,S,C),Ind],NDQ1),
 3220  append(NDQ1,[[maxCardinality(N,S,C),Ind]],NDQ).
 3221
 3222update_expansion_queue(_,maxCardinality(N,S),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
 3223  delete(NDQ0,[maxCardinality(N,S),Ind],NDQ1),
 3224  append(NDQ1,[[maxCardinality(N,S),Ind]],NDQ).
 3225
 3226update_expansion_queue(_,exactCardinality(N,S,C),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
 3227  delete(NDQ0,[exactCardinality(N,S,C),Ind],NDQ1),
 3228  append(NDQ1,[[exactCardinality(N,S,C),Ind]],NDQ).
 3229
 3230update_expansion_queue(_,exactCardinality(N,S),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
 3231  delete(NDQ0,[exactCardinality(N,S),Ind],NDQ1),
 3232  append(NDQ1,[[exactCardinality(N,S),Ind]],NDQ).
 3233
 3234update_expansion_queue(_,C,Ind,[DQ0,NDQ],[DQ,NDQ]):-!,
 3235  delete(DQ0,[C,Ind],DQ1),
 3236  append(DQ1,[[C,Ind]],DQ).
 3237
 3238update_expansion_queue(_,P,Ind1,Ind2,[DQ0,NDQ],[DQ,NDQ]):-!,
 3239  delete(DQ0,[P,Ind1,Ind2],DQ1),
 3240  append(DQ1,[[P,Ind1,Ind2]],DQ).
 3241
 3242
 3243init_expansion_queue(LCA,LPA,EQ):-
 3244  empty_expansion_queue(EmptyEQ),
 3245  add_classes_expqueue(LCA,EmptyEQ,EQ0),
 3246  add_prop_expqueue(LPA,EQ0,EQ).
 3247
 3248add_classes_expqueue([],EQ,EQ).
 3249
 3250add_classes_expqueue([(classAssertion(C,I),_)|T],EQ0,EQ):-
 3251  update_expansion_queue(_,C,I,EQ0,EQ1),
 3252  add_classes_expqueue(T,EQ1,EQ).
 3253
 3254add_prop_expqueue([],EQ,EQ).
 3255
 3256add_prop_expqueue([(propertyAssertion(P,S,O),_)|T],EQ0,EQ):-
 3257  update_expansion_queue(_,P,S,O,EQ0,EQ1),
 3258  add_prop_expqueue(T,EQ1,EQ).
 3259
 3260
 3261
 3262
 3263% ===================================
 3264% TABS
 3265% ===================================
 3266
 3267/*
 3268  initialize the tableau
 3269  tableau is composed of:
 3270  	a directed graph T => tableau without label
 3271  	a red black tree RBN => each node is a pair of inds that contains the label for the edge
 3272  	a red black tree RBR => each node is a property that contains the pairs of inds
 3273*/
 3274new_tabs(([],ItR,RtI)):-
 3275  rb_new(ItR),
 3276  rb_new(RtI).
 3277
 3278/*
 3279  adds nodes and edges to tabs given axioms
 3280*/
 3281create_tabs(L,Tableau0,Tableau):-
 3282  get_tabs(Tableau0,Tabs0),
 3283  create_tabs_int(L,Tabs0,Tabs),
 3284  set_tabs(Tableau0,Tabs,Tableau).
 3285
 3286
 3287create_tabs_int([],G,G).
 3288  
 3289create_tabs_int([(propertyAssertion(P,S,O),_Expl)|T],Tabl0,Tabl):-
 3290  add_edge_int(P,S,O,Tabl0,Tabl1),
 3291  create_tabs_int(T,Tabl1,Tabl).
 3292  
 3293create_tabs_int([(differentIndividuals(Ld),_Expl)|Tail],(T0,RBN,RBR),Tabs):-
 3294  add_vertices(T0,Ld,T1),
 3295  create_tabs_int(Tail,(T1,RBN,RBR),Tabs).
 3296
 3297create_tabs_int([(classAssertion(_,I),_Expl)|Tail],(T0,RBN,RBR),Tabs):-
 3298  add_vertices(T0,[I],T1),
 3299  create_tabs_int(Tail,(T1,RBN,RBR),Tabs).
 3300
 3301
 3302/*
 3303  add edge to tableau
 3304
 3305  add_edge(Property,Subject,Object,Tab0,Tab)
 3306*/
 3307add_edge(P,S,O,Tableau0,Tableau):-
 3308  get_tabs(Tableau0,Tabs0),
 3309  add_edge_int(P,S,O,Tabs0,Tabs),
 3310  set_tabs(Tableau0,Tabs,Tableau).
 3311
 3312add_edge_int(P,S,O,(T0,ItR0,RtI0),(T1,ItR1,RtI1)):-
 3313  add_node_to_tree(P,S,O,ItR0,ItR1),
 3314  add_role_to_tree(P,S,O,RtI0,RtI1),
 3315  add_edge_to_tabl(P,S,O,T0,T1).
 3316
 3317add_node_to_tree(P,S,O,RB0,RB1):-
 3318  rb_lookup((S,O),V,RB0),
 3319  \+ member(P,V),!,
 3320  rb_update(RB0,(S,O),[P|V],RB1).
 3321
 3322add_node_to_tree(P,S,O,RB0,RB0):-
 3323  rb_lookup((S,O),V,RB0),
 3324  member(P,V),!.
 3325
 3326add_node_to_tree(P,S,O,RB0,RB1):-
 3327  \+ rb_lookup([S,O],_,RB0),!,
 3328  rb_insert(RB0,(S,O),[P],RB1).
 3329
 3330add_role_to_tree(P,S,O,RB0,RB1):-
 3331  rb_lookup(P,V,RB0),
 3332  \+ member((S,O),V),!,
 3333  rb_update(RB0,P,[(S,O)|V],RB1).
 3334
 3335add_role_to_tree(P,S,O,RB0,RB0):-
 3336  rb_lookup(P,V,RB0),
 3337  member((S,O),V),!.
 3338
 3339add_role_to_tree(P,S,O,RB0,RB1):-
 3340  \+ rb_lookup(P,_,RB0),!,
 3341  rb_insert(RB0,P,[(S,O)],RB1).
 3342
 3343add_edge_to_tabl(_R,Ind1,Ind2,T0,T0):-
 3344  graph_edge(Ind1,Ind2,T0),!.
 3345
 3346add_edge_to_tabl(_R,Ind1,Ind2,T0,T1):-
 3347  add_edges(T0,[Ind1-Ind2],T1).
 3348
 3349
 3350
 3351/*
 3352  check for an edge
 3353*/
 3354graph_edge(Ind1,Ind2,T0):-
 3355  edges(T0, Edges),
 3356  member(Ind1-Ind2, Edges),!.
 3357
 3358%graph_edge(_,_,_).
 3359
 3360/*
 3361  remove edges and nodes from tableau
 3362
 3363  To remove a node from the tableau use remove_node(Node,Tabs0,Tabs)
 3364*/
 3365
 3366% remove_all_nodes_from_tree(Property,Subject,Object,RBN0,RBN)
 3367% removes from RBN the pair key-values with key (Subject,Object)
 3368% key (Subject,Object) exists
 3369remove_all_nodes_from_tree(_P,S,O,RB0,RB1):-
 3370  rb_lookup((S,O),_,RB0),
 3371  rb_delete(RB0,(S,O),RB1).
 3372
 3373% key (Subject,Object) does not exist
 3374remove_all_nodes_from_tree(_P,S,O,RB0,_RB1):-
 3375  \+ rb_lookup((S,O),_,RB0).
 3376% ----------------
 3377
 3378% remove_role_from_tree(Property,Subject,Object,RBR0,RBR)
 3379% remove in RBR the pair (Subject,Object) from the value associated with key Property
 3380% pair (Subject,Object) does not exist for key Property
 3381remove_role_from_tree(P,S,O,RB,RB):-
 3382  rb_lookup(P,V,RB),
 3383  \+ member((S,O),V).
 3384
 3385% pair (Subject,Object) exists for key Property but it is not the only pair associated to it
 3386remove_role_from_tree(P,S,O,RB0,RB1):-
 3387  rb_lookup(P,V,RB0),
 3388  member((S,O),V),
 3389  delete(V,(S,O),V1),
 3390  dif(V1,[]),
 3391  rb_update(RB0,P,V1,RB1).
 3392
 3393% pair (Subject,Object) exists for key Property and it is the only pair associated to it
 3394remove_role_from_tree(P,S,O,RB0,RB1):-
 3395  rb_lookup(P,V,RB0),
 3396  member((S,O),V),
 3397  delete(V,(S,O),V1),
 3398  V1==[],
 3399  rb_delete(RB0,P,RB1).
 3400% ----------------
 3401
 3402% remove_edge_from_table(Property,Subject,Object,Tab0,Tab)
 3403% removes from T the edge from Subject to Object
 3404remove_edge_from_table(_P,S,O,T,T):-
 3405  \+ graph_edge(S,O,T).
 3406
 3407remove_edge_from_table(_P,S,O,T0,T1):-
 3408  graph_edge(S,O,T0),
 3409  del_edges(T0,[S-O],T1).
 3410% ----------------
 3411
 3412% remove_node_from_table(Subject,Tab0,Tab)
 3413% removes from T the node corresponding to Subject
 3414remove_node_from_table(S,T0,T1):-
 3415  del_vertices(T0,[S],T1).
 3416
 3417
 3418
 3419
 3420
 3421% ===================================
 3422% FUNCTIONS ON ABOX AND TABS
 3423% ===================================
 3424
 3425/*
 3426 * merge
 3427 * 
 3428 * Implement the Merge operation of the tableau. Merge two individuals
 3429 */
 3430% The first three are needed because T in tabs:(T,RBN,RBR) saves sameIndividuals
 3431% as a list instead of a single individual sameIndividual(L).
 3432% The addition of sameIndividual is made after, during the update of the ABox.
 3433% TODO: it could be improved!
 3434/*
 3435merge(M,sameIndividual(LX),sameIndividual(LY),Expl,Tableau0,Tableau):-
 3436  !,
 3437  get_tabs(Tableau0,Tabs0),
 3438  merge_tabs(L,Y,Tabs0,Tabs),
 3439  get_abox(Tableau0,ABox0),
 3440  merge_abox(M,L,Y,Expl,ABox0,ABox),
 3441  set_tabs(Tableau0,Tabs,Tableau1),
 3442  set_abox(Tableau1,ABox,Tableau).
 3443
 3444merge(M,sameIndividual(L),Y,Expl,Tableau0,Tableau):-
 3445  !,
 3446  get_tabs(Tableau0,Tabs0),
 3447  merge_tabs(L,Y,Tabs0,Tabs),
 3448  get_abox(Tableau0,ABox0),
 3449  merge_abox(M,L,Y,Expl,ABox0,ABox),
 3450  set_tabs(Tableau0,Tabs,Tableau1),
 3451  set_abox(Tableau1,ABox,Tableau).
 3452*/
 3453
 3454merge(M,X,Y,Expl,Tableau0,Tableau):-
 3455  !,
 3456  get_tabs(Tableau0,Tabs0),
 3457  merge_tabs(X,Y,Tabs0,Tabs),
 3458  get_abox(Tableau0,ABox0),
 3459  flatten([X,Y],L0),
 3460  sort(L0,L),
 3461  list_as_sameIndividual(L,SI),
 3462  get_clashes(Tableau0,Clashes0),
 3463  merge_abox(M,L,SI,Expl,ABox0,ABox,ClashesToCheck),
 3464  set_abox(Tableau0,ABox,Tableau1),
 3465  check_merged_classes(M,ClashesToCheck,Tableau1,NewClashes),
 3466  update_clashes_after_merge(M,L,SI,Tableau1,Clashes0,ClashesAM),
 3467  append(NewClashes,ClashesAM,Clashes),
 3468  set_tabs(Tableau1,Tabs,Tableau2),
 3469  set_clashes(Tableau2,Clashes,Tableau3),
 3470  get_expansion_queue(Tableau3,ExpQ0),
 3471  update_expansion_queue_after_merge(L,SI,ExpQ0,ExpQ),
 3472  set_expansion_queue(Tableau3,ExpQ,Tableau).
 3473
 3474
 3475/*
 3476 * merge node in tableau. X and Y single individuals
 3477 */
 3478
 3479merge_tabs(X,Y,(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3480  (neighbours(X,T0,LSX0)*->assign(LSX0,LSX);assign([],LSX)),
 3481  (neighbours(Y,T0,LSY0)*->assign(LSY0,LSY);assign([],LSY)),
 3482  transpose_ugraph(T0,TT),
 3483  (neighbours(X,TT,LPX0)*->assign(LPX0,LPX);assign([],LPX)),
 3484  (neighbours(Y,TT,LPY0)*->assign(LPY0,LPY);assign([],LPY)),
 3485  % list_as_sameIndividual([X,Y],SI), %TODO
 3486  flatten([X,Y],L0),
 3487  sort(L0,SI),
 3488  set_predecessor(SI,X,LPX,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),!,
 3489  set_successor(SI,X,LSX,(T1,RBN1,RBR1),(T2,RBN2,RBR2)),!,
 3490  set_predecessor(SI,Y,LPY,(T2,RBN2,RBR2),(T3,RBN3,RBR3)),!,
 3491  set_successor(SI,Y,LSY,(T3,RBN3,RBR3),(T4,RBN4,RBR4)),!,
 3492  remove_nodes(X,Y,(T4,RBN4,RBR4),(T,RBN,RBR)).
 3493
 3494remove_nodes(X,Y,Tabs0,Tabs):-
 3495  remove_node(X,Tabs0,Tabs1),
 3496  remove_node(Y,Tabs1,Tabs).
 3497
 3498% Collects all the connected in input (LP, predecessor) or in output (LS, successor) for node X
 3499% removes from RBN (remove_all_nodes_from_tree) all the pairs key-value where the key contains node X (pairs (X,Ind1) and (Ind1,X))
 3500% and from RBR (remove_edges->remove_role_from_tree) all the pairs containing X from the values of the roles entering in or exiting from X
 3501remove_node(X,(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3502  (neighbours(X,T0,LS0)*->assign(LS0,LS);assign([],LS)),
 3503  transpose_ugraph(T0,TT),
 3504  (neighbours(X,TT,LP0)*->assign(LP0,LP);assign([],LP)),
 3505  remove_node1(X,LS,RBN0,RBR0,RBN1,RBR1),
 3506  remove_node2(X,LP,RBN1,RBR1,RBN,RBR),
 3507  (vertices(T0,VS),member(X,VS)*->del_vertices(T0,[X],T);assign(T0,T)).
 3508
 3509remove_node1(_,[],RBN,RBR,RBN,RBR).
 3510
 3511remove_node1(X,[H|T],RBN0,RBR0,RBN,RBR):-
 3512  rb_lookup((X,H),V,RBN0),
 3513  remove_edges(V,X,H,RBR0,RBR1),
 3514  remove_all_nodes_from_tree(_,X,H,RBN0,RBN1),
 3515  remove_node1(X,T,RBN1,RBR1,RBN,RBR).
 3516
 3517remove_node2(_,[],RBN,RBR,RBN,RBR).
 3518
 3519remove_node2(X,[H|T],RBN0,RBR0,RBN,RBR):-
 3520  rb_lookup((H,X),V,RBN0),
 3521  remove_edges(V,H,X,RBR0,RBR1),
 3522  remove_all_nodes_from_tree(_,H,X,RBN0,RBN1),
 3523  remove_node1(X,T,RBN1,RBR1,RBN,RBR).
 3524
 3525remove_edges([],_,_,RBR,RBR).
 3526
 3527remove_edges([H|T],S,O,RBR0,RBR):-
 3528  remove_role_from_tree(H,S,O,RBR0,RBR1),
 3529  remove_edges(T,S,O,RBR1,RBR).
 3530
 3531
 3532set_predecessor(_NN,_,[],Tabs,Tabs).
 3533
 3534set_predecessor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3535  rb_lookup((H,X),LR,RBN0),
 3536  set_predecessor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
 3537  set_predecessor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
 3538
 3539set_predecessor1(_NN,_H,[],Tabs,Tabs).
 3540
 3541set_predecessor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3542  add_edge_int(R,H,NN,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
 3543  set_predecessor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
 3544
 3545set_successor(_NN,_X,[],Tabs,Tabs).
 3546
 3547set_successor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3548  rb_lookup((X,H),LR,RBN0),
 3549  set_successor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
 3550  set_successor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
 3551
 3552set_successor1(_NN,_H,[],Tabs,Tabs).
 3553
 3554set_successor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
 3555  add_edge_int(R,NN,H,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
 3556  set_successor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
 3557
 3558/*
 3559  merge node in ABox
 3560*/
 3561
 3562% TODO update
 3563merge_abox(_M,_L,_,_,[],[],[]).
 3564
 3565merge_abox(M,L,SI,Expl0,[(classAssertion(C,Ind),ExplT)|T],[(classAssertion(C,SI),Expl)|ABox],[C-SI|CTC]):-
 3566  member(Ind,L),!,
 3567  and_f(M,Expl0,ExplT,Expl),
 3568  %and_f_ax(M,sameIndividual(L),Expl1,Expl),
 3569  merge_abox(M,L,SI,Expl0,T,ABox,CTC).
 3570
 3571merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,SI,Ind2),Expl)|ABox],CTC):-
 3572  member(Ind1,L),!,
 3573  and_f(M,Expl0,ExplT,Expl),
 3574  %and_f_ax(M,sameIndividual(L),Expl1,Expl),
 3575  merge_abox(M,L,SI,Expl0,T,ABox,CTC).
 3576
 3577merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,Ind1,SI),Expl)|ABox],CTC):-
 3578  member(Ind2,L),!,
 3579  and_f(M,Expl0,ExplT,Expl),
 3580  %and_f_ax(M,sameIndividual(L),Expl1,Expl),
 3581  merge_abox(M,L,SI,Expl0,T,ABox,CTC).
 3582
 3583merge_abox(M,L,SI,Expl0,[H|T],[H|ABox],CTC):-
 3584  merge_abox(M,L,SI,Expl0,T,ABox,CTC).
 3585
 3586
 3587/*
 3588  check for new clashes due to merge
 3589 */
 3590
 3591check_merged_classes(_,[],_,[]).
 3592
 3593check_merged_classes(M,[ToCheck|TC],Tab,[ToCheck|NewClashes]):-
 3594  check_clash(M,ToCheck,Tab),!,
 3595  check_merged_classes(M,TC,Tab,NewClashes).
 3596
 3597check_merged_classes(M,[_ToCheck|TC],Tab,NewClashes):-
 3598  check_merged_classes(M,TC,Tab,NewClashes).
 3599
 3600/*
 3601 update clashes ofter merge
 3602 substitute ind in clashes with sameIndividual
 3603 */
 3604
 3605update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes):-
 3606  update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes,0).
 3607
 3608% if last argument is 0 -> need to theck clash for sameIndividual/differentIndividual
 3609% if there is no clash (check_clash returns false), backtrack to (*)
 3610update_clashes_after_merge(M,_,SI,Tableau,[],[SI],0):-
 3611  check_clash(M,SI,Tableau),!.
 3612
 3613% (*)
 3614update_clashes_after_merge(_,_,_,_,[],[],_).
 3615
 3616update_clashes_after_merge(M,L,SI,Tableau,[sameIndividual(LC)|TC0],[SI|TC],0):-
 3617  memberchk(I,L),
 3618  memberchk(I,LC),!,
 3619  update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,1).
 3620
 3621update_clashes_after_merge(M,L,SI,Tableau,[C-I|TC0],[C-SI|TC],UpdatedSI):-
 3622  memberchk(I,L),!,
 3623  update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
 3624
 3625update_clashes_after_merge(M,L,SI,Tableau,[C-sameIndividual(LOld)|TC0],[C-SI|TC],UpdatedSI):-
 3626  memberchk(I,L),
 3627  memberchk(I,LOld),!,
 3628  update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
 3629
 3630update_clashes_after_merge(M,L,SI,Tableau,[Clash|TC0],[Clash|TC],UpdatedSI):-
 3631  update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
 3632
 3633
 3634
 3635
 3636/*
 3637 update expansion queue ofter merge
 3638 substitute ind in expansion queue with sameIndividual
 3639 */
 3640update_expansion_queue_after_merge(L,SI,[ExpQD0,ExpQND0],[ExpQD,ExpQND]):-
 3641  update_expansion_queue_after_merge_int(L,SI,ExpQD0,ExpQD),
 3642  update_expansion_queue_after_merge_int(L,SI,ExpQND0,ExpQND).
 3643
 3644update_expansion_queue_after_merge_int(_,_,[],[]).
 3645
 3646update_expansion_queue_after_merge_int(L,SI,[[C,I]|TC0],[[C,IN]|TC]):-
 3647  substitute_individual(L,I,SI,IN),
 3648  update_expansion_queue_after_merge_int(L,SI,TC0,TC).
 3649
 3650update_expansion_queue_after_merge_int(L,SI,[[P,S,O]|TC0],[[P,SN,ON]|TC]):-
 3651  substitute_individual(L,S,SI,SN),
 3652  substitute_individual(L,O,SI,ON),
 3653  update_expansion_queue_after_merge_int(L,SI,TC0,TC).
 3654
 3655substitute_individual(L,sameIndividual(LSI),SI,SI):-
 3656  memberchk(I,L),
 3657  memberchk(I,LSI),!.
 3658
 3659substitute_individual(_,I,_,I):-!.
 3660
 3661
 3662
 3663% ==================================================================================================================
 3664
 3665/*
 3666sandbox:safe_primitive(trill:sub_class(_,_)).
 3667sandbox:safe_primitive(trill:sub_class(_,_,_)).
 3668sandbox:safe_primitive(trill:prob_sub_class(_,_,_)).
 3669sandbox:safe_primitive(trill:instanceOf(_,_)).
 3670sandbox:safe_primitive(trill:instanceOf(_,_,_)).
 3671sandbox:safe_primitive(trill:prob_instanceOf(_,_,_)).
 3672sandbox:safe_primitive(trill:property_value(_,_,_)).
 3673sandbox:safe_primitive(trill:property_value(_,_,_,_)).
 3674sandbox:safe_primitive(trill:prob_property_value(_,_,_,_)).
 3675sandbox:safe_primitive(trill:unsat(_)).
 3676sandbox:safe_primitive(trill:unsat(_,_)).
 3677sandbox:safe_primitive(trill:prob_unsat(_,_)).
 3678sandbox:safe_primitive(trill:inconsistent_theory).
 3679sandbox:safe_primitive(trill:inconsistent_theory(_)).
 3680sandbox:safe_primitive(trill:prob_inconsistent_theory(_)).
 3681sandbox:safe_primitive(trill:axiom(_)).
 3682sandbox:safe_primitive(trill:add_kb_prefix(_,_)).
 3683sandbox:safe_primitive(trill:add_kb_prefixes(_)).
 3684sandbox:safe_primitive(trill:add_axiom(_)).
 3685sandbox:safe_primitive(trill:add_axioms(_)).
 3686sandbox:safe_primitive(trill:load_kb(_)).
 3687sandbox:safe_primitive(trill:load_owl_kb(_)).
 3688*/
 3689
 3690:- multifile sandbox:safe_meta/2. 3691
 3692sandbox:safe_meta(trill:sub_class(_,_),[]).
 3693sandbox:safe_meta(trill:sub_class(_,_,_),[]).
 3694sandbox:safe_meta(trill:sub_class(_,_,_,_),[]).
 3695sandbox:safe_meta(trill:all_sub_class(_,_,_),[]).
 3696sandbox:safe_meta(trill:prob_sub_class(_,_,_),[]).
 3697sandbox:safe_meta(trill:instanceOf(_,_),[]).
 3698sandbox:safe_meta(trill:instanceOf(_,_,_),[]).
 3699sandbox:safe_meta(trill:instanceOf(_,_,_,_),[]).
 3700sandbox:safe_meta(trill:all_instanceOf(_,_,_),[]).
 3701sandbox:safe_meta(trill:prob_instanceOf(_,_,_),[]).
 3702sandbox:safe_meta(trill:property_value(_,_,_),[]).
 3703sandbox:safe_meta(trill:property_value(_,_,_,_),[]).
 3704sandbox:safe_meta(trill:property_value(_,_,_,_,_),[]).
 3705sandbox:safe_meta(trill:all_property_value(_,_,_,_),[]).
 3706sandbox:safe_meta(trill:prob_property_value(_,_,_,_),[]).
 3707sandbox:safe_meta(trill:unsat(_),[]).
 3708sandbox:safe_meta(trill:unsat(_,_),[]).
 3709sandbox:safe_meta(trill:unsat(_,_,_),[]).
 3710sandbox:safe_meta(trill:all_unsat(_,_),[]).
 3711sandbox:safe_meta(trill:prob_unsat(_,_),[]).
 3712sandbox:safe_meta(trill:inconsistent_theory,[]).
 3713sandbox:safe_meta(trill:inconsistent_theory(_),[]).
 3714sandbox:safe_meta(trill:inconsistent_theory(_,_),[]).
 3715sandbox:safe_meta(trill:all_inconsistent_theory(_),[]).
 3716sandbox:safe_meta(trill:prob_inconsistent_theory(_),[]).
 3717sandbox:safe_meta(trill:axiom(_),[]).
 3718sandbox:safe_meta(trill:kb_prefixes(_),[]).
 3719sandbox:safe_meta(trill:add_kb_prefix(_,_),[]).
 3720sandbox:safe_meta(trill:add_kb_prefixes(_),[]).
 3721sandbox:safe_meta(trill:remove_kb_prefix(_,_),[]).
 3722sandbox:safe_meta(trill:remove_kb_prefix(_),[]).
 3723sandbox:safe_meta(trill:add_axiom(_),[]).
 3724sandbox:safe_meta(trill:add_axioms(_),[]).
 3725sandbox:safe_meta(trill:load_kb(_),[]).
 3726sandbox:safe_meta(trill:load_owl_kb(_),[]).
 3727sandbox:safe_meta(trill:set_tableau_expansion_rules(_,_),[]).
 3728
 3729:- use_module(library(utility_translation)). 3730
 3731user:term_expansion((:- trill),[]):-
 3732  utility_translation:get_module(M),
 3733  set_algorithm(M:trill),
 3734  set_up(M),
 3735  utility_translation:set_up_kb_loading(M),
 3736  trill:add_kb_prefixes(M:[('disponte'='http://ml.unife.it/disponte#'),('owl'='http://www.w3.org/2002/07/owl#')]).
 3737
 3738user:term_expansion((:- trillp),[]):-
 3739  utility_translation:get_module(M),
 3740  set_algorithm(M:trillp),
 3741  set_up(M),
 3742  utility_translation:set_up_kb_loading(M),
 3743  trill:add_kb_prefixes(M:['disponte'='http://ml.unife.it/disponte#','owl'='http://www.w3.org/2002/07/owl#']).
 3744
 3745user:term_expansion((:- tornado),[]):-
 3746  utility_translation:get_module(M),
 3747  set_algorithm(M:tornado),
 3748  set_up(M),
 3749  utility_translation:set_up_kb_loading(M),
 3750  trill:add_kb_prefixes(M:['disponte'='http://ml.unife.it/disponte#','owl'='http://www.w3.org/2002/07/owl#'])