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*********************************/
100load_kb(FileName):-
101 user:consult(FileName).
109load_owl_kb(FileName):-
110 load_owl(FileName).
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.
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.
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 216prologmessage(iri_not_exists(IRIs)) --> 217 [ 'IRIs not existent or wrong argument: ~w' -[IRIs] ]. 218 219prologmessage(inconsistent) --> 220 [ 'Inconsistent ABox' ]. 221 222prologmessage(consistent) --> 223 [ 'Consistent ABox' ]. 224 225prologmessage(wrong_number_max_expl) --> 226 [ 'max_expl option can take integer values or "all"' ]. 227 228prologmessage(timeout_reached) --> 229 [ 'Timeout reached' ]. 230 231/***************************** 232 QUERY OPTIONS 233******************************/
Options can be:
assert_abox(Boolean)
if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1return_prob(Prob)
if present the probability of the query is computed and unified with Probreturn_single_prob(Boolean)
must be used with return_prob(Prob)
. It forces TRILL to return the probability of each single explanationmax_expl(Value)
to limit the maximum number of explanations to find. Value must be an integer. The predicate will return a list containing at most Value different explanationstime_limit(Value)
to limit the time for the inference. The predicate will return the explanations found in the time allowed. Value is the number of seconds allowed for the search of explanations*/
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 ***********/
512instanceOf(M:Class,Ind,Expl,Opt):-
513 execute_query(M,io,[Class,Ind],Expl,Opt),
514 is_expl(M,Expl).
526instanceOf(M:Class,Ind,Expl):-
527 instanceOf(M:Class,Ind,Expl,[]),
528 is_expl(M,Expl).
539all_instanceOf(M:Class,Ind,Expl):-
540 execute_query(M,io,[Class,Ind],Expl,[max_expl(all)]),
541 is_expl(M,Expl).
550instanceOf(M:Class,Ind):-
551 execute_query(M,io,[Class,Ind],Expl,[max_expl(1)]),!,
552 is_expl(M,Expl).
assert_abox(Boolean)
if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1return_prob(Prob)
if present the probability of the query is computed and unified with Prob/
566property_value(M:Prop, Ind1, Ind2,Expl,Opt):-
567 execute_query(M,pv,[Prop, Ind1, Ind2],Expl,Opt),
568 is_expl(M,Expl).
578property_value(M:Prop, Ind1, Ind2,Expl):-
579 property_value(M:Prop, Ind1, Ind2,Expl,[]),
580 is_expl(M,Expl).
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).
600property_value(M:Prop, Ind1, Ind2):-
601 execute_query(M,pv,[Prop, Ind1, Ind2],Expl,[max_expl(1)]),!,
602 is_expl(M,Expl).
assert_abox(Boolean)
if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1return_prob(Prob)
if present the probability of the query is computed and unified with Prob/
617sub_class(M:Class,SupClass,Expl,Opt):-
618 execute_query(M,sc,[Class,SupClass],Expl,Opt),
619 is_expl(M,Expl).
630sub_class(M:Class,SupClass,Expl):-
631 sub_class(M:Class,SupClass,Expl,[]),
632 is_expl(M,Expl).
643all_sub_class(M:Class,SupClass,Expl):-
644 execute_query(M,sc,[Class,SupClass],Expl,[max_expl(all)]),
645 is_expl(M,Expl).
653sub_class(M:Class,SupClass):-
654 execute_query(M,sc,[Class,SupClass],Expl,[max_expl(1)]),!,
655 is_expl(M,Expl).
assert_abox(Boolean)
if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1return_prob(Prob)
if present the probability of the query is computed and unified with Prob/
669unsat(M:Concept,Expl,Opt):-
670 execute_query(M,un,[Concept],Expl,Opt),
671 is_expl(M,Expl).
681unsat(M:Concept,Expl):-
682 unsat(M:Concept,Expl,[]),
683 is_expl(M,Expl).
693all_unsat(M:Concept,Expl):-
694 execute_query(M,un,[Concept],Expl,[max_expl(all)]),
695 is_expl(M,Expl).
703unsat(M:Concept):-
704 execute_query(M,un,[Concept],Expl,[max_expl(1)]),!,
705 is_expl(M,Expl).
assert_abox(Boolean)
if Boolean is set to true the list of aboxes is asserted with the predicate final_abox/1return_prob(Prob)
if present the probability of the query is computed and unified with Prob/
716inconsistent_theory(M:Expl,Opt):-
717 execute_query(M,it,[],Expl,Opt),
718 is_expl(M,Expl).
725inconsistent_theory(M:Expl):-
726 inconsistent_theory(M:Expl,[]),
727 is_expl(M,Expl).
736all_inconsistent_theory(M:Expl):-
737 execute_query(M,it,[],Expl,[max_expl(all)]),
738 is_expl(M,Expl).
745inconsistent_theory:-
746 get_trill_current_module(M),
747 execute_query(M,it,[],Expl,[max_expl(1)]),!,
748 is_expl(M,Expl).
757prob_instanceOf(M:Class,Ind,Prob):-
758 instanceOf(M:Class,Ind,_,[return_prob(Prob)]).
766prob_property_value(M:Prop, Ind1, Ind2,Prob):-
767 property_value(M:Prop, Ind1, Ind2,_,[return_prob(Prob)]).
776prob_sub_class(M:Class,SupClass,Prob):-
777 sub_class(M:Class,SupClass,_,[return_prob(Prob)]).
786prob_unsat(M:Concept,Prob):-
787 unsat(M:Concept,_,[return_prob(Prob)]).
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 */
3025new_tableau(tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}):-
3026 new_abox(ABox),
3027 new_tabs(Tabs),
3028 empty_expansion_queue(ExpansionQueue).
3036init_tableau(ABox,Tabs,tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}):-
3037 empty_expansion_queue(ExpansionQueue).
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 3731userterm_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 3738userterm_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 3745userterm_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#'])
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.