trillo

This module is based on TRILL version 6.0.2.

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

author: - Riccardo Zese
version: - 1.0.0
copyright: - Riccardo Zese */
license: - Artistic License 2.0

15:- module(trillo,[sub_class/2, sub_class/3, prob_sub_class/3, sub_class/4, all_sub_class/3, 16 instanceOf/2, instanceOf/3, prob_instanceOf/3, instanceOf/4, all_instanceOf/3, 17 property_value/3, property_value/4, prob_property_value/4, property_value/5, all_property_value/4, 18 unsat/1, unsat/2, prob_unsat/2, unsat/3, all_unsat/2, 19 inconsistent_theory/0, inconsistent_theory/1, prob_inconsistent_theory/1, inconsistent_theory/2, all_inconsistent_theory/1, 20 resume_query/1, compute_query_prob/1, reset_query/0, 21 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, 22 load_kb/1, load_owl_kb/1, load_owl_kb_from_string/1, set_tableau_expansion_rules/2, 23 build_and_expand/3, instanceOf_meta/6,property_value_meta/7, 24 init_oracle/1] ). 25 26:- meta_predicate sub_class(:,+). 27:- meta_predicate sub_class(:,+,-). 28:- meta_predicate sub_class(:,+,-,+). 29:- meta_predicate all_sub_class(:,+,-). 30:- meta_predicate prob_sub_class(:,+,-). 31:- meta_predicate instanceOf(:,+). 32:- meta_predicate instanceOf(:,+,-). 33:- meta_predicate instanceOf(:,+,-,+). 34:- meta_predicate all_instanceOf(:,+,-). 35:- meta_predicate prob_instanceOf(:,+,-). 36:- meta_predicate property_value(:,+,+). 37:- meta_predicate property_value(:,+,+,-). 38:- meta_predicate property_value(:,+,+,-,+). 39:- meta_predicate all_property_value(:,+,+,-). 40:- meta_predicate prob_property_value(:,+,+,-). 41:- meta_predicate unsat(:). 42:- meta_predicate unsat(:,-). 43:- meta_predicate unsat(:,-,+). 44:- meta_predicate all_unsat(:,-). 45:- meta_predicate prob_unsat(:,-). 46:- meta_predicate inconsistent_theory(:). 47:- meta_predicate inconsistent_theory(:,+). 48:- meta_predicate all_inconsistent_theory(:). 49:- meta_predicate prob_inconsistent_theory(:). 50:- meta_predicate resume_query(:). 51:- meta_predicate compute_query_prob(:). 52:- meta_predicate axiom(:). 53:- meta_predicate kb_prefixes(:). 54:- meta_predicate add_kb_prefix(:,+). 55:- meta_predicate add_kb_prefixes(:). 56:- meta_predicate add_axiom(:). 57:- meta_predicate add_axioms(:). 58:- meta_predicate remove_kb_prefix(:,+). 59:- meta_predicate remove_kb_prefix(:). 60:- meta_predicate remove_axiom(:). 61:- meta_predicate remove_axioms(:). 62:- meta_predicate load_kb(+). 63:- meta_predicate load_owl_kb(+). 64:- meta_predicate load_owl_kb_from_string(+). 65:- meta_predicate set_algorithm(:). 66:- meta_predicate init_trillo(+). 67:- meta_predicate set_tableau_expansion_rules(:,+). 68 69:- use_module(library(lists)). 70:- use_module(library(ugraphs)). 71:- use_module(library(rbtrees)). 72:- use_module(library(dif)). 73:- use_module(library(pengines)). 74:- use_module(library(sandbox)). 75:- use_module(library(aggregate)). 76 77:- reexport(library(bddem)). 78 79:- style_check(-discontiguous). 80 81:- table instanceOf_meta(_,_,_,_,_,lattice(orc/3)),property_value_meta(_,_,_,_,_,_,lattice(orc/3)). 82 83/******************************** 84 DISPONTE IRIS 85*********************************/ 86 87disponte_iri('http://sites.google.com/a/unife.it/ml/disponte#probability'). % Retro-compatibility 88disponte_iri('https://sites.google.com/a/unife.it/ml/disponte#probability'). % Retro-compatibility 89disponte_iri('http://ml.unife.it/disponte#probability'). % Retro-compatibility 90disponte_iri('https://ml.unife.it/disponte#probability'). % Retro-compatibility 91disponte_iri('http://ai.unife.it/disponte#probability'). 92disponte_iri('https://ai.unife.it/disponte#probability'). 93 94/******************************** 95 SETTINGS 96*********************************/ 97:- multifile setting_trillo_default/2. 98setting_trillo_default(det_rules,[o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule]). 99setting_trillo_default(nondet_rules,[or_rule,max_rule,ch_rule]). 100 101set_up(M):- 102 trillo_utility_translation:set_up(M), 103 init_delta(M), 104 M:(dynamic exp_found/2, setting_trillo/2, tab_end/1, query_option/2, tab_util/2), 105 retractall(M:setting_trillo(_,_)), 106 retractall(M:query_option(_,_)), 107 retractall(M:tab_end(_)), 108 retractall(M:tab_util(_,_)). 109 %foreach(setting_trillo_default(DefaultSetting,DefaultVal),assert(M:setting_trillo(DefaultSetting,DefaultVal))). 110 111clean_up(M):- 112 trillo_utility_translation:clean_up(M), 113 M:(dynamic exp_found/2, setting_trillo/2, tab_end/1, query_option/2, tab_util/2), 114 retractall(M:exp_found(_,_)), 115 retractall(M:setting_trillo(_,_)), 116 retractall(M:query_option(_,_)), 117 retractall(M:tab_end(_)), 118 retractall(M:tab_util(_,_)). 119 %retractall(M:delta(_,_)), 120 121/******************************** 122 LOAD KNOWLEDGE BASE 123*********************************/

149load_owl_kb_from_string(String):- 150 load_owl_from_string(String). 151 152/*****************************/ 153 154/***************************** 155 UTILITY PREDICATES 156******************************/ 157%defined in trillo_utility_translation 158:- multifile add_kb_prefix/2, add_kb_prefixes/1, add_axiom/1, add_axioms/1, 159 remove_kb_prefix/2, remove_kb_prefix/1, remove_axiom/1, remove_axioms/1.

236set_tableau_expansion_rules(M:DetRules,NondetRules):- 237 retractall(M:setting_trillo(det_rules,_)), 238 retractall(M:setting_trillo(nondet_rules,_)), 239 assert(M:setting_trillo(det_rules,DetRules)), 240 assert(M:setting_trillo(nondet_rules,NondetRules)). 241 242build_and_expand(M,QueryType,QueryArgs):- 243 set_up_tableau(M), 244 collect_individuals(M,QueryType,QueryArgs,ConnectedInds), 245 dif(ConnectedInds,[]),!, 246 retractall(M:exp_found(_,_)), 247 retractall(M:tab_end(_)), 248 findall(TabInit,M:tab_util(stab,TabInit),LTab), 249 retractall(M:tab_util(stab,_)), 250 build_and_expand_int(M,LTab,ConnectedInds). 251 252build_and_expand(_M,_QueryType,_QueryArgs):-!. 253 254build_and_expand_int(M,[],ConnectedInds):-!, 255 build_abox(M,T1,ConnectedInds), 256 set_next_from_expansion_queue(T1,_,T2), 257 forall(expand_abox(M,T2,T),assert(M:tab_util(stab,T))). 258 259build_and_expand_int(M,LTab,ConnectedInds):- 260 get_axioms_of_individuals(M,ConnectedInds,LCA,LPA,LNA,LDIA,LSIA), 261 findall(Property,M:lpPropertyAssertion(Property),LPA1), 262 findall(Class,M:lpClassAssertion(Class),LCA1), 263 append([LCA,LPA,LNA,LDIA,LSIA],AddAllList), 264 expand_int(M,LTab,LCA,LCA1,LPA,LPA1,LSIA,AddAllList). 265 266expand_int(_,[],_,_,_,_,_,_):-!. 267 268expand_int(M,[T0|LTab],LCA,LCA1,LPA,LPA1,LSIA,AddAllList):- 269 get_expansion_queue(T0,ExpansionQueue0), 270 expand_expansion_queue(LCA,LCA1,LPA,LPA1,ExpansionQueue0,ExpansionQueue), 271 set_expansion_queue(T0,ExpansionQueue,T1), 272 update_abox(M,T1,T2,AddAllList,LSIA), % will expand the KB without the query 273 set_next_from_expansion_queue(T2,_EA1,T3), 274 forall(expand_abox(M,T3,T),assert(M:tab_util(stab,T))), 275 expand_int(M,LTab,LCA,LCA1,LPA,LPA1,LSIA,AddAllList). 276 277expand_abox(M,Tab,Tab):- 278 test_end_expand_queue(M,Tab),!. 279 280expand_abox(M,Tab0,Tab):- 281 extract_current_from_expansion_queue(Tab0,EA), 282 expand_by_apply_all_rules(M,Tab0,EA,Tab1), 283 expand_abox(M,Tab1,Tab). 284 285expand_by_apply_all_rules(M,Tab0,EA,Tab):- 286 M:setting_trillo(det_rules,Rules), 287 apply_det_rules(M,Rules,Tab0,EA,Tab1), 288 ( test_end_apply_rule(M,Tab0,Tab1) -> 289 set_next_from_expansion_queue(Tab1,_EA1,Tab) 290 ; 291 expand_by_apply_all_rules(M,Tab1,EA,Tab) 292 ). 293 294init_oracle(M):- 295 abolish_all_tables, 296 set_up_reasoner(M). 297 298/***************************** 299 METAINT. QUERY PREDICATES 300******************************/ 301 302instanceOf_meta(C,I,E,M,Env,BDD):- 303 retractall(M:exp_found(_,_)), 304 retractall(M:tab_end(_)), 305 build_and_expand(M,io,[C,I]), 306 M:tab_util(stab,TabInit), 307 %build_abox(M,TabInit,io,[C,I]), 308 set_up_tableau(M), 309 ((ground(C)) -> 310 add_q(M,io,TabInit,[C,I],Tab0) 311 ; 312 Tab0=TabInit 313 ), 314 %set_next_from_expansion_queue(Tab0,_,Tab1), 315 check_and_set_next_from_expansion_queue(Tab0,_EA,Tab2), 316 get_explanation(M,Tab2,E), 317 sphere:get_bdd(M,Env,E,BDD). 318 319 320property_value_meta(R,I1,I2,E,M,Env,BDD):- 321 retractall(M:exp_found(_,_)), 322 retractall(M:tab_end(_)), 323 build_and_expand(M,pv,[R,I1,I2]), 324 M:tab_util(stab,TabInit), 325 %build_abox(M,TabInit,pv,[R,I1,I2]), 326 set_up_tableau(M), 327 ((ground(R)) -> 328 add_q(M,pv,TabInit,[R,I1,I2],Tab0) 329 ; 330 Tab0=TabInit 331 ), 332 %set_next_from_expansion_queue(Tab0,_,Tab1), 333 check_and_set_next_from_expansion_queue(Tab0,_EA,Tab2), 334 get_explanation(M,Tab2,E), 335 sphere:get_bdd(M,Env,E,BDD). 336 337% Deletes axiom form all aboxes 338delete_from([],_,[]). 339 340delete_from([(ABox0,Tab)|T],Q,[(ABox,Tab)|T1]):- 341 %writel(ABox0), 342 delete(ABox0,Q,ABox1), 343 Q=(classAssertion(CA,_),_), 344 findall((classAssertion(C,I),E), 345 (member((classAssertion(C,I),E),ABox1),member(CA,E)), 346 ToRemove), 347 subtract(ABox1,ToRemove,ABox), 348 delete_from(T,Q,T1). 349 350 351/***************************** 352 MESSAGES 353******************************/ 354:- multifile prolog:message/1. 355 356prolog:message(iri_not_exists(IRIs)) --> 357 [ 'IRIs not existent or wrong argument: ~w' -[IRIs] ]. 358 359prolog:message(inconsistent) --> 360 [ 'Inconsistent ABox' ]. 361 362prolog:message(inconsistent_inc_expl) --> 363 [ 'Inconsistent ABox. Justification for the inconsistency:' ]. 364 365prolog:message(consistent) --> 366 [ 'Consistent ABox' ]. 367 368prolog:message(wrong_number_max_expl) --> 369 [ 'max_expl option can take integer values or "all"' ]. 370 371prolog:message(timeout_reached) --> 372 [ 'Timeout reached' ]. 373 374prolog:message(unknown_query_option(Option)) --> 375 [ 'Unknown query option: ~w' -[Option] ]. 376 377/***************************** 378 QUERY OPTIONS 379******************************/

393trillo_available_option(assert_abox,in). 394trillo_available_option(compute_prob,in,out). 395trillo_available_option(max_expl,in). 396trillo_available_option(time_limit,in). 397 398get_from_query_options(OptList,Option,SingleValue):- 399 trillo_available_option(Option,_),!, 400 Opt=..[Option,SingleValue], 401 memberchk(Opt,OptList). 402 403get_from_query_options(OptList,Option,Value1,Value2):- 404 trillo_available_option(Option,_,_), 405 Opt=..[Option,Value1,Value2], 406 memberchk(Opt,OptList). 407 408 409set_query_options(_,[]):- !. 410 411set_query_options(M,[QueryOption|TailQueryOptions]) :- 412 QueryOption=..[Option|Value], 413 add_trillo_query_option(M,Option,Value), 414 set_query_options(M,TailQueryOptions). 415 416add_trillo_query_option(M,Option,[ValueIn]) :- 417 trillo_available_option(Option,in),!, 418 retractall(M:query_option(Option,_)), 419 assert(M:query_option(Option,ValueIn)). 420 421add_trillo_query_option(M,Option,_ValueOut) :- 422 trillo_available_option(Option,out),!, 423 retractall(M:query_option(Option,_)), 424 assert(M:query_option(Option,true)). 425 426add_trillo_query_option(M,Option,[ValueIn,_ValueOut]) :- 427 trillo_available_option(Option,in,out),!, 428 retractall(M:query_option(Option,_)), 429 assert(M:query_option(Option,ValueIn)). 430 431add_trillo_query_option(_M,Option,_Value) :- 432 print_message(warning,unknown_query_option(Option)),!. 433 434/**************************** 435 QUERY PREDICATES 436*****************************/ 437 438execute_query(M,QueryType,QueryArgsNC,Expl,QueryOptions):- 439 check_query_args(M,QueryType,QueryArgsNC,QueryArgs), 440 set_up_reasoner(M), 441 set_query_options(M,QueryOptions),!, 442 find_explanations(M,QueryType,QueryArgs,Expl), 443 is_expl(M,Expl), 444 compute_prob_and_close(M,Expl,QueryOptions). 445 446 447% Execution monitor 448find_explanations(M,QueryType,QueryArgs,Expl):- 449 get_open_query_monitor(M,QueryType,QueryArgs), 450 get_n_explanation_monitor(M,MonitorNExpl), 451 get_time_limit_monitor(M,MonitorTimeLimit), 452 find_n_explanations(M,QueryType,QueryArgs,Expl,MonitorNExpl), 453 check_time_limit_monitor(M,MonitorTimeLimit). 454 455find_single_explanation(M,it,['inconsistent','kb'],Expl):-!, 456 build_abox(M,Tableau,it,['inconsistent','kb']), % will expand the KB without the query 457 set_up_tableau(M), 458 set_next_from_expansion_queue(Tableau,_EA,Tableau1), 459 get_explanation(M,Tableau1,Expl). 460 461find_single_explanation(M,QueryType,QueryArgs,Expl):- 462 build_abox(M,Tableau,QueryType,QueryArgs), % will expand the KB without the query 463 (absence_of_clashes(Tableau) -> % TODO if QueryType is inconsistent no check 464 ( 465 add_q(M,QueryType,Tableau,QueryArgs,Tableau0),!, 466 set_up_tableau(M), 467 set_next_from_expansion_queue(Tableau0,_EA,Tableau1), 468 get_explanation(M,Tableau1,Expl) 469 ) 470 ; 471 print_message(warning,inconsistent),!,false 472 ). 473 474/************* 475 476 Monitor predicates 477 478**************/ 479 480% Monitors 481% --- number of explanations --- 482get_n_explanation_monitor(M,MonitorNExpl):- 483 M:query_option(max_expl,MonitorNExpl),!. 484 485get_n_explanation_monitor(M,all):- 486 M:query_option(compute_prob,query),!. 487 488get_n_explanation_monitor(_M,bt):-!. 489 490 491% --- time limit --- 492get_time_limit_monitor(M,MonitorTimeLimit):- 493 M:query_option(time_limit,TimeLimit),!, 494 retractall(M:setting_trillo(timeout,_)), 495 get_time(Start), 496 MonitorTimeLimit is Start + TimeLimit, 497 assert(M:setting_trillo(timeout,MonitorTimeLimit)). 498 499get_time_limit_monitor(_M,inf):-!. 500 501check_time_limit_monitor(_M,inf):-!. % forse no cut. 502 503check_time_limit_monitor(M,MonitorTimeLimit):- 504 get_time(End), 505 End < MonitorTimeLimit,!, 506 retractall(M:query_option(time_limit,_)), 507 NewTimeLimit is MonitorTimeLimit - End, 508 assert(M:query_option(time_limit,NewTimeLimit)). 509 510check_time_limit_monitor(_M,_MonitorTimeLimit):- 511 print_message(warning,timeout_reached),false. 512 513check_time_limit_monitor_status(M):- 514 M:setting_trillo(timeout,Timeout),!, 515 get_time(Now), 516 Timeout<Now. % I must stop 517 518% --- open query --- 519get_open_query_monitor(M,QueryType,QueryArgs):- 520 retractall(M:query_option(active_query,_)), 521 assert(M:query_option(active_query,[QueryType,QueryArgs])). 522 523check_open_query_monitor_status(M,QueryType,QueryArgs):- 524 M:query_option(active_query,[QueryType,QueryArgs]),!. 525 526reset_open_query_monitor(M):- 527 retractall(M:query_option(active_query,_)). 528/* *************** */ 529 530set_up_reasoner(M):- 531 set_up(M), 532 retractall(M:exp_found(_,_)), 533 retractall(M:exp_found(_,_,_)), 534 retractall(M:trilloan_idx(_)), 535 assert(M:trilloan_idx(1)). 536 537set_up_tableau(M):- 538 % TO CHANGE move to KB loading 539 %setting_trillo_default(det_rules,DetRules), 540 %setting_trillo_default(nondet_rules,NondetRules), 541 %set_tableau_expansion_rules(M:DetRules,NondetRules). 542 prune_tableau_rules(M). 543 544% instanceOf 545add_q(M,io,Tableau0,[ClassEx,IndEx],Tableau):- !, 546 neg_class(ClassEx,NClassEx), 547 add_q(M,Tableau0,classAssertion(NClassEx,IndEx),Tableau1), 548 add_clash_to_tableau(M,Tableau1,NClassEx-IndEx,Tableau2), 549 update_expansion_queue_in_tableau(M,NClassEx,IndEx,Tableau2,Tableau),!. 550 551% property_value 552add_q(M,pv,Tableau0,[PropEx,Ind1Ex,Ind2Ex],Tableau):-!, 553 neg_class(PropEx,NPropEx), %use of neg_class to negate property 554 add_q(M,Tableau0,propertyAssertion(NPropEx,Ind1Ex,Ind2Ex),Tableau1), 555 add_clash_to_tableau(M,Tableau1,NPropEx-Ind1Ex-Ind2Ex,Tableau2), 556 update_expansion_queue_in_tableau(M,NPropEx,Ind1Ex,Ind2Ex,Tableau2,Tableau),!. 557 558 559% sub_class 560add_q(M,sc,Tableau0,[SubClassEx,SupClassEx],Tableau):- !, 561 neg_class(SupClassEx,NSupClassEx), 562 query_ind(QInd), 563 add_q(M,Tableau0,classAssertion(intersectionOf([SubClassEx,NSupClassEx]),QInd),Tableau1), 564 trillo_utility_translation:add_kb_atoms(M,class,[intersectionOf([SubClassEx,NSupClassEx])]), % This is necessary to correctly prune expansion rules 565 add_owlThing_ind(M,Tableau1,QInd,Tableau2), 566 add_clash_to_tableau(M,Tableau2,intersectionOf([SubClassEx,NSupClassEx])-QInd,Tableau3), 567 update_expansion_queue_in_tableau(M,intersectionOf([SubClassEx,NSupClassEx]),QInd,Tableau3,Tableau),!. 568 569% unsat 570add_q(M,un,Tableau0,['unsat',ClassEx],Tableau):- !, 571 query_ind(QInd), 572 add_q(M,Tableau0,classAssertion(ClassEx,QInd),Tableau1), 573 add_owlThing_ind(M,Tableau1,QInd,Tableau2), 574 add_clash_to_tableau(M,Tableau2,ClassEx-QInd,Tableau3), 575 update_expansion_queue_in_tableau(M,ClassEx,QInd,Tableau3,Tableau),!. 576 577% inconsistent_theory 578add_q(_,it,Tableau,['inconsistent','kb'],Tableau):- !. % Do nothing 579 580/* 581 Auxiliary predicates to extract the det of individuals connected to the query 582*/ 583 584% Find the individuals directly connected to the given one 585gather_connected_individuals(M,Ind,ConnectedInds):- 586 find_successors(M,Ind,SuccInds), 587 find_predecessors(M,Ind,PredInds), 588 append(SuccInds,PredInds,ConnectedInds). 589 590find_successors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,Ind,ConnectedInd)), List). 591find_predecessors(M,Ind,List) :- findall(ConnectedInd, (M:propertyAssertion(_,ConnectedInd,Ind)), List). 592 593intersect([H|_], List) :- member(H, List), !. 594intersect([_|T], List) :- intersect(T, List). 595 596% Recursively gather all the connected individuals, i.e., isolate the relevant fragment of the KB. 597%scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet). 598scan_connected_individuals(_,[],_,IndividualsSet0,IndividualsSet):-!, 599 sort(IndividualsSet0,IndividualsSet). 600 601scan_connected_individuals(M,[H|IndividualsToCheck],IndividualsChecked,IndividualsSet0,IndividualsSet):- 602 var(H),!, 603 scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet). 604 605scan_connected_individuals(M,[H|IndividualsToCheck],IndividualsChecked,IndividualsSet0,IndividualsSet):- 606 memberchk(H,IndividualsChecked),!, 607 scan_connected_individuals(M,IndividualsToCheck,IndividualsChecked,IndividualsSet0,IndividualsSet). 608 609 610scan_connected_individuals(M,[H|IndividualsToCheck0],IndividualsChecked,IndividualsSet0,IndividualsSet):- 611 gather_connected_individuals(M,H,NewIndividualsToCheck), 612 append(IndividualsSet0,NewIndividualsToCheck,IndividualsSet1), 613 append(IndividualsToCheck0,NewIndividualsToCheck,IndividualsToCheck), 614 scan_connected_individuals(M,IndividualsToCheck,[H|IndividualsChecked],[H|IndividualsSet1],IndividualsSet). 615 616 617% Builds the list of individuals conneted given the query type 618collect_individuals(M,io,[_,IndEx],IndividualsSet):-!, 619 (M:tab_util(iac,L) ; L=[]),!,retractall(M:tab_util(iac,_)), 620 scan_connected_individuals(M,[IndEx],L,[],IndividualsSet), 621 append(L,IndividualsSet,LNew), 622 assert(M:tab_util(iac,LNew)). 623 624collect_individuals(M,pv,[_,Ind1Ex,Ind2Ex],IndividualsSet):-!, 625 (M:tab_util(iac,L) ; L=[]),!,retractall(M:tab_util(iac,_)), 626 scan_connected_individuals(M,[Ind1Ex,Ind2Ex],L,[],IndividualsSet), 627 append(L,IndividualsSet,LNew), 628 assert(M:tab_util(iac,LNew)). 629 630collect_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. 631 query_ind(QInd). 632 633collect_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. 634 query_ind(QInd). 635 636collect_individuals(_,it,['inconsistent','kb'],[]):-!. 637 638/* 639 check the KB atoms to consider only the necessary expansion rules, pruning the useless ones 640*/ 641prune_tableau_rules(M):- 642 M:kb_atom(KBA), 643 Classes=KBA.class, 644 setting_trillo_default(det_rules,DetRules), 645 prune_tableau_rules(Classes,DetRules,PrunedDetRules), 646 setting_trillo_default(nondet_rules,NondetRules), 647 prune_tableau_rules(Classes,NondetRules,PrunedNondetRules), 648 set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules). 649 650add_tableau_rules_from_class(M,someValuesFrom(_,_)):- 651 M:setting_trillo(det_rules,Rules), 652 memberchk(exists_rule,Rules),!. 653 654add_tableau_rules_from_class(M,C):- 655 M:kb_atom(KBA), 656 Classes=KBA.class, 657 setting_trillo_default(det_rules,DetRules), 658 prune_tableau_rules([C|Classes],DetRules,PrunedDetRules), 659 setting_trillo_default(nondet_rules,NondetRules), 660 prune_tableau_rules([C|Classes],NondetRules,PrunedNondetRules), 661 set_tableau_expansion_rules(M:PrunedDetRules,PrunedNondetRules). 662 663% o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule,or_rule,max_rule,ch_rule 664prune_tableau_rules(_,[],[]). 665 666prune_tableau_rules(KBA,[o_rule|TR],[o_rule|PTR]):- 667 memberchk(oneOf(_),KBA),!, 668 prune_tableau_rules(KBA,TR,PTR). 669 670prune_tableau_rules(KBA,[and_rule|TR],[and_rule|PTR]):- 671 memberchk(intersectionOf(_),KBA),!, 672 prune_tableau_rules(KBA,TR,PTR). 673 674prune_tableau_rules(KBA,[unfold_rule|TR],[unfold_rule|PTR]):- 675 !, 676 prune_tableau_rules(KBA,TR,PTR). 677 678prune_tableau_rules(KBA,[add_exists_rule|TR],[add_exists_rule|PTR]):- 679 !, 680 prune_tableau_rules(KBA,TR,PTR). 681 682prune_tableau_rules(KBA,[forall_rule|TR],[forall_rule|PTR]):- 683 memberchk(allValuesFrom(_,_),KBA),!, 684 prune_tableau_rules(KBA,TR,PTR). 685 686prune_tableau_rules(KBA,[forall_plus_rule|TR],[forall_plus_rule|PTR]):- 687 memberchk(allValuesFrom(_,_),KBA),!, 688 prune_tableau_rules(KBA,TR,PTR). 689 690prune_tableau_rules(KBA,[exists_rule|TR],[exists_rule|PTR]):- 691 memberchk(someValuesFrom(_,_),KBA),!, 692 prune_tableau_rules(KBA,TR,PTR). 693 694prune_tableau_rules(KBA,[min_rule|TR],[min_rule|PTR]):- 695 (memberchk(minCardinality(_,_),KBA); memberchk(minCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!, 696 prune_tableau_rules(KBA,TR,PTR). 697 698prune_tableau_rules(KBA,[or_rule|TR],[or_rule|PTR]):- 699 memberchk(unionOf(_),KBA),!, 700 prune_tableau_rules(KBA,TR,PTR). 701 702prune_tableau_rules(KBA,[max_rule|TR],[max_rule|PTR]):- 703 (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!, 704 prune_tableau_rules(KBA,TR,PTR). 705 706 707prune_tableau_rules(KBA,[ch_rule|TR],[ch_rule|PTR]):- 708 (memberchk(maxCardinality(_,_),KBA); memberchk(maxCardinality(_,_,_),KBA);memberchk(exactCardinality(_,_),KBA);memberchk(exactCardinality(_,_,_),KBA)),!, 709 prune_tableau_rules(KBA,TR,PTR). 710 711prune_tableau_rules(KBA,[_|TR],PTR):- 712 prune_tableau_rules(KBA,TR,PTR). 713 714 715/*********** 716 Utilities for queries 717 ***********/ 718 719% findall 720find_n_explanations(M,QueryType,QueryArgs,Expls,all):- 721 !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N) 722 findall(Expl,find_single_explanation(M,QueryType,QueryArgs,Expl),Expls). 723 724% find one in backtracking 725find_n_explanations(M,QueryType,QueryArgs,Expl,bt):- 726 !, % CUT so that no other calls to find_explanation can be ran (to avoid running that with variable N) 727 find_single_explanation(M,QueryType,QueryArgs,Expl). 728 729% find_n_sol 730find_n_explanations(M,QueryType,QueryArgs,Expls,N):- 731 (number(N) -> % CUT so that no other calls to find_explanation can be ran 732 (findnsols(N,Expl,find_single_explanation(M,QueryType,QueryArgs,Expl),Expls),!) % CUT otherwise findnsols would backtracks to look for another N sols 733 ; 734 (print_message(warning,wrong_number_max_expl),!,false) 735 ). 736 737 738% to find all axplanations for probabilistic queries 739all_sub_class_int(M:ClassEx,SupClassEx,Exps):- 740 all_unsat_int(M:intersectionOf([ClassEx,complementOf(SupClassEx)]),Exps). 741 742all_instanceOf_int(M:ClassEx,IndEx,Exps):- 743 findall(Expl,instanceOf(M:ClassEx,IndEx,Expl),Exps). 744 745all_property_value_int(M:PropEx,Ind1Ex,Ind2Ex,Exps):- 746 findall(Expl,property_value(M:PropEx,Ind1Ex,Ind2Ex,Expl),Exps). 747 748all_unsat_int(M:ConceptEx,Exps):- 749 findall(Expl,unsat_internal(M:ConceptEx,Expl),Exps). 750 751 752all_inconsistent_theory_int(M:Exps):- 753 findall(Expl,inconsistent_theory(M:Expl),Exps). 754 755 756compute_prob_and_close(M,Expl,QueryOptions):- 757 M:query_option(compute_prob,expl),!, 758 get_from_query_options(QueryOptions,compute_prob,expl,Prob), 759 compute_prob_single_explanation(M,Expl,Prob),!. 760 761compute_prob_and_close(M,_,QueryOptions):- 762 M:query_option(compute_prob,query),!, 763 get_from_query_options(QueryOptions,compute_prob,query,Prob), 764 findall(Exp,M:exp_found(qp,Exp),Exps), 765 compute_prob(M,Exps,Prob),!. 766 767compute_prob_and_close(_M,_,_):-!. 768 769% checks the explanation 770check_and_close(_,Expl0,Expl):- 771 dif(Expl0,[]), 772 sort(Expl0,Expl). 773 774is_expl(M,Expl):- 775 dif(Expl,[]), 776 dif(Expl,[[]]), 777 initial_expl(M,EExpl), 778 dif(Expl,EExpl). 779 780/* 781find_expls(M,[],['inconsistent','kb'],E):-!, 782 findall(Exp,M:exp_found(['inconsistent','kb'],Exp),Expl0), 783 remove_supersets(Expl0,Expl),!, 784 member(E,Expl). 785 786find_expls(M,[],_Q,_):- 787 M:exp_found(['inconsistent','kb'],_),!, 788 print_message(warning,inconsistent),!,false. 789 790find_expls(M,[],Q,E):- 791 findall(Exp,M:exp_found(Q,Exp),Expl0), 792 remove_supersets(Expl0,Expl),!, 793 member(E,Expl). 794*/ 795% checks if an explanations was already found (instance_of version) 796find_expls(M,[Clash|_],Tab,E):- % QueryArgs 797 clash(M,Clash,Tab,EL0), 798 member(E0-CPs0,EL0), 799 sort(CPs0,CPs1), 800 dif(E0,[]), 801 sort(E0,E), 802 % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp 803 % if it is so, the explanation is labelled as inconsistent kb via Q 804 consistency_check(CPs1,[],Q), 805 %findall(Exp,M:exp_found([C,I],Exp),Expl), 806 %not_already_found(M,Expl,[C,I],E), 807 ( dif(Q,['inconsistent','kb']) -> true ; 808 ( check_open_query_monitor_status(M,it,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)) ), 809 \+ M:exp_found(Q,E), 810 assert(M:exp_found(Q,E)). % QueryArgs 811 812find_expls(M,[_Clash|Clashes],Tab,E):- 813 find_expls(M,Clashes,Tab,E). 814 815% checks if an explanations was already found 816find_expls_from_tab_list(M,[],E):- 817 %findall(Exp-CPs,M:exp_found([C,I,CPs],Exp),Expl), 818 %dif(Expl,[]), 819 findall(Ex0,find_expls_from_choice_point_list(M,Ex0),L0), 820 findall(Ex1,M:exp_found(_,Ex1),L1), 821 append(L0,L1,L), 822 remove_supersets(L,Ls), 823 member(E,Ls), 824 \+ M:exp_found(_,E), 825 assert(M:exp_found(tc,E)). 826 827find_expls_from_tab_list(M,[Tab|_T],E):- % QueryArgs 828 get_solved_clashes(Tab,Clashes), 829 member(Clash,Clashes), 830 clash(M,Clash,Tab,EL0), 831 member(E0-CPs0,EL0), 832 sort(CPs0,CPs1), 833 dif(E0,[]), 834 sort(E0,E), 835 % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp 836 % if it is so, the explanation is labelled as inconsistent kb via Q 837 consistency_check(CPs1,CPs2,_), 838 %dif(CPs2,[]), 839 get_latest_choice(CPs2,ID,Choice), 840 subtract(CPs1,[cpp(ID,Choice)],CPs), %remove cpp from CPs1 so the qp remains inside choice points list 841 update_choice_point_list(M,ID,Choice,E,CPs), 842 fail. 843 844 845find_expls_from_tab_list(M,[_Tab|T],Expl):- 846 %\+ length(T,0), 847 find_expls_from_tab_list(M,T,Expl). 848 849 850combine_expls_from_nondet_rules(M,cp(_,_,_,_,_,Expl),E):- 851 check_non_empty_choice(Expl,ExplList), 852 and_all_f(M,ExplList,ExplanationsList), 853 %check_presence_of_other_choices(ExplanationsList,Explanations,Choices), 854 member(E0-Choices0,ExplanationsList), 855 sort(E0,E), 856 sort(Choices0,Choices1), 857 % this predicate checks if there are inconsistencies in the KB, i.e., explanations without query placeholder qp 858 % if it is so, the explanation is labelled as inconsistent kb via Q 859 consistency_check(Choices1,Choices,Q), 860 ( 861 dif(Choices,[]) -> 862 ( 863 %TODO gestione altri cp 864 get_latest_choice(Choices,ID,Choice), 865 subtract(Choices0,[cpp(ID,Choice)],CPs), %remove cpp from Choices1 so the qp remains inside choice points list 866 update_choice_point_list(M,ID,Choice,E,CPs), 867 fail % to force recursion 868 ) ; 869 ( 870 ( dif(Q,['inconsistent','kb']) -> true ; 871 ( check_open_query_monitor_status(M,it,['inconsistent','kb']) -> true ; print_message(warning,inconsistent)) ), 872 \+ M:exp_found(Q,E) 873 ) 874 ). 875 876find_expls_from_choice_point_list(M,E):- 877 extract_choice_point_list(M,CP), 878 ( 879 combine_expls_from_nondet_rules(M,CP,E) ; 880 find_expls_from_choice_point_list(M,E) 881 ). 882 883 884check_non_empty_choice(Expl,ExplList):- 885 dict_pairs(Expl,_,PairsList), 886 findall(Ex,member(_-Ex,PairsList),ExplList), 887 \+ memberchk([],ExplList). 888 889 890check_presence_of_other_choices([],[],[]). 891 892check_presence_of_other_choices([E-[]|ExplanationsList],[E|Explanations],Choices):- !, 893 check_presence_of_other_choices(ExplanationsList,Explanations,Choices). 894 895check_presence_of_other_choices([E-CP|ExplanationsList],[E|Explanations],[CP|Choices]):- 896 check_presence_of_other_choices(ExplanationsList,Explanations,Choices). 897 898check_CP([],_). 899 900check_CP([cp(CP,N)|CPT],L):- 901 findall(cp,member(_-[cp(CP,N)|CPT],L),ExplPartsList), 902 length(ExplPartsList,N), 903 check_CP(CPT,L). 904 905 906not_already_found(_M,[],_Q,_E):-!. 907 908not_already_found(_M,[H|_T],_Q,E):- 909 subset(H,E),!, 910 fail. 911 912not_already_found(M,[H|_T],Q,E):- 913 subset(E,H),!, 914 retract(M:exp_found(Q,H)). 915 916not_already_found(M,[_H|T],Q,E):- 917 not_already_found(M,T,Q,E). 918 919 920get_latest_choice([],0,0). 921 922get_latest_choice(CPs,ID,Choice):- 923 get_latest_choice_point(CPs,0,ID), 924 get_latest_choice_of_cp(CPs,ID,0,Choice). 925 926get_latest_choice_point([],ID,ID). 927 928get_latest_choice_point([cpp(ID0,_)|T],ID1,ID):- 929 ID2 is max(ID1,ID0), 930 get_latest_choice_point(T,ID2,ID). 931 932 933get_latest_choice_of_cp([],_,C,C). 934 935get_latest_choice_of_cp([cpp(ID,C0)|T],ID,C1,C):- !, 936 C2 is max(C1,C0), 937 get_latest_choice_of_cp(T,ID,C2,C). 938 939get_latest_choice_of_cp([_|T],ID,C1,C):- 940 get_latest_choice_of_cp(T,ID,C1,C). 941 942 943remove_supersets([H|T],ExplanationsList):- 944 remove_supersets([H],T,ExplanationsList). 945 946remove_supersets(E,[],E). 947 948remove_supersets(E0,[H|T],ExplanationsList):- 949 remove_supersets_int(E0,H,E), 950 remove_supersets(E,T,ExplanationsList). 951 952remove_supersets_int(E0,H,E0):- 953 memberchk(H,E0),!. 954 955remove_supersets_int(E0,H,E0):- 956 member(H1,E0), 957 subset(H1,H),!. 958 959remove_supersets_int(E0,H,E):- 960 member(H1,E0), 961 subset(H,H1),!, 962 nth0(_,E0,H1,E1), 963 remove_supersets_int(E1,H,E). 964 965remove_supersets_int(E,H,[H|E]). 966 967 968% this predicate checks if there are inconsistencies in the KB, i.e., explanations with query placeholder qp 969% if it is so, the explanation is labelled as inconsistent kb 970%consistency_check(CPs,CPs,['inconsistent','kb'],['inconsistent','kb']):- !. 971 972consistency_check(CPs0,CPs,Q):- 973 (nth0(_,CPs0,qp,CPs) -> (Q=qp) ; (Q=['inconsistent','kb'],CPs=CPs0)). 974 975 976/****************************/ 977 978/*********** 979 Queries 980 - with and without explanations - 981 ***********/

1271resume_query(M:Expl):- 1272 check_open_query_monitor_status(M,_,_), 1273 M:tab_end(Tab), 1274 retract(M:tab_end(Tab)), 1275 set_up_tableau(M), 1276 check_and_set_next_from_expansion_queue(Tab,_EA,Tab1), 1277 get_explanation(M,Tab1,Expl).

1294reset_query:- 1295 get_trillo_current_module(M), 1296 set_up_reasoner(M). 1297 1298 1299 1300/*********** 1301 Utilities for queries 1302 ***********/ 1303 1304% adds the query into the ABox 1305add_q(M,Tableau0,Query,Tableau):- 1306 query_empty_expl(M,Expl), 1307 add_to_tableau(Tableau0,(Query,Expl),Tableau1), 1308 create_tabs([(Query,Expl)],Tableau1,Tableau). 1309 1310 1311% initialize an empty explanation for the query with the query placeholder 'qp' in teh choicepoint list 1312query_empty_expl(M,Expl):- 1313 empty_expl(M,EExpl), 1314 add_choice_point(M,qp,EExpl,Expl). 1315 1316remove_query_empty_expl(M,Expl0,Expl):- 1317 query_empty_expl(M,QPExpl),!, 1318 delete_qp(Expl0,QPExpl,Expl), 1319 dif(Expl,[]). 1320 1321 1322% expands query arguments using prefixes and checks their existence in the kb 1323% returns the non-present arguments 1324check_query_args(M,QT,QA,QAEx):- 1325 from_query_type_to_args_type(QT,AT), 1326 check_query_args_1(M,AT,QA,QAExT,NotEx),!, 1327 check_query_not_existent_args(QA,QAExT,NotEx,QAEx),!. 1328 1329check_query_not_existent_args(QA,QAExT,[],QAEx) :- !, 1330 ( length(QA,1) -> 1331 QAEx = ['unsat'|QAExT] 1332 ; 1333 ( length(QA,0) -> QAEx = ['inconsistent','kb'] ; QAEx = QAExT) 1334 ). 1335check_query_not_existent_args(_QA,_QAExT,NotEx,_QAEx) :- 1336 print_message(warning,iri_not_exists(NotEx)),!,fail. 1337 1338from_query_type_to_args_type(io,[class,ind]):- !. 1339from_query_type_to_args_type(pv,[prop,ind,ind]):- !. 1340from_query_type_to_args_type(sc,[class,class]):- !. 1341from_query_type_to_args_type(un,[class]):- !. 1342from_query_type_to_args_type(it,[]):- !. 1343 1344check_query_args_1(_,_,[],[],[]). 1345 1346check_query_args_1(M,[ATH|ATT],[H|T],[HEx|TEx],NotEx):- 1347 check_query_args_2(M,[ATH],[H],[HEx]),!, 1348 check_query_args_1(M,ATT,T,TEx,NotEx). 1349 1350check_query_args_1(M,[_|ATT],[H|T],TEx,[H|NotEx]):- 1351 check_query_args_1(M,ATT,T,TEx,NotEx). 1352 1353% expands query arguments using prefixes and checks their existence in the kb 1354check_query_args_2(M,AT,L,LEx) :- 1355 M:ns4query(NSList), 1356 expand_all_ns(M,L,NSList,false,LEx), %from trillo_utility_translation module 1357 check_query_args_presence(M,AT,LEx). 1358 1359check_query_args_presence(_M,_AT,[]):-!. 1360 1361check_query_args_presence(M,[class|ATT],['http://www.w3.org/2002/07/owl#Thing'|T]) :- 1362 check_query_args_presence(M,ATT,T). 1363 1364check_query_args_presence(M,[AT|ATT],[H|T]) :- 1365 nonvar(H), 1366 atomic(H),!, 1367 find_atom_in_axioms(M,AT,H),%!, 1368 check_query_args_presence(M,ATT,T). 1369 1370check_query_args_presence(M,[AT|ATT],[H|T]) :- 1371 nonvar(H), 1372 \+ atomic(H),!, 1373 H =.. [CE|L], 1374 flatten(L,L1), 1375 from_expression_to_args_type(CE,AT,L1,ATs), 1376 check_query_args_presence(M,ATs,L1), 1377 check_query_args_presence(M,ATT,T). 1378 1379/* 1380check_query_args_presence(M,[_|T]):- 1381 check_query_args_presence(M,T). 1382*/ 1383 1384% looks for presence of atoms in kb's axioms 1385find_atom_in_axioms(M,class,H):- 1386 M:kb_atom(L1), 1387 ( member(H,L1.class) ),!. 1388 1389find_atom_in_axioms(M,ind,H):- 1390 M:kb_atom(L1), 1391 ( member(H,L1.individual) ; member(H,L1.datatype) ),!. 1392 1393find_atom_in_axioms(M,prop,H):- 1394 M:kb_atom(L1), 1395 ( member(H,L1.objectProperty) ; member(H,L1.dataProperty) ; member(H,L1.annotationProperty) ),!. 1396 1397find_atom_in_axioms(_,num,H):- 1398 integer(H),!. 1399 1400from_expression_to_args_type(complementOf,class,_,[class]) :- !. 1401from_expression_to_args_type(someValuesFrom,class,_,[prop,class]) :- !. 1402from_expression_to_args_type(allValuesFrom,class,_,[prop,class]) :- !. 1403from_expression_to_args_type(hasValue,class,_,[prop,ind]) :- !. 1404from_expression_to_args_type(hasSelf,class,_,[prop]) :- !. 1405from_expression_to_args_type(minCardinality,class,[_,_,_],[num,prop,class]) :- !. 1406from_expression_to_args_type(minCardinality,class,[_,_],[num,prop]) :- !. 1407from_expression_to_args_type(maxCardinality,class,[_,_,_],[num,prop,class]) :- !. 1408from_expression_to_args_type(maxCardinality,class,[_,_],[num,prop]) :- !. 1409from_expression_to_args_type(exactCardinality,class,[_,_,_],[num,prop,class]) :- !. 1410from_expression_to_args_type(exactCardinality,class,[_,_],[num,prop]) :- !. 1411from_expression_to_args_type(inverseOf,prop,_,[prop]) :- !. 1412from_expression_to_args_type(ExprList,AT,L1,ATs):- 1413 is_expr_list(ExprList,AT,ListType),!, 1414 create_list(ListType,L1,ATs). 1415 1416 1417is_expr_list(intersectionOf,class,class). 1418is_expr_list(unionOf,class,class). 1419is_expr_list(oneOf,class,ind). 1420is_expr_list(propertyChain,prop,prop). 1421 1422create_list([],_,[]). 1423 1424create_list([_|T],AT,[AT|ATT]):- 1425 create_list(T,AT,ATT). 1426 1427 1428 1429 1430 1431 1432 1433/****************************/ 1434 1435/************** 1436 FIND FUNCTIONS 1437***************/ 1438findClassAssertion(_M,C,Ind,Expl1,ABox):- 1439 findClassAssertion(C,Ind,Expl1,ABox). 1440 1441findClassAssertion(C,Ind,Expl1,ABox):- 1442 ( 1443 is_list(Ind) -> 1444 ( 1445 find((classAssertion(C,sameIndividual(Ind)),Expl1),ABox) 1446 ) ; 1447 ( 1448 find((classAssertion(C,Ind),Expl1),ABox) 1449 ) 1450 ). 1451 1452findClassAssertion('http://www.w3.org/2002/07/owl#Thing',Ind,[],ABox):- 1453 \+ find((classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),_),ABox). 1454 1455 1456findClassAssertion(M,C,Ind,E,_ABox):- 1457 M:lpClassAssertion(C), 1458 empty_expl(M,E0), 1459 ( 1460 is_list(Ind) -> 1461 ( 1462 Ind1S=sameIndividual(Ind) 1463 ) ; 1464 ( 1465 Ind1S=Ind 1466 ) 1467 ), 1468 and_f_ax(M,lpClassAssertion(C,Ind1S),E0,E). 1469 1470findPropertyAssertion(_M,R,Ind1,Ind2,Expl1,ABox):- 1471 findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox). 1472 1473findPropertyAssertion(R,Ind1,Ind2,Expl1,ABox):- 1474 ( 1475 is_list(Ind1) -> 1476 ( 1477 Ind1S=sameIndividual(Ind1) 1478 ) ; 1479 ( 1480 Ind1S=Ind1 1481 ) 1482 ), 1483 ( 1484 is_list(Ind2) -> 1485 ( 1486 Ind2S=sameIndividual(Ind2) 1487 ) ; 1488 ( 1489 Ind2S=Ind2 1490 ) 1491 ), 1492 find((propertyAssertion(R,Ind1S,Ind2S),Expl1),ABox). 1493 1494findPropertyAssertion(M,R,Ind1,Ind2,E,_ABox):- 1495 M:lpPropertyAssertion(R), 1496 empty_expl(M,E0), 1497 ( 1498 is_list(Ind1) -> 1499 ( 1500 Ind1S=sameIndividual(Ind1) 1501 ) ; 1502 ( 1503 Ind1S=Ind1 1504 ) 1505 ), 1506 ( 1507 is_list(Ind2) -> 1508 ( 1509 Ind2S=sameIndividual(Ind2) 1510 ) ; 1511 ( 1512 Ind2S=Ind2 1513 ) 1514 ), 1515 and_f_ax(M,lpPropertyAssertion(R,Ind1S,Ind2S),E0,E). 1516 1517/**************************** 1518 TABLEAU ALGORITHM 1519****************************/ 1520 1521/* 1522find_clash(M,(ABox0,Tabs0),Expl2):- 1523 apply_rules((ABox0,Tabs0),(ABox,Tabs)), 1524 clash(M,(ABox,Tabs),Expl). 1525*/ 1526 1527%------------- 1528% clash managing 1529% previous version, manages only one clash at time 1530% need some tricks in some rules for managing the cases of more than one clash 1531% TO IMPROVE! 1532%------------ 1533:- multifile clash/4. 1534 1535clash(M,owlnothing,Tab,Expl):- 1536 get_abox(Tab,ABox), 1537 %write('clash 6'),nl, 1538 findClassAssertion4OWLNothing(M,ABox,Expl). 1539 1540clash(M,C-Ind,Tab,Expl):- 1541 get_abox(Tab,ABox), 1542 %write('clash 1'),nl, 1543 findClassAssertion(C,Ind,Expl1,ABox), 1544 neg_class(C,NegC), 1545 findClassAssertion(NegC,Ind,Expl2,ABox), 1546 and_f(M,Expl1,Expl2,Expl). 1547 1548clash(M,sameIndividual(LS),Tab,Expl):- 1549 get_abox(Tab,ABox), 1550 %write('clash 2.a'),nl, 1551 findSameIndividual(LS,(sameIndividual(LSABox),Expl1),ABox), 1552 ground(LSABox), 1553 find((differentIndividuals(LD),Expl2),ABox), 1554 member(X,LSABox), 1555 member(Y,LSABox), 1556 member(X,LD), 1557 member(Y,LD), 1558 dif(X,Y), 1559 and_f(M,Expl1,Expl2,Expl). 1560 1561clash(M,differentIndividuals(LS),Tab,Expl):- 1562 get_abox(Tab,ABox), 1563 %write('clash 2.b'),nl, 1564 findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl1),ABox), 1565 ground(LSABox), 1566 find((sameIndividual(LD),Expl2),ABox), 1567 member(X,LSABox), 1568 member(Y,LSABox), 1569 member(X,LD), 1570 member(Y,LD), 1571 dif(X,Y), 1572 and_f(M,Expl1,Expl2,Expl). 1573 1574clash(M,C-sameIndividual(L1),Tab,Expl):- 1575 get_abox(Tab,ABox), 1576 %write('clash 3'),nl, 1577 findClassAssertion(C,sameIndividual(L1),Expl1,ABox), 1578 ground(L1), 1579 neg_class(C,NegC), 1580 findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox), 1581 ground(L2), 1582 samemember(L1,L2),!, 1583 and_f(M,Expl1,Expl2,Expl). 1584 1585samemember(L1,L2):- 1586 member(X,L1), 1587 member(X,L2),!. 1588 1589clash(M,C-Ind1,Tab,Expl):- 1590 get_abox(Tab,ABox), 1591 %write('clash 4'),nl, 1592 findClassAssertion(C,Ind1,Expl1,ABox), 1593 neg_class(C,NegC), 1594 findClassAssertion(NegC,sameIndividual(L2),Expl2,ABox), 1595 ground(L2), 1596 member(Ind1,L2), 1597 and_f(M,Expl1,Expl2,Expl). 1598 1599clash(M,C-sameIndividual(L1),Tab,Expl):- 1600 get_abox(Tab,ABox), 1601 %write('clash 5'),nl, 1602 findClassAssertion(C,sameIndividual(L1),Expl1,ABox), 1603 ground(L1), 1604 neg_class(C,NegC), 1605 findClassAssertion(NegC,Ind2,Expl2,ABox), 1606 member(Ind2,L1), 1607 and_f(M,Expl1,Expl2,Expl). 1608 1609clash(M,C1-Ind,Tab,Expl):- 1610 get_abox(Tab,ABox), 1611 findClassAssertion(C1,Ind,Expl1,ABox), 1612 %write('clash 7'),nl, 1613 M:disjointClasses(L), % TODO use hierarchy 1614 member(C1,L), 1615 member(C2,L), 1616 dif(C1,C2), 1617 findClassAssertion(C2,Ind,Expl2,ABox), 1618 and_f(M,Expl1,Expl2,ExplT), 1619 and_f_ax(M,disjointClasses(L),ExplT,Expl). 1620 1621clash(M,C1-Ind,Tab,Expl):- 1622 get_abox(Tab,ABox), 1623 findClassAssertion(C1,Ind,Expl1,ABox), 1624 %write('clash 8'),nl, 1625 M:disjointUnion(Class,L), % TODO use hierarchy 1626 member(C1,L), 1627 member(C2,L), 1628 dif(C1,C2), 1629 findClassAssertion(C2,Ind,Expl2,ABox), 1630 and_f(M,Expl1,Expl2,ExplT), 1631 and_f_ax(M,disjointUnion(Class,L),ExplT,Expl). 1632 1633clash(M,P-Ind1-Ind2,Tab,Expl):- 1634 get_abox(Tab,ABox), 1635 %write('clash 11'),nl, 1636 findPropertyAssertion(P,Ind1,Ind2,Expl1,ABox), 1637 neg_class(P,NegP), % use of neg_class with a property 1638 findPropertyAssertion(NegP,Ind1,Ind2,Expl2,ABox), 1639 and_f(M,Expl1,Expl2,Expl). 1640 1641 1642/* 1643clash(M,Tab,Expl):- 1644 %write('clash 9'),nl, 1645 findClassAssertion(maxCardinality(N,S,C),Ind,Expl1,ABox), 1646 s_neighbours(M,Ind,S,Tab,SN), 1647 get_abox(Tab,ABox), 1648 individual_class_C(SN,C,ABox,SNC), 1649 length(SNC,LSS), 1650 LSS @> N, 1651 make_expl(M,Ind,S,SNC,Expl1,ABox,Expl). 1652 1653clash(M,Tab,Expl):- 1654 %write('clash 10'),nl, 1655 findClassAssertion(maxCardinality(N,S),Ind,Expl1,ABox), 1656 s_neighbours(M,Ind,S,Tab,SN), 1657 length(SN,LSS), 1658 LSS @> N, 1659 make_expl(Ind,S,SN,Expl1,ABox,Expl). 1660 1661 1662% -------------- 1663 1664make_expl(_,_,_,[],Expl,_,Expl). 1665 1666make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):- 1667 findPropertyAssertion(S,Ind,H,Expl2,ABox), 1668 and_f(M,Expl2,Expl0,Expl1), 1669 make_expl(M,Ind,S,T,Expl1,ABox,Expl). 1670*/ 1671 1672% -------------- 1673findClassAssertion4OWLNothing(M,ABox,Expl):- 1674 findClassAssertion(M,'http://www.w3.org/2002/07/owl#Nothing',_Ind,Expl,ABox). 1675 1676 1677make_expl(_,_,_,[],Expl,_,Expl). 1678 1679make_expl(M,Ind,S,[H|T],Expl0,ABox,Expl):- 1680 findPropertyAssertion(M,S,Ind,H,Expl2,ABox), 1681 and_f(M,Expl2,Expl0,Expl1), 1682 make_expl(M,Ind,S,T,Expl1,ABox,Expl). 1683% -------------- 1684 1685findSameIndividual(LS,(sameIndividual(LSABox),Expl),ABox):- 1686 find((sameIndividual(LSABox),Expl),ABox), 1687 all_members(LS,LSABox). 1688 1689findDifferentIndividuals(LS,(differentIndividuals(LSABox),Expl),ABox):- 1690 find((differentIndividuals(LSABox),Expl),ABox), 1691 all_members(LS,LSABox). 1692 1693all_members(LS,LSABox):- 1694 member(H1,LS), 1695 member(H2,LS), 1696 dif(H1,H2), 1697 member(H1,LSABox), 1698 member(H2,LSABox),!. 1699 1700 1701 1702:- multifile check_clash/3. 1703 1704check_clash(_,'http://www.w3.org/2002/07/owl#Nothing'-_,_):- 1705 %write('clash 6'),nl, 1706 !. 1707 1708check_clash(M,C-Ind,Tab):- 1709 get_abox(Tab,ABox), 1710 %write('clash 1'),nl, 1711 neg_class(C,NegC), 1712 findClassAssertion(M,NegC,Ind,_,ABox),!. 1713 1714check_clash(_,sameIndividual(LS),Tab):- 1715 get_abox(Tab,ABox), 1716 %write('clash 2.a'),nl, 1717 find((differentIndividuals(LD),_Expl2),ABox), 1718 member(X,LS), 1719 member(Y,LS), 1720 member(X,LD), 1721 member(Y,LD), 1722 dif(X,Y),!. 1723 1724check_clash(_,differentIndividuals(LS),Tab):- 1725 get_abox(Tab,ABox), 1726 %write('clash 2.b'),nl, 1727 find((sameIndividual(LD),_Expl2),ABox), 1728 member(X,LS), 1729 member(Y,LS), 1730 member(X,LD), 1731 member(Y,LD), 1732 dif(X,Y),!. 1733 1734check_clash(M,C-sameIndividual(L1),Tab):- 1735 get_abox(Tab,ABox), 1736 %write('clash 3'),nl, 1737 neg_class(C,NegC), 1738 findClassAssertion(M,NegC,sameIndividual(L2),_Expl2,ABox), 1739 member(X,L1), 1740 member(X,L2),!. 1741 1742check_clash(M,C-Ind1,Tab):- 1743 get_abox(Tab,ABox), 1744 %write('clash 4'),nl, 1745 neg_class(C,NegC), 1746 findClassAssertion(M,NegC,sameIndividual(L2),_Expl2,ABox), 1747 member(Ind1,L2),!. 1748 1749check_clash(M,C-sameIndividual(L1),Tab):- 1750 get_abox(Tab,ABox), 1751 %write('clash 5'),nl, 1752 neg_class(C,NegC), 1753 findClassAssertion(M,NegC,Ind2,_,ABox), 1754 member(Ind2,L1),!. 1755 1756check_clash(M,C1-Ind,Tab):- 1757 get_abox(Tab,ABox), 1758 %write('clash 7'),nl, 1759 M:disjointClasses(L), % TODO use hierarchy 1760 member(C1,L), 1761 member(C2,L), 1762 dif(C1,C2), 1763 findClassAssertion(M,C2,Ind,_,ABox),!. 1764 1765check_clash(M,C1-Ind,Tab):- 1766 get_abox(Tab,ABox), 1767 %write('clash 8'),nl, 1768 M:disjointUnion(_Class,L), % TODO use hierarchy 1769 member(C1,L), 1770 member(C2,L), 1771 dif(C1,C2), 1772 findClassAssertion(M,C2,Ind,_,ABox),!. 1773 1774check_clash(M,P-Ind1-Ind2,Tab):- 1775 get_abox(Tab,ABox), 1776 %write('clash 11'),nl, 1777 neg_class(P,NegP), % use of neg_class with a property 1778 findPropertyAssertion(M,NegP,Ind1,Ind2,_,ABox),!. 1779 1780% ------------- 1781% rules application 1782% ------------- 1783expand_queue(_M,Tab,Tab,Expl):- 1784 get_clashes(Tab,Clashes), 1785 dif(Clashes,[]), 1786 dif(Expl,[]). 1787 1788expand_queue(M,Tab,_,_):- 1789 test_end_expand_queue(M,Tab),!, 1790 assert(M:tab_end(Tab)), 1791 fail. 1792 1793expand_queue(M,Tab0,Tab,Expl):- 1794 extract_from_expansion_queue(Tab0,EA,Tab1),!, 1795 apply_all_rules(M,Tab1,EA,Tab2,Expl), 1796 % update_queue(M,T,NewExpQueue), 1797 expand_queue(M,Tab2,Tab,Expl). 1798 1799 1800test_end_expand_queue(M,_):- 1801 check_time_limit_monitor_status(M),!. 1802 1803test_end_expand_queue(_,Tab):- 1804 expansion_queue_is_empty(Tab). 1805 1806%expand_queue(M,ABox0,[_EA|T],ABox):- 1807% expand_queue(M,ABox0,T,ABox). 1808 1809get_explanation(M,Tab,Expl):- 1810 get_explanation_int(M,Tab,Expl). 1811 1812get_explanation(M,_,Expl):- 1813 findall(Tab,M:tab_end(Tab),L), 1814 %retractall(M:tab_end(_)), 1815 find_expls_from_tab_list(M,L,Expl). 1816 1817get_explanation_int(M,Tab,_):- 1818 test_end_expand_queue(M,Tab),!, 1819 assert(M:tab_end(Tab)), 1820 fail. 1821 1822get_explanation_int(M,Tab0,Expl):- 1823 extract_current_from_expansion_queue(Tab0,EA), 1824 apply_all_rules(M,Tab0,EA,Tab1,Expl0), 1825 ( dif(Expl0,[]) -> 1826 Expl = Expl0 1827 ; 1828 get_explanation_int(M,Tab1,Expl) 1829 ). 1830 1831apply_all_rules(_,Tab,[],Tab,[]):-!. 1832 1833apply_all_rules(M,Tab0,EA,Tab,Expl):- 1834 M:setting_trillo(det_rules,Rules), 1835 apply_det_rules(M,Rules,Tab0,EA,Tab1), 1836 get_clashes(Tab1,Clash), 1837 assert(M:tab_end(Tab1)), 1838 continue_or_return_expl(M,Rules,Tab0,Tab1,Clash,Tab,Expl). 1839 1840continue_or_return_expl(M,Rules,Tab0,Tab1,[],Tab,Expl):-!, 1841 continue(M,Rules,Tab0,Tab1,[],Tab,Expl). 1842 1843continue_or_return_expl(M,_Rules,_Tab0,Tab,Clash,Tab,Expl):- 1844 find_expls(M,Clash,Tab,Expl). 1845 1846continue_or_return_expl(M,Rules,Tab0,Tab1,Clash,Tab,Expl):-!, 1847 continue(M,Rules,Tab0,Tab1,Clash,Tab,Expl). 1848 1849continue(M,_Rules,Tab0,Tab1,_Clash,Tab,Expl):- 1850 retract(M:tab_end(Tab1)), 1851 ( test_end_apply_rule(M,Tab0,Tab1) -> 1852 ( 1853 set_next_from_expansion_queue(Tab0,_EA1,Tab), 1854 Expl=[] 1855 ) 1856 ; 1857 ( 1858 pop_clashes(Tab1,_,Tab2), 1859 set_next_from_expansion_queue(Tab2,EA1,Tab3), 1860 apply_all_rules(M,Tab3,EA1,Tab,Expl) 1861 ) 1862 ). 1863 1864 1865 1866apply_det_rules(M,_,Tab,_,Tab):- 1867 check_time_limit_monitor_status(M),!. 1868 1869apply_det_rules(M,[],Tab0,EA,Tab):- 1870 M:setting_trillo(nondet_rules,Rules), 1871 apply_nondet_rules(M,Rules,Tab0,EA,Tab). 1872 1873apply_det_rules(M,[H|T],Tab0,EA,Tab):- 1874 %C=..[H,Tab,Tab1], 1875 call(H,M,Tab0,EA,Tab1),!, 1876 apply_det_rules(M,T,Tab1,EA,Tab). 1877 1878apply_det_rules(M,[_|T],Tab0,EA,Tab):- 1879 apply_det_rules(M,T,Tab0,EA,Tab). 1880 1881apply_nondet_rules(M,_,Tab,_,Tab):- 1882 check_time_limit_monitor_status(M),!. 1883 1884apply_nondet_rules(_,[],Tab,_EA,Tab). 1885 1886apply_nondet_rules(M,[H|T],Tab0,EA,Tab):- 1887 %C=..[H,Tab,L], 1888 call(H,M,Tab0,EA,L),!, 1889 member(Tab1,L), 1890 dif(Tab0,Tab1), 1891 apply_nondet_rules(M,T,Tab1,EA,Tab). 1892 1893apply_nondet_rules(M,[_|T],Tab0,EA,Tab):- 1894 apply_nondet_rules(M,T,Tab0,EA,Tab). 1895 1896test_end_apply_rule(M,_,_):- 1897 check_time_limit_monitor_status(M),!. 1898 1899test_end_apply_rule(_,Tab0,Tab1):- 1900 same_tableau(Tab0,Tab1). 1901 1902/* 1903apply_all_rules(M,Tab0,Tab):- 1904 apply_nondet_rules([or_rule,max_rule], 1905 Tab0,Tab1), 1906 (Tab0=Tab1 -> 1907 Tab=Tab1; 1908 apply_all_rules(M,Tab1,Tab)). 1909 1910apply_det_rules([],Tab,Tab). 1911apply_det_rules([H|_],Tab0,Tab):- 1912 %C=..[H,Tab,Tab1], 1913 once(call(H,Tab0,Tab)). 1914apply_det_rules([_|T],Tab0,Tab):- 1915 apply_det_rules(T,Tab0,Tab). 1916apply_nondet_rules([],Tab0,Tab):- 1917 apply_det_rules([o_rule,and_rule,unfold_rule,add_exists_rule,forall_rule,forall_plus_rule,exists_rule,min_rule],Tab0,Tab). 1918apply_nondet_rules([H|_],Tab0,Tab):- 1919 %C=..[H,Tab,L], 1920 once(call(H,Tab0,L)), 1921 member(Tab,L), 1922 dif(Tab0,Tab). 1923apply_nondet_rules([_|T],Tab0,Tab):- 1924 apply_nondet_rules(T,Tab0,Tab). 1925*/ 1926 1927 1928/*********** 1929 rules 1930************/ 1931 1932/* 1933 add_exists_rule 1934 1935 Looks up for a role that links 2 individuals, if it find it, it searches a subclass axiom 1936 in the KB that contains 'someValuesFrom(R,C)' where R is the role which links the 2 individuals 1937 and C is a class in which the 2nd individual belongs to. 1938 1939 This rule hasn't a corresponding rule in the tableau 1940 ======================== 1941*/ 1942add_exists_rule(M,Tab0,[R,Ind1,Ind2],Tab):- 1943 get_abox(Tab0,ABox), 1944 findall(C-Expl2,(findClassAssertion(M,C,Ind2,Expl2,ABox),\+unifiable(C,someValuesFrom(_,_),_),existsInKB(M,R,C)),L), 1945 findPropertyAssertion(M,R,Ind1,Ind2,Expl1,ABox),!, 1946 scan_exists_from_class_list(M,R,Ind1,Expl1,ABox,L,Tab0,Tab),!. 1947 1948add_exists_rule(_,Tab,[someValuesFrom(_,_),_Ind2],Tab):-!. 1949 1950add_exists_rule(M,Tab0,[C,Ind2],Tab):- 1951 get_abox(Tab0,ABox), 1952 findall(R-Ind1-Expl1,(findPropertyAssertion(M,R,Ind1,Ind2,Expl1,ABox),existsInKB(M,R,C)),L), 1953 findClassAssertion(M,C,Ind2,Expl2,ABox),!, 1954 scan_exists_from_rule_list(M,C,Expl2,ABox,L,Tab0,Tab),!. 1955 1956existsInKB(M,R,C):- 1957 M:subClassOf(A,B), 1958 member(someValuesFrom(R,C),[A,B]),!. 1959 1960existsInKB(M,R,C):- 1961 M:equivalentClasses(L), 1962 member(someValuesFrom(R,C),L),!. 1963 1964scan_exists_from_class_list(M,_,_,_,_,[],Tab,Tab):-!, 1965 add_tableau_rules_from_class(M,someValuesFrom(_,_)). 1966 1967scan_exists_from_class_list(M,R,Ind1,Expl1,ABox,[C-Expl2|T],Tab0,Tab):- 1968 and_f(M,Expl1,Expl2,Expl), 1969 modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab1), 1970 scan_exists_from_class_list(M,R,Ind1,Expl1,ABox,T,Tab1,Tab). 1971 1972scan_exists_from_class_list(M,R,Ind1,Expl1,ABox,[_|T],Tab0,Tab):- 1973 scan_exists_from_class_list(M,R,Ind1,Expl1,ABox,T,Tab0,Tab). 1974 1975% ----------------- 1976 1977scan_exists_from_rule_list(M,_,_,_,[],Tab,Tab):-!, 1978 add_tableau_rules_from_class(M,someValuesFrom(_,_)). 1979 1980scan_exists_from_rule_list(M,C,Expl2,ABox,[R-Ind1-Expl1|T],Tab0,Tab):- 1981 and_f(M,Expl1,Expl2,Expl), 1982 modify_ABox(M,Tab0,someValuesFrom(R,C),Ind1,Expl,Tab1), 1983 scan_exists_from_rule_list(M,C,Expl2,ABox,T,Tab1,Tab). 1984 1985scan_exists_from_rule_list(M,C,Expl2,ABox,[_|T],Tab0,Tab):- 1986 scan_exists_from_rule_list(M,C,Expl2,ABox,T,Tab0,Tab). 1987 1988/* *************** */ 1989 1990/* 1991 and_rule 1992 ================= 1993*/ 1994and_rule(M,Tab0,[intersectionOf(LC),Ind],Tab):- 1995 get_abox(Tab0,ABox), 1996 findClassAssertion(M,intersectionOf(LC),Ind,Expl,ABox),!, 1997 \+ indirectly_blocked(M,Ind,Tab0), 1998 scan_and_list(M,LC,Ind,Expl,Tab0,Tab). 1999 2000 2001%---------------- 2002scan_and_list(_M,[],_Ind,_Expl,Tab,Tab):-!. 2003 2004scan_and_list(M,[C|T],Ind,Expl,Tab0,Tab):- 2005 modify_ABox(M,Tab0,C,Ind,Expl,Tab1),!, 2006 scan_and_list(M,T,Ind,Expl,Tab1,Tab). 2007 2008scan_and_list(M,[_C|T],Ind,Expl,Tab0,Tab):- 2009 scan_and_list(M,T,Ind,Expl,Tab0,Tab). 2010/* ************* */ 2011 2012/* 2013 or_rule 2014 =============== 2015*/ 2016or_rule(M,Tab0,[unionOf(LC),Ind],L):- 2017 get_abox(Tab0,ABox), 2018 findClassAssertion(M,unionOf(LC),Ind,Expl,ABox),!, 2019 \+ indirectly_blocked(M,Ind,Tab0), 2020 %not_ind_intersected_union(M,Ind,LC,ABox), 2021 % length(LC,NClasses), 2022 get_choice_point_id(M,ID), 2023 scan_or_list(M,LC,0,ID,Ind,Expl,Tab0,L), 2024 dif(L,[]), 2025 create_choice_point(M,Ind,or,unionOf(LC),LC,_),!. % last variable whould be equals to ID 2026 2027not_ind_intersected_union(M,Ind,LC,ABox):- 2028 \+ ind_intersected_union(M,Ind,LC,ABox). 2029 2030ind_intersected_union(M,Ind,LC,ABox) :- 2031 member(C,LC), 2032 findClassAssertion(M,C,Ind,_,ABox),!. 2033%--------------- 2034scan_or_list(_,[],_,_,_,_,_,[]):- !. 2035 2036scan_or_list(M,[C|T],N0,CP,Ind,Expl0,Tab0,[Tab|L]):- 2037 add_choice_point(M,cpp(CP,N0),Expl0,Expl), 2038 modify_ABox(M,Tab0,C,Ind,Expl,Tab), 2039 N is N0 + 1, 2040 scan_or_list(M,T,N,CP,Ind,Expl0,Tab0,L). 2041 2042/* **************** */ 2043 2044/* 2045 exists_rule 2046 ================== 2047*/ 2048exists_rule(M,Tab0,[someValuesFrom(R,C),Ind1],Tab):- 2049 get_abox(Tab0,ABox0), 2050 findClassAssertion(M,someValuesFrom(R,C),Ind1,Expl,ABox0),!, 2051 \+ blocked(M,Ind1,Tab0), 2052 \+ connected_individual(M,R,C,Ind1,ABox0), 2053 new_ind(M,Ind2), 2054 add_edge(R,Ind1,Ind2,Tab0,Tab1), 2055 retractall(M:tab_util(rc,_)), 2056 add_owlThing_ind(M,Tab1,Ind2,Tab2), 2057 modify_ABox(M,Tab2,C,Ind2,Expl,Tab3), 2058 modify_ABox(M,Tab3,R,Ind1,Ind2,Expl,Tab). 2059 2060 2061 2062%--------------- 2063connected_individual(M,R,C,Ind1,ABox):- 2064 findPropertyAssertion(R,Ind1,Ind2,_,ABox), 2065 findClassAssertion(M,C,Ind2,_,ABox). 2066 2067/* ************ */ 2068 2069/* 2070 forall_rule 2071 =================== 2072*/ 2073forall_rule(M,Tab0,[allValuesFrom(R,C),Ind1],Tab):- 2074 \+ indirectly_blocked(M,Ind1,Tab0),!, 2075 get_abox(Tab0,ABox), 2076 findall(Ind2-Expl2,findPropertyAssertion(M,R,Ind1,Ind2,Expl2,ABox),L), 2077 findClassAssertion(M,allValuesFrom(R,C),Ind1,Expl1,ABox),!, 2078 scan_forall_from_class_list(M,C,Expl1,L,Tab0,Tab). 2079 2080forall_rule(M,Tab0,[R,Ind1,Ind2],Tab):- 2081 \+ indirectly_blocked(M,Ind1,Tab0),!, 2082 get_abox(Tab0,ABox), 2083 findall(C-Expl1,findClassAssertion(M,allValuesFrom(R,C),Ind1,Expl1,ABox),L), 2084 findPropertyAssertion(M,R,Ind1,Ind2,Expl2,ABox),!, 2085 scan_forall_from_rule_list(M,Ind2,Expl2,L,Tab0,Tab). 2086 2087forall_rule(_,Tab,_,Tab):-!. 2088 2089% ------------------ 2090 2091scan_forall_from_class_list(_M,_C,_Expl1,[],Tab,Tab):-!. 2092 2093scan_forall_from_class_list(M,C,Expl1,[Ind2-Expl2|T],Tab0,Tab):- 2094 and_f(M,Expl1,Expl2,Expl), 2095 modify_ABox(M,Tab0,C,Ind2,Expl,Tab1),!, 2096 scan_forall_from_class_list(M,C,Expl1,T,Tab1,Tab). 2097 2098scan_forall_from_class_list(M,C,Expl1,[_|T],Tab0,Tab):- 2099 scan_forall_from_class_list(M,C,Expl1,T,Tab0,Tab). 2100 2101% ------------------ 2102 2103scan_forall_from_rule_list(_M,_Ind2,_Expl2,[],Tab,Tab):-!. 2104 2105scan_forall_from_rule_list(M,Ind2,Expl2,[C-Expl1|T],Tab0,Tab):- 2106 and_f(M,Expl1,Expl2,Expl), 2107 modify_ABox(M,Tab0,C,Ind2,Expl,Tab1),!, 2108 scan_forall_from_rule_list(M,Ind2,Expl2,T,Tab1,Tab). 2109 2110scan_forall_from_rule_list(M,Ind2,Expl2,[_|T],Tab0,Tab):- 2111 scan_forall_from_rule_list(M,Ind2,Expl2,T,Tab0,Tab). 2112 2113 2114/* ************** */ 2115 2116/* 2117 forall_plus_rule 2118 ================= 2119*/ 2120forall_plus_rule(M,Tab0,[allValuesFrom(S,C),Ind1],Tab):- 2121 \+ indirectly_blocked(M,Ind1,Tab0),!, 2122 get_abox(Tab0,ABox), 2123 findall(R-Ind2-Expl2,findPropertyAssertion(M,R,Ind1,Ind2,Expl2,ABox),LPropAss), 2124 findClassAssertion(M,allValuesFrom(S,C),Ind1,Expl1,ABox),!, 2125 scan_forall_plus_from_class_list(M,S,C,Expl1,LPropAss,Tab0,Tab). 2126 2127forall_plus_rule(M,Tab0,[R,Ind1,Ind2],Tab):- 2128 \+ indirectly_blocked(M,Ind1,Tab0),!, 2129 get_abox(Tab0,ABox), 2130 findall(S-C-Expl1,findClassAssertion(M,allValuesFrom(S,C),Ind1,Expl1,ABox),LClassAss), 2131 findPropertyAssertion(M,R,Ind1,Ind2,Expl2,ABox),!, 2132 scan_forall_plus_from_rule_list(M,R,Ind2,Expl2,LClassAss,Tab0,Tab). 2133 2134forall_plus_rule(_,Tab,_,Tab):-!. 2135 2136% -------------- 2137find_sub_sup_trans_role(M,R,S,Expl):- 2138 M:subPropertyOf(R,S), 2139 M:transitiveProperty(R), 2140 initial_expl(M,EExpl), 2141 and_f_ax(M,subPropertyOf(R,S),EExpl,Expl0), 2142 and_f_ax(M,transitive(R),Expl0,Expl). 2143 2144find_sub_sup_trans_role(M,R,S,Expl):- 2145 M:subPropertyOf(R,S), 2146 \+ M:transitiveProperty(R), 2147 initial_expl(M,EExpl), 2148 and_f_ax(M,subPropertyOf(R,S),EExpl,Expl). 2149 2150% ------------------ 2151 2152scan_forall_plus_from_class_list(_M,_S,_C,_Expl1,[],Tab,Tab):-!. 2153 2154scan_forall_plus_from_class_list(M,S,C,Expl1,[R-Ind2-Expl2|T],Tab0,Tab):- 2155 find_sub_sup_trans_role(M,R,S,Expl3),!, 2156 and_f(M,Expl1,Expl2,ExplT), 2157 and_f(M,ExplT,Expl3,Expl), 2158 modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab1),!, 2159 scan_forall_plus_from_class_list(M,S,C,Expl1,T,Tab1,Tab). 2160 2161scan_forall_plus_from_class_list(M,S,C,Expl1,[_|T],Tab0,Tab):- 2162 scan_forall_plus_from_class_list(M,S,C,Expl1,T,Tab0,Tab). 2163 2164% ------------------ 2165 2166scan_forall_plus_from_rule_list(_M,_R,_Ind2,_Expl2,[],_,Tab,Tab):-!. 2167 2168scan_forall_plus_from_rule_list(M,R,Ind2,Expl2,[S-C-Expl1|T],Tab0,Tab):- 2169 find_sub_sup_trans_role(M,R,S,Expl3),!, 2170 and_f(M,Expl1,Expl2,ExplT), 2171 and_f(M,ExplT,Expl3,Expl), 2172 modify_ABox(M,Tab0,allValuesFrom(R,C),Ind2,Expl,Tab1),!, 2173 scan_forall_plus_from_rule_list(M,R,Ind2,Expl2,T,Tab1,Tab). 2174 2175scan_forall_plus_from_rule_list(M,R,Ind2,Expl2,[_|T],Tab0,Tab):- 2176 scan_forall_plus_from_rule_list(M,R,Ind2,Expl2,T,Tab0,Tab). 2177 2178 2179/* ************ */ 2180 2181/* 2182 unfold_rule 2183 =========== 2184*/ 2185unfold_rule(M,Tab0,[C,Ind],Tab):- 2186 unfold_rule_c1(M,Tab0,[C,Ind],Tab1), 2187 unfold_rule_c2(M,Tab1,[C,Ind],Tab2), 2188 unfold_rule_c3(M,Tab2,[C,Ind],Tab). 2189 2190unfold_rule(M,Tab0,[P,Ind1,Ind2],Tab):- 2191 unfold_rule_p1(M,Tab0,[P,Ind1,Ind2],Tab1), 2192 unfold_rule_p2(M,Tab1,[P,Ind1,Ind2],Tab2), 2193 unfold_rule_p3(M,Tab2,[P,Ind1,Ind2],Tab3), 2194 unfold_rule_p4(M,Tab3,[P,Ind1,Ind2],Tab). 2195 2196unfold_rule_c1(M,Tab0,[C,Ind],Tab):- 2197 get_abox(Tab0,ABox), 2198 findClassAssertion(M,C,Ind,Expl,ABox),!, 2199 % usare findall(D-AX,find_sub_sup_class(M,C,D,Ax),L) e iniziare ciclo per evitare di ripetere stessi test più volte 2200 find_superclasses(M,C,L), 2201 scan_supclass_list(M,Ind,Expl,L,Tab0,Tab),!. 2202 2203/* -- unfold_rule 2204 takes a class C1 in which Ind belongs, find a not atomic class C 2205 that contains C1 (C is seen as list of classes), controls if 2206 the individual Ind belongs to all those classes, if yes it finds a class D (if exists) 2207 that is the superclass or an equivalent class of C and adds D to label of Ind 2208 - for managing tableau with more than one clash - 2209 correspond to the ce_rule 2210 -- 2211*/ 2212unfold_rule_c2(M,Tab0,[C1,Ind],Tab):- 2213 find_not_atomic_classes(M,C1,LNotAt), 2214 scan_notat_list(M,C1,Ind,LNotAt,Tab0,Tab). 2215 2216/* 2217 * -- unfold_rule 2218 * manage the negation 2219 * -- 2220 */ 2221unfold_rule_c3(M,Tab0,[complementOf(C),Ind],Tab):- 2222 get_abox(Tab0,ABox), 2223 findClassAssertion(M,complementOf(C),Ind,Expl,ABox),!, 2224 find_neg_class(C,D), 2225 and_f_ax(M,complementOf(C),Expl,AxL), 2226 (modify_ABox(M,Tab0,D,Ind,AxL,Tab1)->add_nominal(M,D,Ind,Tab1,Tab);Tab=Tab0),!. 2227 2228unfold_rule_c3(_M,Tab,_,Tab). 2229 2230% ---------------- 2231% scan_supclass_list 2232scan_supclass_list(_,_,_,[],Tab,Tab):- !. 2233 2234scan_supclass_list(M,Ind,Expl,[D-Ax|T],Tab0,Tab):- 2235 and_f_ax(M,Ax,Expl,AxL), 2236 modify_ABox(M,Tab0,D,Ind,AxL,Tab1),!, 2237 add_nominal(M,D,Ind,Tab1,Tab2),!, 2238 scan_supclass_list(M,Ind,Expl,T,Tab2,Tab). 2239 2240scan_supclass_list(M,Ind,Expl,[_|T],Tab0,Tab):- 2241 scan_supclass_list(M,Ind,Expl,T,Tab0,Tab). 2242 2243% ---------------- 2244% scan_notat_list 2245scan_notat_list(_,_C1,_Ind,[],Tab,Tab):- !. 2246 2247scan_notat_list(M,C1,Ind,[unionOf(UO)-_|T],Tab0,Tab):-!, 2248 get_abox(Tab0,ABox), 2249 findClassAssertion(M,C1,Ind,Expl,ABox), 2250 modify_ABox(M,Tab0,unionOf(UO),Ind,Expl,Tab1),!, 2251 add_nominal(M,unionOf(UO),Ind,Tab1,Tab2),!, 2252 scan_notat_list(M,C1,Ind,T,Tab2,Tab). 2253 2254scan_notat_list(M,C1,Ind,[C-L|T],Tab0,Tab):- 2255 get_abox(Tab0,ABox), 2256 find_all(M,Ind,L,ABox,Expl), 2257 modify_ABox(M,Tab0,C,Ind,Expl,Tab1),!, 2258 add_nominal(M,C,Ind,Tab1,Tab2),!, 2259 scan_notat_list(M,C1,Ind,T,Tab2,Tab). 2260 2261scan_notat_list(M,C1,Ind,[_|T],Tab0,Tab):- 2262 scan_notat_list(M,C1,Ind,T,Tab0,Tab). 2263 2264% ---------------- 2265% add_nominal 2266 2267add_nominal(M,D,Ind,Tab0,Tab):- 2268 get_abox(Tab0,ABox0), 2269 ((D = oneOf(_), 2270 \+ member(nominal(Ind),ABox0)) 2271 -> 2272 ( 2273 ABox1 = [nominal(Ind)|ABox0], 2274 (member((classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),_E),ABox1) 2275 -> 2276 set_abox(Tab0,ABox1,Tab) 2277 ; 2278 (empty_expl(M,Expl),set_abox(Tab0,[(classAssertion('http://www.w3.org/2002/07/owl#Thing',Ind),Expl)|ABox1],Tab)) 2279 ) 2280 ) 2281 ; 2282 set_abox(Tab0,ABox0,Tab) 2283 ). 2284 2285% ---------------- 2286% find_superclasses looks in the Tab if the list of superclasses has been already found. If not creates the list class-expl 2287%find_superclasses(_,Tab,C,Tab,L):- 2288% get_superclasses(Tab,C,L),!. 2289 2290%find_superclasses(M,Tab0,C,Tab1,L):- 2291% findall(D-Ax,find_sub_sup_class(M,C,D,Ax),L), 2292% set_superclasses(Tab0,C,L,Tab1). 2293 2294find_superclasses(M,C,L):- 2295 M:tab_util(sc,C-L),!. 2296 2297find_superclasses(M,C,L):- 2298 findall(D-Ax,find_sub_sup_class(M,C,D,Ax),L), 2299 assert(M:tab_util(sc,C-L)). 2300 2301find_not_atomic_classes(M,C,LNotAt):- 2302 M:tab_util(na,C-LNotAt),!. 2303 2304find_not_atomic_classes(M,C,LNotAt):- 2305 findall(D-L,find_not_atomic(M,C,D,L),LNotAt). 2306 2307 2308% ---------------- 2309% unionOf, intersectionOf, subClassOf, negation, allValuesFrom, someValuesFrom, exactCardinality(min and max), maxCardinality, minCardinality 2310:- multifile find_neg_class/2. 2311 2312find_neg_class(unionOf(L),intersectionOf(NL)):- 2313 neg_list(L,NL). 2314 2315find_neg_class(intersectionOf(L),unionOf(NL)):- 2316 neg_list(L,NL). 2317 2318find_neg_class(subClassOf(C,D),intersectionOf(C,ND)):- 2319 neg_class(D,ND). 2320 2321find_neg_class(complementOf(C),C). 2322 2323find_neg_class(allValuesFrom(R,C),someValuesFrom(R,NC)):- 2324 neg_class(C,NC). 2325 2326find_neg_class(someValuesFrom(R,C),allValuesFrom(R,NC)):- 2327 neg_class(C,NC). 2328 2329find_neg_class(exactCardinality(N,R,C),unionOf([maxCardinality(NMax,R,C),minCardinality(NMin,R,C)])):- 2330 NMax is N - 1, 2331 NMin is N + 1. 2332 2333find_neg_class(minCardinality(N,R,C),maxCardinality(NMax,R,C)):- 2334 NMax is N - 1. 2335 2336find_neg_class(maxCardinality(N,R,C),minCardinality(NMin,R,C)):- 2337 NMin is N + 1. 2338 2339% --------------- 2340 2341neg_class(complementOf(C),C):- !. 2342 2343neg_class(C,complementOf(C)):- !. 2344 2345% --------------- 2346 2347neg_list([],[]). 2348 2349neg_list([H|T],[complementOf(H)|T1]):- 2350 neg_list(T,T1). 2351 2352neg_list([complementOf(H)|T],[H|T1]):- 2353 neg_list(T,T1). 2354 2355%----------------- 2356:- multifile find_sub_sup_class/4. 2357 2358% subClassOf 2359find_sub_sup_class(M,C,D,subClassOf(C,D)):- 2360 M:subClassOf(C,D). 2361 2362%equivalentClasses 2363find_sub_sup_class(M,C,D,equivalentClasses(L)):- 2364 M:equivalentClasses(L), 2365 member(C,L), 2366 member(D,L), 2367 dif(C,D). 2368 2369%concept for concepts allValuesFrom 2370find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(R,D),Ax):- 2371 find_sub_sup_class(M,C,D,Ax), 2372 atomic(D). 2373 2374%role for concepts allValuesFrom 2375find_sub_sup_class(M,allValuesFrom(R,C),allValuesFrom(S,C),subPropertyOf(R,S)):- 2376 M:subPropertyOf(R,S). 2377 2378%concept for concepts someValuesFrom 2379find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(R,D),Ax):- 2380 find_sub_sup_class(M,C,D,Ax), 2381 atomic(D). 2382 2383%role for concepts someValuesFrom 2384find_sub_sup_class(M,someValuesFrom(R,C),someValuesFrom(S,C),subPropertyOf(R,S)):- 2385 M:subPropertyOf(R,S). 2386 2387%role for concepts exactCardinality 2388find_sub_sup_class(M,exactCardinality(N,R),exactCardinality(N,S),subPropertyOf(R,S)):- 2389 M:subPropertyOf(R,S). 2390 2391%concept for concepts exactCardinality 2392find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,R,D),Ax):- 2393 find_sub_sup_class(M,C,D,Ax), 2394 atomic(D). 2395 2396%role for concepts exactCardinality 2397find_sub_sup_class(M,exactCardinality(N,R,C),exactCardinality(N,S,C),subPropertyOf(R,S)):- 2398 M:subPropertyOf(R,S). 2399 2400%role for concepts maxCardinality 2401find_sub_sup_class(M,maxCardinality(N,R),maxCardinality(N,S),subPropertyOf(R,S)):- 2402 M:subPropertyOf(R,S). 2403 2404%concept for concepts maxCardinality 2405find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,R,D),Ax):- 2406 find_sub_sup_class(M,C,D,Ax), 2407 atomic(D). 2408 2409%role for concepts maxCardinality 2410find_sub_sup_class(M,maxCardinality(N,R,C),maxCardinality(N,S,C),subPropertyOf(R,S)):- 2411 M:subPropertyOf(R,S). 2412 2413%role for concepts minCardinality 2414find_sub_sup_class(M,minCardinality(N,R),minCardinality(N,S),subPropertyOf(R,S)):- 2415 M:subPropertyOf(R,S). 2416 2417%concept for concepts minCardinality 2418find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,R,D),Ax):- 2419 find_sub_sup_class(M,C,D,Ax), 2420 atomic(D). 2421 2422%role for concepts minCardinality 2423find_sub_sup_class(M,minCardinality(N,R,C),minCardinality(N,S,C),subPropertyOf(R,S)):- 2424 M:subPropertyOf(R,S). 2425 2426/******************* 2427 managing the concept (C subclassOf Thing) 2428 this implementation doesn't work well in a little set of cases 2429 TO IMPROVE! 2430 *******************/ 2431/* 2432find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2433 M:subClassOf(A,B), 2434 member(C,[A,B]),!. 2435 2436find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2437 M:classAssertion(C,_),!. 2438 2439find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2440 M:equivalentClasses(L), 2441 member(C,L),!. 2442 2443find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2444 M:unionOf(L), 2445 member(C,L),!. 2446 2447find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2448 M:equivalentClasses(L), 2449 member(someValuesFrom(_,C),L),!. 2450 2451find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2452 M:equivalentClasses(L), 2453 member(allValuesFrom(_,C),L),!. 2454 2455find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2456 M:equivalentClasses(L), 2457 member(minCardinality(_,_,C),L),!. 2458 2459find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2460 M:equivalentClasses(L), 2461 member(maxCardinality(_,_,C),L),!. 2462 2463find_sub_sup_class(M,C,'http://www.w3.org/2002/07/owl#Thing',subClassOf(C,'http://www.w3.org/2002/07/owl#Thing')):- 2464 M:equivalentClasses(L), 2465 member(exactCardinality(_,_,C),L),!. 2466 2467*/ 2468 2469%-------------------- 2470% looks for not atomic concepts descriptions containing class C 2471find_not_atomic(M,C,Ax,LC):- 2472 M:subClassOf(A,B), 2473 find_not_atomic_int(C,[A,B],Ax,LC). 2474 2475find_not_atomic(M,C,Ax,LC):- 2476 M:equivalentClasses(L), 2477 find_not_atomic_int(C,L,Ax,LC). 2478 2479/* 2480find_not_atomic(M,C,unionOf(L1),L1):- 2481 M:subClassOf(A,B), 2482 member(unionOf(L1),[A,B]), 2483 member(C,L1). 2484 2485find_not_atomic(M,C,unionOf(L1),L1):- 2486 M:equivalentClasses(L), 2487 member(unionOf(L1),L), 2488 member(C,L1). 2489*/ 2490 2491find_not_atomic_int(C,LC0,intersectionOf(L1),L1):- 2492 member(intersectionOf(L1),LC0), 2493 member(C,L1). 2494 2495find_not_atomic_int(C,LC0,Ax,LC):- 2496 member(intersectionOf(L1),LC0), 2497 find_not_atomic_int(C,L1,Ax,LC). 2498 2499find_not_atomic_int(C,LC0,unionOf(L1),L1):- 2500 member(unionOf(L1),LC0), 2501 member(C,L1). 2502 2503find_not_atomic_int(C,LC0,Ax,LC):- 2504 member(unionOf(L1),LC0), 2505 find_not_atomic_int(C,L1,Ax,LC). 2506 2507 2508 2509 2510% ----------------------- 2511% puts together the explanations of all the concepts found by find_not_atomic/3 2512find_all(_M,_,[],_,[]). 2513 2514find_all(M,Ind,[H|T],ABox,ExplT):- 2515 findClassAssertion(M,H,Ind,Expl1,ABox), 2516 find_all(M,Ind,T,ABox,Expl2), 2517 and_f(M,Expl1,Expl2,ExplT). 2518 2519 2520/* -- unfold_rule 2521 * control propertyRange e propertyDomain 2522 * -- 2523 */ 2524unfold_rule_p1(M,Tab0,[P,S,O],Tab):- 2525 get_abox(Tab0,ABox), 2526 findall(Ind-D-Expl,find_class_prop_range_domain(M,P,S,O,Ind,D,Expl,ABox),L), 2527 scan_rangedom_list(M,L,Tab0,Tab). 2528 2529% ---------------- 2530 2531find_class_prop_range_domain(M,P,S,O,O,D,Expl,ABox):- 2532 findPropertyAssertion(M,P,S,O,ExplPA,ABox), 2533 %ind_as_list(IndL,L), 2534 %member(Ind,L), 2535 M:propertyRange(P,D), 2536 and_f_ax(M,propertyRange(P,D),ExplPA,Expl). 2537 2538find_class_prop_range_domain(M,P,S,O,S,D,Expl,ABox):- 2539 findPropertyAssertion(M,P,S,O,ExplPA,ABox), 2540 %ind_as_list(IndL,L), 2541 %member(Ind,L), 2542 M:propertyDomain(P,D), 2543 and_f_ax(M,propertyDomain(P,D),ExplPA,Expl). 2544 2545% ---------------- 2546% scan_rangedom_list 2547scan_rangedom_list(_,[],Tab,Tab):- !. 2548 2549scan_rangedom_list(M,[Ind-D-Expl|T],Tab0,Tab):- 2550 modify_ABox(M,Tab0,D,Ind,Expl,Tab1),!, 2551 add_nominal(M,D,Ind,Tab1,Tab2),!, 2552 scan_rangedom_list(M,T,Tab2,Tab). 2553 2554scan_rangedom_list(M,[_|T],Tab0,Tab):- 2555 scan_rangedom_list(M,T,Tab0,Tab). 2556 2557% ------------------------ 2558% unfold_rule to unfold roles 2559% ------------------------ 2560% sub properties 2561unfold_rule_p2(M,Tab0,[C,Ind1,Ind2],Tab):- 2562 get_abox(Tab0,ABox), 2563 findPropertyAssertion(M,C,Ind1,Ind2,Expl,ABox),!, 2564 find_superproperties(M,C,L), 2565 scan_subinvprop_list(M,Ind1,Ind2,Expl,L,Tab0,Tab). 2566 2567%inverseProperties 2568unfold_rule_p3(M,Tab0,[C,Ind1,Ind2],Tab):- 2569 get_abox(Tab0,ABox), 2570 findPropertyAssertion(M,C,Ind1,Ind2,Expl,ABox),!, 2571 findall(D-Ax,find_inverse_property(M,C,D,Ax),L), 2572 scan_subinvprop_list(M,Ind2,Ind1,Expl,L,Tab0,Tab). 2573 2574%transitiveProperties 2575unfold_rule_p4(M,Tab0,[C,Ind1,Ind2],Tab):- 2576 get_abox(Tab0,ABox), 2577 find_transitive_property(M,C,Ax),!, 2578 findPropertyAssertion(M,C,Ind1,Ind2,Expl,ABox),!, 2579 and_f_ax(M,Ax,Expl,AxL), 2580 findall(Ind3-ExplSecond,findPropertyAssertion(M,C,Ind2,Ind3,ExplSecond,ABox),L), 2581 scan_trans_list(M,C,Ind1,AxL,L,Tab0,Tab). 2582 2583unfold_rule_p4(_,Tab,_,Tab). 2584 2585%----------------- 2586find_superproperties(M,C,L):- 2587 M:tab_util(sp,C-L),!. 2588 2589find_superproperties(M,C,L):- 2590 findall(D-Ax,find_sub_sup_property(M,C,D,Ax),L). 2591 2592 2593% subPropertyOf 2594find_sub_sup_property(M,C,D,subPropertyOf(C,D)):- 2595 M:subPropertyOf(C,D). 2596 2597%equivalentProperties 2598find_sub_sup_property(M,C,D,equivalentProperties(L)):- 2599 M:equivalentProperties(L), 2600 member(C,L), 2601 member(D,L), 2602 dif(C,D). 2603 2604%----------------- 2605%inverseProperties 2606find_inverse_property(M,C,D,inverseProperties(C,D)):- 2607 M:inverseProperties(C,D). 2608 2609find_inverse_property(M,C,D,inverseProperties(D,C)):- 2610 M:inverseProperties(D,C). 2611 2612%inverseProperties 2613find_inverse_property(M,C,C,symmetricProperty(C)):- 2614 M:symmetricProperty(C). 2615 2616%----------------- 2617%transitiveProperties 2618find_transitive_property(M,C,transitiveProperty(C)):- 2619 M:transitiveProperty(C). 2620 2621% ---------------- 2622% scan_subinvprop_list 2623scan_subinvprop_list(_,_Ind1,_Ind2,_Expl,[],Tab,Tab):- !. 2624 2625scan_subinvprop_list(M,Ind1,Ind2,Expl,[D-Ax|T],Tab0,Tab):- 2626 and_f_ax(M,Ax,Expl,AxL), 2627 modify_ABox(M,Tab0,D,Ind1,Ind2,AxL,Tab1),!, 2628 add_nominal(M,D,Ind1,Tab1,Tab2),!, 2629 add_nominal(M,D,Ind2,Tab2,Tab3),!, 2630 scan_subinvprop_list(M,Ind1,Ind2,Expl,T,Tab3,Tab). 2631 2632scan_subinvprop_list(M,Ind1,Ind2,Expl,[_|T],Tab0,Tab):- 2633 scan_subinvprop_list(M,Ind1,Ind2,Expl,T,Tab0,Tab). 2634 2635% ---------------- 2636% scan_trans_list 2637scan_trans_list(_,_,_,_,[],Tab,Tab):- !. 2638 2639scan_trans_list(M,C,Ind1,AxL,[Ind3-ExplSecond|T],Tab0,Tab):- 2640 and_f(M,AxL,ExplSecond,ExplTrans), 2641 modify_ABox(M,Tab0,C,Ind1,Ind3,ExplTrans,Tab1),!, 2642 scan_trans_list(M,C,Ind1,AxL,T,Tab1,Tab). 2643 2644scan_trans_list(M,C,Ind1,AxL,[_|T],Tab0,Tab):- 2645 scan_trans_list(M,C,Ind1,AxL,T,Tab0,Tab). 2646 2647 2648/* ************* */ 2649 2650/* 2651 ce_rule 2652 ============= 2653*/ 2654ce_rule(M,Tab0,Tab):- 2655 get_tabs(Tab0,(T,_,_)), 2656 find_not_sub_sup_class(M,Ax,UnAx), 2657 vertices(T,Inds), 2658 apply_ce_to(M,Inds,Ax,UnAx,Tab0,Tab). 2659 2660 2661% ------------------ 2662find_not_sub_sup_class(M,subClassOf(C,D),unionOf(complementOf(C),D)):- 2663 M:subClassOf(C,D), 2664 \+ atomic(C). 2665 2666 2667find_not_sub_sup_class(M,equivalentClasses(L),unionOf(L1)):- 2668 M:equivalentClasses(L), 2669 member(C,L), 2670 \+ atomic(C), 2671 copy_neg_c(C,L,L1). 2672 2673%------------------------- 2674copy_neg_c(_,[],[]). 2675 2676copy_neg_c(C,[C|T],[complementOf(C)|T1]):- 2677 !, 2678 copy_neg_c(C,T,T1). 2679 2680copy_neg_c(C,[H|T],[H|T1]):- 2681 copy_neg_c(C,T,T1). 2682 2683%--------------------- 2684apply_ce_to(_M,[],_,_,Tab,Tab). 2685 2686apply_ce_to(M,[Ind|T],Ax,UnAx,Tab0,Tab):- 2687 \+ indirectly_blocked(M,Ind,Tab), 2688 modify_ABox(M,Tab0,UnAx,Ind,[Ax],Tab1),!, 2689 apply_ce_to(M,T,Ax,UnAx,Tab1,Tab). 2690 2691apply_ce_to(M,[_Ind|T],Ax,UnAx,Tab0,Tab):- 2692 apply_ce_to(M,T,Ax,UnAx,Tab0,Tab). 2693 2694/* **************** */ 2695 2696/* 2697 min_rule 2698 ============= 2699*/ 2700min_rule(M,Tab0,[minCardinality(N,S),Ind1],Tab):- 2701 \+ blocked(M,Ind1,Tab0),!, 2702 get_abox(Tab0,ABox), 2703 findClassAssertion(M,minCardinality(N,S),Ind1,Expl,ABox),!, 2704 s_neighbours(M,Ind1,S,Tab0,SN), 2705 safe_s_neigh(M,SN,S,Tab0,SS), 2706 length(SS,LSS), 2707 LSS @< N, 2708 NoI is N-LSS, 2709 min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1), 2710 modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab). 2711 2712 2713min_rule(M,Tab0,[minCardinality(N,S,C),Ind1],Tab):- 2714 \+ blocked(M,Ind1,Tab0),!, 2715 get_abox(Tab0,ABox), 2716 findClassAssertion(M,minCardinality(N,S,C),Ind1,Expl,ABox),!, 2717 s_neighbours(M,Ind1,S,Tab0,SN), 2718 safe_s_neigh_C(M,SN,S,C,Tab0,ABox,SS), 2719 length(SS,LSS), 2720 LSS @< N, 2721 NoI is N-LSS, 2722 min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1), 2723 modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab). 2724 2725min_rule(M,Tab0,[exactCardinality(N,S),Ind1],Tab):- 2726 \+ blocked(M,Ind1,Tab0),!, 2727 get_abox(Tab0,ABox), 2728 findClassAssertion(M,exactCardinality(N,S),Ind1,Expl,ABox),!, 2729 s_neighbours(M,Ind1,S,Tab0,SN), 2730 safe_s_neigh(M,SN,S,Tab0,SS), 2731 length(SS,LSS), 2732 LSS @< N, 2733 NoI is N-LSS, 2734 min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab0,Tab1), 2735 modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab). 2736 2737 2738min_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],Tab):- 2739 \+ blocked(M,Ind1,Tab0),!, 2740 get_abox(Tab0,ABox), 2741 findClassAssertion(M,exactCardinality(N,S,C),Ind1,Expl,ABox),!, 2742 s_neighbours(M,Ind1,S,Tab0,SN), 2743 safe_s_neigh_C(M,SN,S,C,Tab0,SS), 2744 length(SS,LSS), 2745 LSS @< N, 2746 NoI is N-LSS, 2747 min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab0,Tab1), 2748 modify_ABox(M,Tab1,differentIndividuals(NI),Expl,Tab). 2749 2750min_rule(_,Tab,_,Tab):-!. 2751 2752% ---------------------- 2753min_rule_neigh(_,0,_,_,_,[],Tab,Tab). 2754 2755min_rule_neigh(M,N,S,Ind1,Expl,[Ind2|NI],Tab0,Tab):- 2756 N > 0, 2757 NoI is N-1, 2758 new_ind(M,Ind2), 2759 add_edge(S,Ind1,Ind2,Tab0,Tab1), 2760 retractall(M:tab_util(rc,_)), 2761 add_owlThing_ind(M,Tab1,Ind2,Tab2), 2762 modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3), 2763 %check_block(Ind2,Tab3), 2764 min_rule_neigh(M,NoI,S,Ind1,Expl,NI,Tab3,Tab). 2765 2766%---------------------- 2767min_rule_neigh_C(_,0,_,_,_,_,[],Tab,Tab). 2768 2769min_rule_neigh_C(M,N,S,C,Ind1,Expl,[Ind2|NI],Tab0,Tab):- 2770 N > 0, 2771 NoI is N-1, 2772 new_ind(M,Ind2), 2773 add_edge(S,Ind1,Ind2,Tab0,Tab1), 2774 retractall(M:tab_util(rc,_)), 2775 add_owlThing_ind(M,Tab1,Ind2,Tab2), 2776 modify_ABox(M,Tab2,S,Ind1,Ind2,Expl,Tab3), 2777 modify_ABox(M,Tab3,C,Ind2,[propertyAssertion(S,Ind1,Ind2)|Expl],Tab4), 2778 %check_block(Ind2,Tab4), 2779 min_rule_neigh_C(M,NoI,S,C,Ind1,Expl,NI,Tab4,Tab). 2780 2781%--------------------- 2782safe_s_neigh(_,[],_,_,[]):-!. 2783 2784safe_s_neigh(M,[H|T],S,Tab,[H|ST]):- 2785 safe(M,H,S,Tab), 2786 safe_s_neigh(M,T,S,Tab,ST). 2787 2788safe_s_neigh_C(M,L,S,C,Tab,LT):- 2789 get_abox(Tab,ABox), 2790 safe_s_neigh_C(M,L,S,C,Tab,ABox,LT). 2791 2792safe_s_neigh_C(_,[],_,_,_,_,_,[]):-!. 2793 2794safe_s_neigh_C(M,[H|T],S,C,Tab,ABox,[H|ST]):- 2795 safe(M,H,S,Tab), 2796 findClassAssertion(M,C,H,_,ABox),!, 2797 safe_s_neigh_C(M,T,S,C,Tab,ABox,ST). 2798 2799/* **************** */ 2800 2801/* 2802 max_rule 2803 ================ 2804*/ 2805max_rule(M,Tab0,[maxCardinality(N,S),Ind],L):- 2806 \+ indirectly_blocked(M,Ind,Tab0), 2807 get_abox(Tab0,ABox), 2808 findClassAssertion(M,maxCardinality(N,S),Ind,Expl0,ABox),!, 2809 s_neighbours(M,Ind,S,Tab0,SN), 2810 length(SN,LSS), 2811 LSS @> N, 2812 get_choice_point_id(M,ID), 2813 scan_max_list(M,maxCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 2814 2815max_rule(M,Tab0,[maxCardinality(N,S,C),Ind],L):- 2816 \+ indirectly_blocked(M,Ind,Tab0),!, 2817 get_abox(Tab0,ABox), 2818 findClassAssertion(M,maxCardinality(N,S,C),Ind,Expl0,ABox),!, 2819 s_neighbours(M,Ind,S,Tab0,SN), 2820 individual_class_C(M,SN,C,ABox,SNC), 2821 length(SNC,LSS), 2822 LSS @> N, 2823 get_choice_point_id(M,ID), 2824 scan_max_list(M,maxCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID 2825 2826%--------------------- 2827 2828max_rule(M,Tab0,[exactCardinality(N,S),Ind],L):- 2829 \+ indirectly_blocked(M,Ind,Tab0), 2830 get_abox(Tab0,ABox), 2831 findClassAssertion(M,exactCardinality(N,S),Ind,Expl0,ABox),!, 2832 s_neighbours(M,Ind,S,Tab0,SN), 2833 length(SN,LSS), 2834 LSS @> N, 2835 get_choice_point_id(M,ID), 2836 scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 2837 2838max_rule(M,Tab0,[exactCardinality(N,S,C),Ind],L):- 2839 \+ indirectly_blocked(M,Ind,Tab0), 2840 get_abox(Tab0,ABox), 2841 findClassAssertion(M,exactCardinality(N,S,C),Ind,Expl0,ABox),!, 2842 s_neighbours(M,Ind,S,Tab0,SN), 2843 individual_class_C(M,SN,C,ABox,SNC), 2844 length(SNC,LSS), 2845 LSS @> N, 2846 get_choice_point_id(M,ID), 2847 scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID 2848 2849max_rule(M,Tab0,[S,Ind,_],L):- 2850 \+ indirectly_blocked(M,Ind,Tab0), 2851 get_abox(Tab0,ABox), 2852 findClassAssertion(M,exactCardinality(N,S),Ind,Expl0,ABox),!, 2853 s_neighbours(M,Ind,S,Tab0,SN), 2854 length(SN,LSS), 2855 LSS @> N, 2856 get_choice_point_id(M,ID), 2857 scan_max_list(M,exactCardinality(N,S),S,'http://www.w3.org/2002/07/owl#Thing',SN,ID,Ind,Expl0,Tab0,ABox,L),!. 2858 2859max_rule(M,Tab0,[S,Ind,_],L):- 2860 \+ indirectly_blocked(M,Ind,Tab0), 2861 get_abox(Tab0,ABox), 2862 findClassAssertion(M,exactCardinality(N,S,C),Ind,Expl0,ABox),!, 2863 s_neighbours(M,Ind,S,Tab0,SN), 2864 individual_class_C(M,SN,C,ABox,SNC), 2865 length(SNC,LSS), 2866 LSS @> N, 2867 get_choice_point_id(M,ID), 2868 scan_max_list(M,exactCardinality(N,S,C),S,C,SNC,ID,Ind,Expl0,Tab0,ABox,L),!. % last variable whould be equals to ID 2869 2870%--------------------- 2871 2872scan_max_list(M,MaxCardClass,S,C,SN,CP,Ind,Expl,Tab0,ABox,Tab_list):- 2873 create_couples_for_merge(SN,[],Ind_couples), % MAYBE check_individuals_not_equal(M,YI,YJ,ABox), instead of dif 2874 length(Ind_couples,NChoices), 2875 ( 2876 NChoices @> 1 -> (FirstChoice = -1) ; (FirstChoice = 0) 2877 ), 2878 create_list_for_max_rule(M,Ind_couples,FirstChoice,CP,Ind,S,C,Expl,Tab0,ABox,Tab_list), 2879 dif(Tab_list,[]), 2880 ( dif(FirstChoice,-1) -> 2881 create_choice_point(M,Ind,mr,MaxCardClass,Ind_couples,_) 2882 ; 2883 true 2884 ). % last variable whould be equals to ID 2885 2886create_couples_for_merge([],Ind_couples,Ind_couples). 2887 2888create_couples_for_merge([H|T],Ind_couples0,Ind_couples):- 2889 create_couples_for_merge_int(H,T,Ind_couples0,Ind_couples1), 2890 create_couples_for_merge(T,Ind_couples1,Ind_couples). 2891 2892create_couples_for_merge_int(_,[],Ind_couples,Ind_couples). 2893 2894create_couples_for_merge_int(I,[H|T],Ind_couples0,Ind_couples):- 2895 create_couples_for_merge_int(I,T,[I-H|Ind_couples0],Ind_couples). 2896 2897create_list_for_max_rule(_,[],_,_,_,_,_,_,_,_,[]). 2898 2899create_list_for_max_rule(M,[YI-YJ|Ind_couples],N0,CP,Ind,S,C,Expl0,Tab0,ABox,[Tab|Tab_list]):- 2900 findPropertyAssertion(M,S,Ind,YI,ExplYI,ABox), 2901 findPropertyAssertion(M,S,Ind,YJ,ExplYJ,ABox), 2902 findClassAssertion(M,C,YI,ExplCYI,ABox), 2903 findClassAssertion(M,C,YJ,ExplCYJ,ABox), 2904 and_f(M,ExplYI,ExplYJ,ExplS0), 2905 and_f(M,ExplS0,ExplCYI,ExplS1), 2906 and_f(M,ExplS1,ExplCYJ,ExplC0), 2907 and_f(M,ExplC0,Expl0,ExplT0), 2908 ( 2909 dif(N0,-1) -> 2910 ( 2911 add_choice_point(M,cpp(CP,N0),ExplT0,ExplT), 2912 N is N0 + 1 2913 ) ; 2914 ( 2915 ExplT = ExplT0, 2916 N = N0 2917 ) 2918 ), 2919 flatten([YI,YJ],LI), 2920 merge_all_individuals(M,[(sameIndividual(LI),ExplT)],Tab0,Tab), 2921 create_list_for_max_rule(M,Ind_couples,N,CP,Ind,S,C,Expl0,Tab0,ABox,Tab_list). 2922 2923/* 2924scan_max_list(M,S,SN,CP,Ind,Expl,ABox0,Tabs0,YI-YJ,ABox,Tabs):- 2925 member(YI,SN), 2926 member(YJ,SN), 2927 % generate cp 2928 check_individuals_not_equal(M,YI,YJ,ABox0), 2929 findPropertyAssertion(M,S,Ind,YI,ExplYI,ABox0), 2930 findPropertyAssertion(M,S,Ind,YJ,ExplYJ,ABox0), 2931 and_f(M,ExplYI,ExplYJ,Expl0), 2932 and_f(M,Expl0,Expl,ExplT0), 2933 add_choice_point(M,cpp(CP,N0),ExplT0,ExplT), 2934 merge_all_individuals(M,[(sameIndividual([YI,YJ]),ExplT)],ABox0,Tabs0,ABox,Tabs). 2935*/ 2936 2937%-------------------- 2938check_individuals_not_equal(M,X,Y,ABox):- 2939 dif(X,Y), 2940 \+ same_ind(M,[X],Y,ABox). 2941%-------------------- 2942individual_class_C(_,[],_,_,[]). 2943 2944individual_class_C(M,[H|T],C,ABox,[H|T1]):- 2945 findClassAssertion(M,C,H,_,ABox),!, 2946 individual_class_C(M,T,C,ABox,T1). 2947 2948individual_class_C(M,[_H|T],C,ABox,T1):- 2949 %\+ findClassAssertion(M,C,H,_,ABox), 2950 individual_class_C(M,T,C,ABox,T1). 2951/* *************** */ 2952 2953/* 2954 ch_rule 2955 ================ 2956*/ 2957% TODO da sistemare 2958ch_rule(M,Tab0,[maxCardinality(N,S,C),Ind1],L):- 2959 \+ indirectly_blocked(M,Ind1,Tab0), 2960 get_abox(Tab0,ABox), 2961 findClassAssertion(M,maxCardinality(N,S,C),Ind1,Expl1,ABox),!, 2962 findall(Ind2-Expl2,findPropertyAssertion(M,S,Ind1,Ind2,Expl2,ABox),LPropAss), 2963 scan_ch_role_list(M,maxCardinality(N,S,C),Expl1,ABox,LPropAss,0,[Tab0],L),!. 2964 2965ch_rule(M,Tab0,[exactCardinality(N,S,C),Ind1],L):- 2966 \+ indirectly_blocked(M,Ind1,Tab0), 2967 get_abox(Tab0,ABox), 2968 findClassAssertion(M,exactCardinality(N,S,C),Ind1,Expl1,ABox),!, 2969 findall(Ind2-Expl2,findPropertyAssertion(M,S,Ind1,Ind2,Expl2,ABox),LPropAss), 2970 scan_ch_role_list(M,exactCardinality(N,S,C),Expl1,ABox,LPropAss,0,[Tab0],L),!. 2971 2972ch_rule(M,Tab0,[S,Ind1,Ind2],L):- 2973 \+ indirectly_blocked(M,Ind1,Tab0), 2974 get_abox(Tab0,ABox), 2975 findPropertyAssertion(M,S,Ind1,Ind2,Expl2,ABox),!, 2976 findall(maxCardinality(N,S,C)-Expl1,findClassAssertion(M,maxCardinality(N,S,C),Ind1,Expl1,ABox),LClassAss), 2977 scan_ch_class_list(M,Ind2,Expl2,ABox,LClassAss,0,[Tab0],L). 2978 2979ch_rule(M,Tab0,[S,Ind1,Ind2],L):- 2980 \+ indirectly_blocked(M,Ind1,Tab0), 2981 get_abox(Tab0,ABox), 2982 findPropertyAssertion(M,S,Ind1,Ind2,Expl2,ABox),!, 2983 findall(exactCardinality(N,S,C)-Expl1,findClassAssertion(M,exactCardinality(N,S,C),Ind1,Expl1,ABox),LClassAss), 2984 scan_ch_class_list(M,Ind2,Expl2,ABox,LClassAss,0,[Tab0],L). 2985 2986%--------------------- 2987 2988scan_ch_role_list(_,_,_,_,[],1,TabL,TabL):-!. 2989 2990scan_ch_role_list(M,Class,Expl1,ABox,[Ind2-Expl2|T],_,Tab0L,TabL):- 2991 Class=..[_,_N,_S,C], 2992 absent_c_not_c(M,Ind2,C,ABox),!, 2993 and_f(M,Expl1,Expl2,Expl), 2994 scan_ch_list_int(M,C,Ind2,Expl,Class,Tab0L,Tab1L),!, 2995 scan_ch_role_list(M,Class,Expl1,ABox,T,1,Tab1L,TabL). 2996 2997scan_ch_role_list(M,Class,Expl1,ABox,[_|T],Mod,Tab0L,TabL):- 2998 scan_ch_role_list(M,Class,Expl1,ABox,T,Mod,Tab0L,TabL). 2999 3000 3001scan_ch_class_list(_M,_Ind2,_,_,[],1,TabL,TabL):-!. 3002 3003scan_ch_class_list(M,Ind2,Expl2,ABox,[Class-Expl1|T],_,Tab0L,TabL):- 3004 Class=..[_,_N,_S,C], 3005 absent_c_not_c(M,Ind2,C,ABox),!, 3006 and_f(M,Expl1,Expl2,Expl), 3007 scan_ch_list_int(M,C,Ind2,Expl,Class,Tab0L,Tab1L),!, 3008 scan_ch_class_list(M,Ind2,Expl2,ABox,T,1,Tab1L,TabL). 3009 3010scan_ch_class_list(M,Ind2,Expl2,ABox,[_|T],Mod,Tab0L,TabL):- 3011 scan_ch_class_list(M,Ind2,Expl2,ABox,T,Mod,Tab0L,TabL). 3012 3013 3014scan_ch_list_int(_M,_C,_,_,_,[],[]):-!. 3015 3016scan_ch_list_int(M,C,Ind2,Expl,Class,[Tab0|TabT],L):- 3017 scan_ch_list_int(M,C,Ind2,Expl,Class,TabT,L0), 3018 get_choice_point_id(M,ID),%gtrace, 3019 neg_class(C,NC), 3020 scan_or_list(M,[C,NC],0,ID,Ind2,Expl,Tab0,L1), 3021 dif(L,[]),!, 3022 create_choice_point(M,Ind2,ch,Class,[C,NC],_),!, % last variable whould be equals to ID 3023 append(L0,L1,L),!. 3024 3025scan_ch_list_int(M,C,Ind2,Expl,Class,[_|TabT],L):- 3026 scan_ch_list_int(M,C,Ind2,Expl,Class,TabT,L). 3027 3028% --------------------- 3029 3030 3031absent_c_not_c(M,Ind,C,ABox) :- 3032 \+ is_there_c_not_c(M,Ind,C,ABox). 3033 3034is_there_c_not_c(M,Ind,C,ABox) :- 3035 findClassAssertion(M,C,Ind,_,ABox),!. 3036 3037is_there_c_not_c(M,Ind,C,ABox) :- 3038 neg_class(C,NC), 3039 findClassAssertion(M,NC,Ind,_,ABox),!. 3040 3041/* *************** */ 3042 3043/* 3044 o_rule 3045 ============ 3046*/ 3047% TODO da sistemare 3048o_rule(M,Tab0,[oneOf(C),X],Tab):- 3049 get_abox(Tab0,ABox), 3050 findClassAssertion(M,oneOf(C),X,ExplX,ABox),!, 3051 nominal(C,Tab0),!, 3052 findall(Y-ExplY, 3053 (findClassAssertion(M,oneOf(D),Y,ExplY,ABox), 3054 containsCommon(C,D),dif(X,Y), 3055 notDifferentIndividuals(M,X,Y,ABox) 3056 ),LOneOf), 3057 ind_as_list(X,LX), 3058 scan_o_list(M,X,LX,ExplX,ABox,LOneOf,Tab0,Tab). 3059 3060scan_o_list(_M,_X,_LX,_ExplX,_,[],Tab,Tab):-!. 3061 3062scan_o_list(M,X,LX,ExplX,ABox,[Y-ExplY|T],Tab0,Tab):- 3063 ind_as_list(Y,LY), 3064 and_f(M,ExplX,ExplY,ExplC), 3065 flatten([LX,LY],LI0), 3066 sort(LI0,LI), 3067 absent(sameIndividual(LI),ExplC,ABox),!, 3068 merge(M,X,Y,ExplC,Tab0,Tab1),!, 3069 scan_o_list(M,X,LX,ExplX,ABox,T,Tab1,Tab). 3070 3071scan_o_list(M,X,LX,ExplX,ABox,[_|T],Tab0,Tab):- 3072 scan_o_list(M,X,LX,ExplX,ABox,T,Tab0,Tab). 3073 3074 3075containsCommon(L1,L2):- 3076 member(X,L1), 3077 member(X,L2),!. 3078% ------------------- 3079 3080/* ************* */ 3081 3082/*********** 3083 utility for sameIndividual 3084************/ 3085 3086ind_as_list(sameIndividual(L),L):- 3087 retract_sameIndividual(L),!. 3088 3089ind_as_list(X,[X]):- 3090 atomic(X). 3091 3092list_as_sameIndividual(L0,sameIndividual(L)):- 3093 list_as_sameIndividual_int(L0,L1), 3094 sort(L1,L). 3095 3096list_as_sameIndividual_int([],[]). 3097 3098list_as_sameIndividual_int([sameIndividual(L0)|T0],L):- 3099 !, 3100 append(L0,T0,L1), 3101 list_as_sameIndividual_int(L1,L). 3102 3103list_as_sameIndividual_int([H|T0],[H|T]):- 3104 list_as_sameIndividual_int(T0,T). 3105 3106 3107find_same(H,ABox,L,Expl):- 3108 find((sameIndividual(L),Expl),ABox), 3109 member(X,L), 3110 member(X,H),!. 3111 3112find_same(_H,_ABox,[],[]). 3113 3114 3115/* 3116 retract_sameIndividual(L) 3117 ========== 3118*/ 3119retract_sameIndividual(sameIndividual(L)):- 3120 !, 3121 retract_sameIndividual(L). 3122 3123retract_sameIndividual(L):- 3124 get_trillo_current_module(N), 3125 retract(N:sameIndividual(L)). 3126 3127retract_sameIndividual(L):- 3128 get_trillo_current_module(N), 3129 \+ retract(N:sameIndividual(L)). 3130/* ****** */ 3131 3132/* 3133 * nominal/2, blockable/2, blocked/2, indirectly_blocked/2 and safe/3 3134 * 3135 */ 3136 3137nominal(Inds,Tab):- 3138 get_abox(Tab,ABox), 3139 find((nominal(Ind)),ABox), 3140 member(Ind,Inds),!. 3141 3142% ---------------- 3143 3144blockable(M,Ind,_):- 3145 M:tab_util(bkl,Ind),!. 3146 3147blockable(M,Ind,Tab):- 3148 get_abox(Tab,ABox), 3149 ( find((nominal(Ind)),ABox) 3150 -> 3151 false 3152 ; 3153 true ),!, 3154 assert(M:tab_util(bkl,Ind)). 3155 3156% --------------- 3157 3158blocked(M,Ind,_):- 3159 M:tab_util(bk,Ind),!. 3160 3161blocked(M,Ind,Tab):- 3162 check_block(M,Ind,Tab),!, 3163 assert(M:tab_util(bk,Ind)). 3164 3165/* 3166 3167 control for blocking an individual 3168 3169*/ 3170 3171check_block(M,Ind,Tab):- 3172 blockable(M,Ind,Tab), 3173 get_tabs(Tab,(T,_,_)), 3174 transpose_ugraph(T,T1), 3175 ancestor_nt(M,Ind,T1,A), 3176 neighbours(Ind,T1,N), 3177 check_block1(M,Ind,A,N,Tab),!. 3178 3179check_block(M,Ind,Tab):- 3180 blockable(M,Ind,Tab), 3181 get_tabs(Tab,(T,_,_)), 3182 transpose_ugraph(T,T1), 3183 neighbours(Ind,T1,N), 3184 check_block2(M,N,Tab),!. 3185 3186 3187check_block1(M,Indx,A,N,Tab):- 3188 member(Indx0,N), 3189 member(Indy,A), 3190 member(Indy0,A), 3191 get_tabs(Tab,(T,RBN,_)), 3192 neighbours(Indy,T,N2), 3193 member(Indy0,N2), 3194 rb_lookup((Indx0,Indx),V,RBN), 3195 rb_lookup((Indy0,Indy),V2,RBN), 3196 member(R,V), 3197 member(R,V2), 3198 get_abox(Tab,ABox), 3199 same_label(Indx,Indy0,ABox), 3200 same_label(Indx0,Indy,ABox), 3201 all_node_blockable(M,Indx0,Indy0,Tab),!. 3202 3203%check_block2([],_). 3204 3205check_block2(M,[H|Tail],Tab):- 3206 blocked(M,H,Tab), 3207 check_block2(M,Tail,Tab). 3208 3209%--------------- 3210indirectly_blocked(M,Ind,_):- 3211 M:tab_util(ib,Ind),!. 3212 3213indirectly_blocked(M,Ind,Tab):- 3214 get_tabs(Tab,(T,_RBN,_RBR)), 3215 transpose_ugraph(T,T1), 3216 neighbours(Ind,T1,N), 3217 member(A,N), 3218 blocked(M,A,Tab),!, 3219 assert(M:tab_util(ib,Ind)). 3220 3221%--------------------- 3222/* 3223 An R-neighbour y of a node x is safe if 3224 (i) x is blockable or 3225 (ii) x is a nominal node and y is not blocked. 3226*/ 3227 3228safe(M,Ind,R,_):- 3229 M:tab_util(sf,Ind-R),!. 3230 3231safe(M,Ind,R,Tab):- 3232 get_tabs(Tab,(_,_,RBR)), 3233 rb_lookup(R,V,RBR), 3234 get_parent(X,Ind,V), 3235 blockable(M,X,Tab),!, 3236 assert(M:tab_util(sf,Ind-R)). 3237 3238safe(M,Ind,R,Tab):- 3239 get_tabs(Tab,(_,_,RBR)), 3240 rb_lookup(R,V,RBR), 3241 get_parent(X,Ind,V), 3242 nominal(X,Tab),!, 3243 \+ blocked(M,Ind,Tab),!, 3244 assert(M:tab_util(sf,Ind-R)). 3245 3246get_parent(X,Ind,[(X,Ind)|_T]):-!. 3247 3248get_parent(X,Ind,[(X,LI)|_T]):- 3249 is_list(LI), 3250 member(Ind,LI),!. 3251 3252get_parent(X,Ind,[_|T]):- 3253 get_parent(X,Ind,T). 3254 3255 3256/* ***** */ 3257 3258/* 3259 writel 3260 write a list one element at each line 3261 ========== 3262*/ 3263writel([]):-!. 3264 3265writel([T|C]):- 3266 write(T),nl, 3267 writel(C). 3268 3269/* 3270 writeABox 3271 ========== 3272*/ 3273writeABox(Tab):- 3274 get_abox(Tab,ABox), 3275 writel(ABox). 3276 3277 3278/* 3279 build_abox 3280 =============== 3281*/ 3282 3283add_owlThing_ind(M,Tab0,Ind,Tab):- 3284 prepare_nom_list(M,[Ind],NomListOut), 3285 add_all_to_tableau(M,NomListOut,Tab0,Tab). 3286 3287add_owlThing_list(M,Tab0,Tab):- % TODO 3288 get_tabs(Tab0,(T,_,_)), 3289 vertices(T,NomListIn), 3290 prepare_nom_list(M,NomListIn,NomListOut), 3291 add_all_to_tableau(M,NomListOut,Tab0,Tab). 3292 3293%-------------- 3294 3295prepare_nom_list(_,[],[]):-!. 3296 3297prepare_nom_list(M,[literal(_)|T],T1):-!, 3298 prepare_nom_list(M,T,T1). 3299 3300prepare_nom_list(M,[H|T],[(classAssertion('http://www.w3.org/2002/07/owl#Thing',H),Expl)|T1]):-!, 3301 initial_expl(M,Expl), 3302 prepare_nom_list(M,T,T1). 3303%-------------- 3304 3305 3306/* merge nodes in (ABox,Tabs) */ 3307 3308merge_all_individuals(_,[],Tab,Tab):-!. 3309 3310merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):- 3311 get_abox(Tab0,ABox0), 3312 find_same(H,ABox0,L,ExplL), 3313 dif(L,[]),!, 3314 merge_all1(M,H,Expl,L,Tab0,Tab1), 3315 flatten([H,L],HL0), 3316 sort(HL0,HL), 3317 list_as_sameIndividual(HL,SI), %TODO 3318 %flatten([H,L],L0), 3319 %sort(L0,SI), 3320 and_f(M,Expl,ExplL,ExplT), 3321 add_to_tableau(Tab1,(SI,ExplT),Tab2), 3322 remove_from_tableau(Tab2,(sameIndividual(L),ExplL),Tab3), 3323 retract_sameIndividual(L), 3324 merge_all_individuals(M,T,Tab3,Tab). 3325 3326merge_all_individuals(M,[(sameIndividual(H),Expl)|T],Tab0,Tab):- 3327 %get_abox(Tab0,ABox0), 3328 %find_same(H,ABox0,L,_), 3329 %L==[],!, 3330 merge_all2(M,H,Expl,Tab0,Tab1), 3331 add_to_tableau(Tab1,(sameIndividual(H),Expl),Tab2), 3332 merge_all_individuals(M,T,Tab2,Tab). 3333 3334merge_all1(_M,[],_,_,Tab,Tab). 3335 3336merge_all1(M,[H|T],Expl,L,Tab0,Tab):- 3337 \+ member(H,L), 3338 merge(M,H,L,Expl,Tab0,Tab1), 3339 merge_all1(M,T,Expl,[H|L],Tab1,Tab). 3340 3341merge_all1(M,[H|T],Expl,L,Tab0,Tab):- 3342 member(H,L), 3343 merge_all1(M,T,Expl,L,Tab0,Tab). 3344 3345 3346 3347merge_all2(M,[X,Y|T],Expl,Tab0,Tab):- 3348 merge(M,X,Y,Expl,Tab0,Tab1), 3349 merge_all1(M,T,Expl,[X,Y],Tab1,Tab). 3350 3351 3352 3353/* 3354 creation of the query anon individual 3355 3356*/ 3357query_ind(trilloan(0)). 3358 3359/* 3360 creation of a new individual 3361 3362*/ 3363new_ind(M,trilloan(I)):- 3364 retract(M:trilloan_idx(I)), 3365 I1 is I+1, 3366 assert(M:trilloan_idx(I1)). 3367 3368/* 3369 same label for two individuals 3370 3371*/ 3372 3373same_label(X,Y,ABox):- 3374 \+ different_label(X,Y,ABox), 3375 !. 3376 3377/* 3378 different label in two individuals 3379 3380*/ 3381 3382different_label(X,Y,ABox):- 3383 findClassAssertion(C,X,_,ABox), 3384 \+ findClassAssertion(C,Y,_,ABox). 3385 3386different_label(X,Y,ABox):- 3387 findClassAssertion(C,Y,_,ABox), 3388 \+ findClassAssertion(C,X,_,ABox). 3389 3390 3391/* 3392 all nodes in path from X to Y are blockable? 3393 3394*/ 3395 3396all_node_blockable(M,X,Y,Tab):- 3397 get_tabs(Tab,(T,_,_)), 3398 graph_min_path(X,Y,T,P), 3399 all_node_blockable1(M,P,Tab). 3400 3401all_node_blockable1(_,[],_). 3402 3403all_node_blockable1(M,[H|Tail],Tab):- 3404 blockable(M,H,Tab), 3405 all_node_blockable1(M,Tail,Tab). 3406 3407/* 3408 find a path in the graph 3409 returns only one of the shortest path (if there are 2 paths that have same length, it returns only one of them) 3410*/ 3411/* 3412% It may enter in infinite loop when there is a loop in the graph 3413graph_min_path(X,Y,T,P):- 3414 findall(Path, graph_min_path1(X,Y,T,Path), Ps), 3415 min_length(Ps,P). 3416 3417graph_min_path1(X,Y,T,[X,Y]):- 3418 member(X-L,T), 3419 member(Y,L). 3420 3421graph_min_path1(X,Y,T,[X|P]):- 3422 member(X-L,T), 3423 member(Z,L), 3424 graph_min_path1(Z,Y,T,P). 3425 3426min_length([H],H). 3427 3428min_length([H|T],MP):- 3429 min_length(T,P), 3430 length(H,N), 3431 length(P,NP), 3432 (N<NP -> 3433 MP= H 3434 ; 3435 MP= P). 3436*/ 3437 3438graph_min_path(X,Y,T,P):- 3439 edges(T, Es), 3440 aggregate_all(min(Length,Path),graph_min_path1(X,Y,Es,Length,Path),min(_L,P)). 3441 3442 3443graph_min_path1(X, Y, Es, N, Path) :- 3444 graph_min_path1_int(X, Y, Es, [], Path), 3445 length(Path, N). 3446 3447graph_min_path1_int(X, Y, Es, Seen, [X]) :- 3448 \+ memberchk(X, Seen), 3449 member(X-Y, Es). 3450graph_min_path1_int(X, Z, Es, Seen, [X|T]) :- 3451 \+ memberchk(X, Seen), 3452 member(X-Y, Es), 3453 graph_min_path1_int(Y, Z, Es, [X|Seen], T), 3454 \+ memberchk(X, T). 3455 3456/* 3457 find all ancestor of a node 3458 3459*/ 3460ancestor(Ind,T,AN):- 3461 transpose_ugraph(T,T1), 3462 findall(Y,connection(Ind,T1,Y),AN). 3463 %ancestor1([Ind],T1,[],AN). 3464 3465ancestor_nt(M,Ind,TT,AN):- 3466 connection(M,Ind,TT,AN). 3467 %findall(Y,connection(Ind,TT,Y),AN). 3468 3469ancestor1([],_,A,A). 3470 3471ancestor1([Ind|Tail],T,A,AN):- 3472 neighbours(Ind,T,AT), 3473 add_all_n(AT,Tail,Tail1), 3474 add_all_n(A,AT,A1), 3475 ancestor1(Tail1,T,A1,AN). 3476 3477%:- table connection/3. 3478connection(M,X,_T,L):- 3479 M:tab_util(rc,X-L),!. 3480 3481connection(M,X,T,L):- 3482 reachable(X,T,L), 3483 assert(M:tab_util(rc,X-L)). 3484 3485 3486 3487%----------------- 3488/* 3489 3490 add_all_n(L1,L2,LO) 3491 add in L2 all item of L1 without duplicates 3492 3493*/ 3494 3495add_all_n([],A,A). 3496 3497add_all_n([H|T],A,AN):- 3498 \+ member(H,A), 3499 add_all_n(T,[H|A],AN). 3500 3501add_all_n([H|T],A,AN):- 3502 member(H,A), 3503 add_all_n(T,A,AN). 3504/* *************** */ 3505 3506 3507 3508/* 3509 find all S neighbours (S is a role) 3510*/ 3511s_neighbours(M,Ind1,S,Tab,SN):- 3512 get_tabs(Tab,(_,_,RBR)), 3513 rb_lookup(S,VN,RBR),!, 3514 s_neighbours1(Ind1,VN,SN0), 3515 flatten(SN0,SN1), 3516 get_abox(Tab,ABox), 3517 s_neighbours2(M,SN1,SN1,SN,ABox),!. 3518 3519s_neighbours(_,_Ind1,_S,_Tab,[]). % :- 3520% get_tabs(Tab,(_,_,RBR)), 3521% \+ rb_lookup(S,_VN,RBR). 3522 3523s_neighbours1(_,[],[]). 3524 3525s_neighbours1(Ind1,[(Ind1,Y)|T],[Y|T1]):- 3526 s_neighbours1(Ind1,T,T1). 3527 3528s_neighbours1(Ind1,[(X,_Y)|T],T1):- 3529 dif(X,Ind1), 3530 s_neighbours1(Ind1,T,T1). 3531 3532s_neighbours2(_,_,[],[],_). 3533 3534s_neighbours2(M,SN,[H|T],[H|T1],ABox):- 3535 s_neighbours2(M,SN,T,T1,ABox), 3536 not_same_ind(M,T1,H,ABox),!. 3537 3538s_neighbours2(M,SN,[_H|T],T1,ABox):- 3539 s_neighbours2(M,SN,T,T1,ABox). 3540 %same_ind(M,T1,H,ABox). 3541 3542 3543%----------------- 3544 3545not_same_ind(M,SN,H,_ABox):- 3546 M:differentIndividuals(SI), 3547 member(H,SI), 3548 member(H2,SI), 3549 member(H2,SN), 3550 dif(H,H2),!. 3551 3552not_same_ind(_,SN,H,ABox):- 3553 find((differentIndividuals(SI),_),ABox), 3554 member(H,SI), 3555 member(H2,SI), 3556 member(H2,SN), 3557 dif(H,H2),!. 3558 3559not_same_ind(M,SN,H,ABox):- 3560 \+ same_ind(M,SN,H,ABox),!. 3561 3562same_ind(M,SN,H,_ABox):- 3563 M:sameIndividual(SI), 3564 member(H,SI), 3565 member(H2,SI), 3566 member(H2,SN), 3567 dif(H,H2). 3568 3569same_ind(_,SN,H,ABox):- 3570 find((sameIndividual(SI),_),ABox), 3571 member(H,SI), 3572 member(H2,SI), 3573 member(H2,SN), 3574 dif(H,H2). 3575 3576/* ************* */ 3577 3578/* 3579 s_predecessors 3580 ============== 3581 find all S-predecessor of Ind 3582*/ 3583 3584s_predecessors(M,Ind1,S,Tab,SN):- 3585 get_tabs(Tab,(_,_,RBR)), 3586 rb_lookup(S,VN,RBR), 3587 s_predecessors1(Ind1,VN,SN1), 3588 get_abox(Tab,ABox), 3589 s_predecessors2(M,SN1,SN,ABox). 3590 3591s_predecessors(_M,_Ind1,S,(_ABox,(_,_,RBR)),[]):- 3592 \+ rb_lookup(S,_VN,RBR). 3593 3594s_predecessors1(_,[],[]). 3595 3596s_predecessors1(Ind1,[(Y,Ind1)|T],[Y|T1]):- 3597 s_predecessors1(Ind1,T,T1). 3598 3599s_predecessors1(Ind1,[(_X,Y)|T],T1):- 3600 dif(Y,Ind1), 3601 s_predecessors1(Ind1,T,T1). 3602 3603s_predecessors2(_M,[],[],_). 3604 3605s_predecessors2(M,[H|T],[H|T1],ABox):- 3606 s_predecessors2(M,T,T1,ABox), 3607 \+ same_ind(M,T1,H,ABox). 3608 3609s_predecessors2(M,[H|T],T1,ABox):- 3610 s_predecessors2(M,T,T1,ABox), 3611 same_ind(M,T1,H,ABox). 3612 3613/* ********** */ 3614 3615/* ************* 3616 3617Probability computation 3618 Old version 3619 3620 ************* */ 3621 3622/* 3623build_formula([],[],Var,Var). 3624 3625build_formula([D|TD],TF,VarIn,VarOut):- 3626 build_term(D,[],[],VarIn,Var1),!, 3627 build_formula(TD,TF,Var1,VarOut). 3628 3629build_formula([D|TD],[F|TF],VarIn,VarOut):- 3630 build_term(D,[],F,VarIn,Var1), 3631 build_formula(TD,TF,Var1,VarOut). 3632 3633build_term([],F,F,Var,Var). 3634 3635build_term([(Ax,S)|TC],F0,F,VarIn,VarOut):-!, 3636 (p_x(Ax,_)-> 3637 (nth0_eq(0,NVar,VarIn,(Ax,S))-> 3638 Var1=VarIn 3639 ; 3640 append(VarIn,[(Ax,S)],Var1), 3641 length(VarIn,NVar) 3642 ), 3643 build_term(TC,[[NVar,0]|F0],F,Var1,VarOut) 3644 ; 3645 (p(Ax,_)-> 3646 (nth0_eq(0,NVar,VarIn,(Ax,[]))-> 3647 Var1=VarIn 3648 ; 3649 append(VarIn,[(Ax,[])],Var1), 3650 length(VarIn,NVar) 3651 ), 3652 build_term(TC,[[NVar,0]|F0],F,Var1,VarOut) 3653 ; 3654 build_term(TC,F0,F,VarIn,VarOut) 3655 ) 3656 ). 3657 3658build_term([Ax|TC],F0,F,VarIn,VarOut):-!, 3659 (p(Ax,_)-> 3660 (nth0_eq(0,NVar,VarIn,(Ax,[]))-> 3661 Var1=VarIn 3662 ; 3663 append(VarIn,[(Ax,[])],Var1), 3664 length(VarIn,NVar) 3665 ), 3666 build_term(TC,[[NVar,0]|F0],F,Var1,VarOut) 3667 ; 3668 build_term(TC,F0,F,VarIn,VarOut) 3669 ). 3670*/ 3671 3672/* nth0_eq(PosIn,PosOut,List,El) takes as input a List, 3673an element El and an initial position PosIn and returns in PosOut 3674the position in the List that contains an element exactly equal to El 3675*/ 3676 3677/* 3678nth0_eq(N,N,[H|_T],El):- 3679 H==El,!. 3680 3681nth0_eq(NIn,NOut,[_H|T],El):- 3682 N1 is NIn+1, 3683 nth0_eq(N1,NOut,T,El). 3684 3685*/ 3686/* var2numbers converts a list of couples (Rule,Substitution) into a list 3687of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer 3688starting from 0 */ 3689/* 3690var2numbers([],_N,[]). 3691 3692var2numbers([(R,_S)|T],N,[[N,2,[Prob,Prob1,0.3,0.7]]|TNV]):- 3693 (p(R,_);p_x(R,_)), 3694 compute_prob_ax(R,Prob),!, 3695 Prob1 is 1-Prob, 3696 N1 is N+1, 3697 var2numbers(T,N1,TNV). 3698 3699 3700compute_prob_ax(R,Prob):- 3701 findall(P, p(R,P),Probs), 3702 compute_prob_ax1(Probs,Prob). 3703 3704compute_prob_ax1([Prob],Prob):-!. 3705 3706compute_prob_ax1([Prob1,Prob2],Prob):-!, 3707 Prob is Prob1+Prob2-(Prob1*Prob2). 3708 3709compute_prob_ax1([Prob1 | T],Prob):- 3710 compute_prob_ax1(T,Prob0), 3711 Prob is Prob1 + Prob0 - (Prob1*Prob0). 3712 3713*/ 3714 3715/********************** 3716 3717 Probability Computation 3718 3719***********************/ 3720/* 3721:- thread_local 3722 %get_var_n/5, 3723 rule_n/1, 3724 na/2, 3725 v/3. 3726 3727%rule_n(0). 3728 3729compute_prob(M,Explanations,Prob):- 3730 retractall(v(_,_,_)), 3731 retractall(na(_,_)), 3732 retractall(rule_n(_)), 3733 assert(rule_n(0)), 3734 %findall(1,M:annotationAssertion('http://ml.unife.it/disponte#probability',_,_),NAnnAss),length(NAnnAss,NV), 3735 get_bdd_environment(M,Env), 3736 build_bdd(M,Env,Explanations,BDD), 3737 ret_prob(Env,BDD,Prob), 3738 clean_environment(M,Env), !. 3739 3740compute_prob_single_explanation(M,Expl,Prob):- 3741 ret_prob(M,Expl,1.0,Prob). 3742 3743ret_prob(_,[],Prob,Prob):-!. 3744 3745ret_prob(M,[Ax|T],Prob0,Prob):- 3746 compute_prob_ax(M,Ax,Prob1),!, 3747 Prob2 is Prob0 * Prob1, 3748 ret_prob(M,T,Prob2,Prob). 3749 3750ret_prob(M,[_|T],Prob0,Prob):- 3751 ret_prob(M,T,Prob0,Prob). 3752 3753 3754get_var_n(Env,R,S,Probs,V):- 3755 ( 3756 v(R,S,V) -> 3757 true 3758 ; 3759 %length(Probs,L), 3760 add_var(Env,Probs,R,V), 3761 assert(v(R,S,V)) 3762 ). 3763 3764 3765get_prob_ax(M,(Ax,_Ind),N,Prob):- !, 3766 compute_prob_ax(M,Ax,Prob), 3767 ( na(Ax,N) -> 3768 true 3769 ; 3770 rule_n(N), 3771 assert(na(Ax,N)), 3772 retract(rule_n(N)), 3773 N1 is N + 1, 3774 assert(rule_n(N1)) 3775 ). 3776 3777get_prob_ax(M,Ax,N,Prob):- !, 3778 compute_prob_ax(M,Ax,Prob), 3779 ( na(Ax,N) -> 3780 true 3781 ; 3782 rule_n(N), 3783 assert(na(Ax,N)), 3784 retract(rule_n(N)), 3785 N1 is N + 1, 3786 assert(rule_n(N1)) 3787 ). 3788 3789prob_number(ProbAT,ProbA):- 3790 atom_number(ProbAT,ProbA). 3791 3792compute_prob_ax(M,Ax,Prob):- 3793 findall(ProbA,(disponte_iri(DisponteIri),M:annotationAssertion(DisponteIri,Ax,literal(ProbAT)),prob_number(ProbAT,ProbA)),Probs), 3794 compute_prob_ax1(Probs,Prob). 3795 3796compute_prob_ax1([Prob],Prob):-!. 3797 3798compute_prob_ax1([Prob1,Prob2],Prob):-!, 3799 Prob is Prob1+Prob2-(Prob1*Prob2). 3800 3801compute_prob_ax1([Prob1 | T],Prob):- 3802 compute_prob_ax1(T,Prob0), 3803 Prob is Prob1 + Prob0 - (Prob1*Prob0). 3804 3805*/ 3806 3807get_trillo_current_module(M):- 3808 trillo_utility_translation:get_module(M). 3809/**************/ 3810 3811/* 3812:- multifile sandbox:safe_primitive/1. 3813 3814sandbox:safe_primitive(trillo:get_var_n(_,_,_,_,_)). 3815*/ 3816 3817 3818 3819 3820% ========================================================================================================== 3821% TABLEAU MANAGER 3822% ========================================================================================================== 3823 3824% ====================================================================== 3825% As Dict 3826% ====================================================================== 3827 3828/* getters and setters for Tableau */ 3829 3830get_abox(Tab,ABox):- 3831 ABox = Tab.abox. 3832 3833set_abox(Tab0,ABox,Tab):- 3834 Tab = Tab0.put(abox,ABox). 3835 3836get_sameind(Tab,SameInd):- 3837 SameInd = Tab.sameind. 3838 3839get_sameind(Tab,Ind,SameInd):- 3840 SameInd = Tab.sameind.get(Ind,[]). 3841 3842set_sameind(Tab0,SameInd,Tab):- 3843 Tab = Tab0.put(sameind,SameInd). 3844 3845get_tabs(Tab,Tabs):- 3846 Tabs = Tab.tabs. 3847 3848set_tabs(Tab0,Tabs,Tab):- 3849 Tab = Tab0.put(tabs,Tabs). 3850 3851get_clashes(Tab,Clashes):- 3852 Clashes-_ = Tab.clashes. 3853 3854get_solved_clashes(Tab,SolvedClashes):- 3855 _-SolvedClashes = Tab.clashes. 3856 3857set_clashes(Tab0,Clashes,Tab):- 3858 _-SolvedClashes = Tab0.clashes, 3859 Tab = Tab0.put(clashes,Clashes-SolvedClashes). 3860 3861set_clashes(Tab0,Clashes,SolvedClashes,Tab):- 3862 Tab = Tab0.put(clashes,Clashes-SolvedClashes). 3863 3864pop_clashes(Tab0,Clashes,Tab):- 3865 Clashes-SolvedClashes0 = Tab0.clashes, 3866 empty_partial_clashes(EmptyToSolveClashes), 3867 union(Clashes,SolvedClashes0,SolvedClashes), 3868 set_clashes(Tab0, EmptyToSolveClashes, SolvedClashes,Tab). 3869 3870absence_of_clashes(Tab):- 3871 get_clashes(Tab,Clashes), 3872 Clashes=[]. 3873 3874% to_solve-solved clashes 3875empty_clashes(Clashes-SolvedClashes):- 3876 empty_partial_clashes(Clashes), 3877 empty_partial_clashes(SolvedClashes). 3878 3879empty_partial_clashes([]). 3880 3881get_expansion_queue(Tab,ExpansionQueue):- 3882 ExpansionQueue = Tab.expq. 3883 3884set_expansion_queue(Tab0,ExpansionQueue,Tab):- 3885 Tab = Tab0.put(expq,ExpansionQueue). 3886 3887extract_current_from_expansion_queue(Tab,EA):- 3888 get_expansion_queue(Tab,[[EA],_,_]),!. 3889 3890set_next_from_expansion_queue(Tab0,EA,Tab):- 3891 get_expansion_queue(Tab0,EQ0), 3892 extract_from_expansion_queue_int(EQ0,EA,EQ),!, 3893 set_expansion_queue(Tab0,EQ,Tab). 3894 3895extract_from_expansion_queue_int([_,[],[EA|T]],EA,[[EA],[],T]). 3896 3897extract_from_expansion_queue_int([_,[EA|T],NonDetQ],EA,[[EA],T,NonDetQ]). 3898 3899extract_from_expansion_queue_int([_,[],[]],[],[[],[],[]]). 3900 3901check_and_set_next_from_expansion_queue(Tab,EA,Tab):- 3902 get_expansion_queue(Tab,[[EA],_,_]),!. 3903 3904check_and_set_next_from_expansion_queue(Tab0,EA,Tab):- 3905 set_next_from_expansion_queue(Tab0,EA,Tab). 3906 3907expansion_queue_is_empty(Tab):- 3908 get_expansion_queue(Tab,EQ), 3909 empty_expansion_queue(EQ). 3910 3911empty_expansion_queue([[],[],[]]). 3912 3913same_tableau(Tab1,Tab2):- 3914 get_abox(Tab1,ABox), 3915 get_abox(Tab2,ABox), 3916 get_tabs(Tab1,Tabs), 3917 get_tabs(Tab2,Tabs). 3918 3919/* initializers */

3926new_tableau(tableau{ 3927 abox:ABox, 3928 tabs:Tabs, 3929 clashes:Clashes, 3930 expq:ExpansionQueue, 3931 sameind:sameind{} 3932 }):- 3933 new_abox(ABox), 3934 new_tabs(Tabs), 3935 empty_clashes(Clashes), 3936 empty_expansion_queue(ExpansionQueue).

3944init_tableau(ABox,Tabs,tableau{ 3945 abox:ABox, 3946 tabs:Tabs, 3947 clashes:Clashes, 3948 expq:ExpansionQueue, 3949 sameind:sameind{} 3950 }):- 3951 empty_clashes(Clashes), 3952 empty_expansion_queue(ExpansionQueue).

3959init_tableau(ABox,Tabs,ExpansionQueue,tableau{ 3960 abox:ABox, 3961 tabs:Tabs, 3962 clashes:Clashes, 3963 expq:ExpansionQueue, 3964 sameind:sameind{} 3965 }):- 3966 empty_clashes(Clashes).

3973init_tableau(ABox,tableau{abox:ABox}):-!. 3974 3975 3976% ====================================================================== 3977% As List (missing Expansion Queue!) 3978% ====================================================================== 3979/* 3980 3981get_abox([ABox,_,_],ABox). 3982 3983set_abox([_,Tabs,C],ABox,[ABox,Tabs,C]). 3984 3985get_tabs([_,Tabs,_],Tabs). 3986 3987set_tabs([ABox,_,C],Tabs,[ABox,Tabs,C]). 3988 3989get_clashes([_,_,Clashes],Clashes). 3990 3991set_clashes([ABox,Tabs,_],Clashes,[ABox,Tabs,Clashes]). 3992 3993 3994 3995new_tableau([ABox,Tabs,[]]):- 3996 new_abox(ABox), 3997 new_tabs(Tabs). 3998 3999 4000 4001init_tableau(ABox,Tabs,[ABox,Tabs,[]]). 4002 4003*/ 4004 4005 4006 4007% =================================== 4008% ABOX 4009% =================================== 4010 4011/* abox as a list */ 4012 4013new_abox([]). 4014 4015 4016/* add El to ABox */ 4017add_to_tableau(Tableau0,El,Tableau):- 4018 get_abox(Tableau0,ABox0), 4019 add_to_abox(ABox0,El,ABox), 4020 set_abox(Tableau0,ABox,Tableau). 4021 4022remove_from_tableau(Tableau0,El,Tableau):- 4023 get_abox(Tableau0,ABox0), 4024 remove_from_abox(ABox0,El,ABox), 4025 set_abox(Tableau0,ABox,Tableau). 4026 4027add_clash_to_tableau(M,Tableau0,ToCheck,Tableau):- 4028 check_clash(M,ToCheck,Tableau0),!, 4029 get_clashes(Tableau0,Clashes0), 4030 add_to_clashes(Clashes0,ToCheck,Clashes), 4031 set_clashes(Tableau0,Clashes,Tableau). 4032 4033add_clash_to_tableau(_,Tableau,_,Tableau). 4034 4035assign(L,L). 4036/* 4037 find & control (not find) 4038*/ 4039find(El,ABox):- 4040 member(El,ABox). 4041 4042control(El,ABox):- 4043 \+ find(El,ABox). 4044 4045/* end of abox a s list */ 4046 4047/* abox as a red-black tree */ 4048/*new_abox(T):- 4049 rb_new(T). 4050 4051add(A,(Ass,Ex),A1):- 4052 rb_insert(A,(Ass,Ex),[],A1). 4053 4054find((Ass,Ex),A):- 4055 rb_lookup((Ass,Ex),_,A). 4056*/ 4057/* end of abox as a rb tree */ 4058 4059 4060add_to_abox(ABox,El,[El|ABox]). 4061 4062remove_from_abox(ABox0,El,ABox):- 4063 delete(ABox0,El,ABox). 4064 4065add_to_sameind(SameInd0,LI,SameInd):- 4066 findall(I1-I2,(member(I1,LI),member(I2,LI),dif(I1,I2)),ToAdd), 4067 add_to_sameind_int(SameInd0,ToAdd,SameInd). 4068 4069add_to_sameind_int(SameInd0,[],SameInd0):-!. 4070 4071add_to_sameind_int(SameInd0,[H|TToAdd],SameInd):- 4072 member(H,SameInd0),!, 4073 add_to_sameind_int(SameInd0,TToAdd,SameInd). 4074 4075add_to_sameind_int(SameInd0,[H|TToAdd],[H|SameInd]):-!, 4076 add_to_sameind_int(SameInd0,TToAdd,SameInd). 4077 4078 4079check_clash_and_add_to_clashes(M,El,Tableau0,C0,C1):- 4080 check_clash(M,El,Tableau0),!, 4081 add_to_clashes(C0,El,C1). 4082 4083check_clash_and_add_to_clashes(_M,_El,_Tableau,C,C):- !. 4084 4085add_to_clashes(Clashes,'http://www.w3.org/2002/07/owl#Nothing'-_,[owlnothing|Clashes]):-!. 4086 4087add_to_clashes(Clashes,El,[El|Clashes]). 4088 4089remove_from_abox(Clashes0,El,Clashes):- 4090 delete(Clashes0,El,Clashes). 4091 4092/* 4093 add_all_to_tableau(M,L1,L2,LO). 4094 add in L2 all item of L1 4095*/ 4096add_all_to_tableau(M,L,Tableau0,Tableau):- 4097 get_abox(Tableau0,ABox0), 4098 get_clashes(Tableau0,Clashes0), 4099 get_tabs(Tableau0,Tabs0), 4100 get_sameind(Tableau0,SameInd0), 4101 add_all_to_abox_and_clashes(M,L,Tableau0,ABox0,ABox,Clashes0,Clashes,Tabs0,Tabs,SameInd0,SameInd), 4102 set_abox(Tableau0,ABox,Tableau1), 4103 set_clashes(Tableau1,Clashes,Tableau2), 4104 set_tabs(Tableau2,Tabs,Tableau3), 4105 set_sameind(Tableau3,SameInd,Tableau). 4106 4107add_all_to_abox_and_clashes(_,[],_,A,A,C,C,T,T,S,S):-!. 4108 4109add_all_to_abox_and_clashes(M,[(classAssertion(Class,I),Expl)|Tail],Tableau,A0,A,C0,C,(T0,RBN,RBR),T,SameInd0,SameInd):- 4110 add_to_abox(A0,(classAssertion(Class,I),Expl),A1), 4111 init_tableau(A1,TabOnlyABox), 4112 check_clash_and_add_to_clashes(M,Class-I,TabOnlyABox,C0,C1),!, 4113 add_vertices(T0,[I],T1), 4114 add_all_to_abox_and_clashes(M,Tail,Tableau,A1,A,C1,C,(T1,RBN,RBR),T,SameInd0,SameInd). 4115 4116add_all_to_abox_and_clashes(M,[(sameIndividual(LI),Expl)|Tail],Tableau,A0,A,C0,C,(T0,RBN,RBR),T,SameInd0,SameInd):- 4117 add_to_abox(A0,(sameIndividual(LI),Expl),A1), 4118 init_tableau(A1,TabOnlyABox), 4119 check_clash_and_add_to_clashes(M,sameIndividual(LI),TabOnlyABox,C0,C1),!, 4120 add_vertices(T0,LI,T1), 4121 add_to_sameind(SameInd0,LI,SameInd1), 4122 add_all_to_abox_and_clashes(M,Tail,Tableau,A1,A,C1,C,(T1,RBN,RBR),T,SameInd1,SameInd). 4123 4124add_all_to_abox_and_clashes(M,[(differentIndividuals(LI),Expl)|Tail],Tableau,A0,A,C0,C,(T0,RBN,RBR),T,SameInd0,SameInd):- 4125 add_to_abox(A0,(differentIndividuals(LI),Expl),A1), 4126 init_tableau(A1,TabOnlyABox), 4127 check_clash_and_add_to_clashes(M,differentIndividuals(LI),TabOnlyABox,C0,C1),!, 4128 add_vertices(T0,LI,T1), 4129 add_all_to_abox_and_clashes(M,Tail,Tableau,A1,A,C1,C,(T1,RBN,RBR),T,SameInd0,SameInd). 4130 4131add_all_to_abox_and_clashes(M,[(propertyAssertion(P,S,O),Expl)|Tail],Tableau,A0,A,C0,C,T0,T,SameInd0,SameInd):-!, 4132 add_to_abox(A0,(propertyAssertion(P,S,O),Expl),A1), 4133 add_edge_int(P,S,O,T0,T1), 4134 add_all_to_abox_and_clashes(M,Tail,Tableau,A1,A,C0,C,T1,T,SameInd0,SameInd). 4135 4136add_all_to_abox_and_clashes(M,[H|Tail],Tableau,A0,A,C0,C,T0,T,SameInd0,SameInd):-!, 4137 add_to_abox(A0,H,A1), 4138 add_all_to_abox_and_clashes(M,Tail,Tableau,A1,A,C0,C,T0,T,SameInd0,SameInd). 4139 4140add_all_to_abox([],A,A). 4141 4142add_all_to_abox([H|T],A0,A):- 4143 add_to_abox(A0,H,A1), 4144 add_all_to_abox(T,A1,A). 4145 4146/* ************** */ 4147 4148 4149 4150% =================================== 4151% EXPANSION QUEUE 4152% =================================== 4153 4154 4155 4156% ------------ 4157% Utility for rule application 4158% ------------ 4159update_expansion_queue_in_tableau(M,C,Ind,Tab0,Tab):- 4160 get_expansion_queue(Tab0,ExpansionQueue0), 4161 update_expansion_queue(M,C,Ind,ExpansionQueue0,ExpansionQueue), 4162 set_expansion_queue(Tab0,ExpansionQueue,Tab). 4163 4164update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab0,Tab):- 4165 get_expansion_queue(Tab0,ExpansionQueue0), 4166 update_expansion_queue(M,P,Ind1,Ind2,ExpansionQueue0,ExpansionQueue), 4167 set_expansion_queue(Tab0,ExpansionQueue,Tab). 4168 4169 4170update_expansion_queue(_,Class,Ind,[[[Class,Ind]],DQ,NDQ0],[[[Class,Ind]],DQ,NDQ0]):-!. 4171 4172update_expansion_queue(_,P,Ind1,Ind2,[[[P,Ind1,Ind2]],DQ0,NDQ],[[[P,Ind1,Ind2]],DQ0,NDQ]):-!. 4173 4174update_expansion_queue(_,unionOf(L),Ind,[Curr,DQ,NDQ0],[Curr,DQ,NDQ]):-!, 4175 delete(NDQ0,[unionOf(L),Ind],NDQ1), 4176 append(NDQ1,[[unionOf(L),Ind]],NDQ). 4177 4178update_expansion_queue(_,maxCardinality(N,S,C),Ind,[Curr,DQ,NDQ0],[Curr,DQ,NDQ]):-!, 4179 delete(NDQ0,[maxCardinality(N,S,C),Ind],NDQ1), 4180 append(NDQ1,[[maxCardinality(N,S,C),Ind]],NDQ). 4181 4182update_expansion_queue(_,maxCardinality(N,S),Ind,[Curr,DQ,NDQ0],[Curr,DQ,NDQ]):-!, 4183 delete(NDQ0,[maxCardinality(N,S),Ind],NDQ1), 4184 append(NDQ1,[[maxCardinality(N,S),Ind]],NDQ). 4185 4186update_expansion_queue(_,exactCardinality(N,S,C),Ind,[Curr,DQ,NDQ0],[Curr,DQ,NDQ]):-!, 4187 delete(NDQ0,[exactCardinality(N,S,C),Ind],NDQ1), 4188 append(NDQ1,[[exactCardinality(N,S,C),Ind]],NDQ). 4189 4190update_expansion_queue(_,exactCardinality(N,S),Ind,[Curr,DQ,NDQ0],[Curr,DQ,NDQ]):-!, 4191 delete(NDQ0,[exactCardinality(N,S),Ind],NDQ1), 4192 append(NDQ1,[[exactCardinality(N,S),Ind]],NDQ). 4193 4194update_expansion_queue(_,C,Ind,[Curr,DQ0,NDQ],[Curr,DQ,NDQ]):-!, 4195 delete(DQ0,[C,Ind],DQ1), 4196 append(DQ1,[[C,Ind]],DQ). 4197 4198update_expansion_queue(_,P,Ind1,Ind2,[Curr,DQ0,NDQ],[Curr,DQ,NDQ]):-!, 4199 delete(DQ0,[P,Ind1,Ind2],DQ1), 4200 append(DQ1,[[P,Ind1,Ind2]],DQ). 4201 4202 4203init_expansion_queue(LCA,LPA,EQ):- 4204 empty_expansion_queue(EmptyEQ), 4205 add_classes_expqueue(LCA,EmptyEQ,EQ0), 4206 add_prop_expqueue(LPA,EQ0,EQ). 4207 4208init_expansion_queue(LCA,LCA1,LPA,LPA1,EQ):- 4209 empty_expansion_queue(EmptyEQ), 4210 add_classes_expqueue(LCA,EmptyEQ,EQ0), 4211 add_lpclasses_expqueue(LCA1,EQ0,EQ1), 4212 add_prop_expqueue(LPA,EQ1,EQ2), 4213 add_lpprop_expqueue(LPA1,EQ2,EQ). 4214 4215expand_expansion_queue(LCA,LCA1,LPA,LPA1,InitEQ,EQ):- 4216 add_classes_expqueue(LCA,InitEQ,EQ0), 4217 add_lpclasses_expqueue(LCA1,EQ0,EQ1), 4218 add_prop_expqueue(LPA,EQ1,EQ2), 4219 add_lpprop_expqueue(LPA1,EQ2,EQ). 4220 4221 4222add_classes_expqueue([],EQ,EQ). 4223 4224add_classes_expqueue([(classAssertion(C,I),_)|T],EQ0,EQ):- 4225 update_expansion_queue(_,C,I,EQ0,EQ1), 4226 add_classes_expqueue(T,EQ1,EQ). 4227 4228add_lpclasses_expqueue([],EQ,EQ). 4229 4230add_lpclasses_expqueue([C|T],EQ0,EQ):- 4231 update_expansion_queue(_,C,_,EQ0,EQ1), 4232 add_lpclasses_expqueue(T,EQ1,EQ). 4233 4234add_prop_expqueue([],EQ,EQ). 4235 4236add_prop_expqueue([(propertyAssertion(P,S,O),_)|T],EQ0,EQ):- 4237 update_expansion_queue(_,P,S,O,EQ0,EQ1), 4238 add_prop_expqueue(T,EQ1,EQ). 4239 4240add_lpprop_expqueue([],EQ,EQ). 4241 4242add_lpprop_expqueue([P|T],EQ0,EQ):- 4243 update_expansion_queue(_,P,_,_,EQ0,EQ1), 4244 add_lpprop_expqueue(T,EQ1,EQ). 4245 4246 4247 4248% =================================== 4249% TABS 4250% =================================== 4251 4252/* 4253 initialize the tableau 4254 tableau is composed of: 4255 a directed graph T => tableau without label 4256 a red black tree RBN => each node is a pair of inds that contains the label for the edge 4257 a red black tree RBR => each node is a property that contains the pairs of inds 4258*/ 4259new_tabs(([],ItR,RtI)):- 4260 rb_new(ItR), 4261 rb_new(RtI). 4262 4263/* 4264 adds nodes and edges to tabs given axioms 4265*/ 4266create_tabs(L,Tableau0,Tableau):- 4267 get_tabs(Tableau0,Tabs0), 4268 create_tabs_int(L,Tabs0,Tabs), 4269 set_tabs(Tableau0,Tabs,Tableau). 4270 4271 4272create_tabs_int([],G,G). 4273 4274create_tabs_int([(propertyAssertion(P,S,O),_Expl)|T],Tabl0,Tabl):- 4275 add_edge_int(P,S,O,Tabl0,Tabl1), 4276 create_tabs_int(T,Tabl1,Tabl). 4277 4278create_tabs_int([(differentIndividuals(Ld),_Expl)|Tail],(T0,RBN,RBR),Tabs):- 4279 add_vertices(T0,Ld,T1), 4280 create_tabs_int(Tail,(T1,RBN,RBR),Tabs). 4281 4282create_tabs_int([(classAssertion(_,I),_Expl)|Tail],(T0,RBN,RBR),Tabs):- 4283 add_vertices(T0,[I],T1), 4284 create_tabs_int(Tail,(T1,RBN,RBR),Tabs). 4285 4286 4287/* 4288 add edge to tableau 4289 4290 add_edge(Property,Subject,Object,Tab0,Tab) 4291*/ 4292add_edge(P,S,O,Tableau0,Tableau):- 4293 get_tabs(Tableau0,Tabs0), 4294 add_edge_int(P,S,O,Tabs0,Tabs), 4295 set_tabs(Tableau0,Tabs,Tableau). 4296 4297add_edge_int(P,S,O,(T0,ItR0,RtI0),(T1,ItR1,RtI1)):- 4298 add_node_to_tree(P,S,O,ItR0,ItR1), 4299 add_role_to_tree(P,S,O,RtI0,RtI1), 4300 add_edge_to_tabl(P,S,O,T0,T1). 4301 4302add_node_to_tree(P,S,O,RB0,RB1):- 4303 rb_lookup((S,O),V,RB0), 4304 \+ member(P,V),!, 4305 rb_update(RB0,(S,O),[P|V],RB1). 4306 4307add_node_to_tree(P,S,O,RB0,RB0):- 4308 rb_lookup((S,O),V,RB0), 4309 member(P,V),!. 4310 4311add_node_to_tree(P,S,O,RB0,RB1):- 4312 \+ rb_lookup([S,O],_,RB0),!, 4313 rb_insert(RB0,(S,O),[P],RB1). 4314 4315add_role_to_tree(P,S,O,RB0,RB1):- 4316 rb_lookup(P,V,RB0), 4317 \+ member((S,O),V),!, 4318 rb_update(RB0,P,[(S,O)|V],RB1). 4319 4320add_role_to_tree(P,S,O,RB0,RB0):- 4321 rb_lookup(P,V,RB0), 4322 member((S,O),V),!. 4323 4324add_role_to_tree(P,S,O,RB0,RB1):- 4325 \+ rb_lookup(P,_,RB0),!, 4326 rb_insert(RB0,P,[(S,O)],RB1). 4327 4328add_edge_to_tabl(_R,Ind1,Ind2,T0,T0):- 4329 graph_edge(Ind1,Ind2,T0),!. 4330 4331add_edge_to_tabl(_R,Ind1,Ind2,T0,T1):- 4332 add_edges(T0,[Ind1-Ind2],T1). 4333 4334 4335 4336/* 4337 check for an edge 4338*/ 4339graph_edge(Ind1,Ind2,T0):- 4340 edges(T0, Edges), 4341 member(Ind1-Ind2, Edges),!. 4342 4343%graph_edge(_,_,_). 4344 4345/* 4346 remove edges and nodes from tableau 4347 4348 To remove a node from the tableau use remove_node(Node,Tabs0,Tabs) 4349*/ 4350 4351% remove_all_nodes_from_tree(Property,Subject,Object,RBN0,RBN) 4352% removes from RBN the pair key-values with key (Subject,Object) 4353% key (Subject,Object) exists 4354remove_all_nodes_from_tree(_P,S,O,RB0,RB1):- 4355 rb_lookup((S,O),_,RB0), 4356 rb_delete(RB0,(S,O),RB1). 4357 4358% key (Subject,Object) does not exist 4359remove_all_nodes_from_tree(_P,S,O,RB0,_RB1):- 4360 \+ rb_lookup((S,O),_,RB0). 4361% ---------------- 4362 4363% remove_role_from_tree(Property,Subject,Object,RBR0,RBR) 4364% remove in RBR the pair (Subject,Object) from the value associated with key Property 4365% pair (Subject,Object) does not exist for key Property 4366remove_role_from_tree(P,S,O,RB,RB):- 4367 rb_lookup(P,V,RB), 4368 \+ member((S,O),V). 4369 4370% pair (Subject,Object) exists for key Property but it is not the only pair associated to it 4371remove_role_from_tree(P,S,O,RB0,RB1):- 4372 rb_lookup(P,V,RB0), 4373 member((S,O),V), 4374 delete(V,(S,O),V1), 4375 dif(V1,[]), 4376 rb_update(RB0,P,V1,RB1). 4377 4378% pair (Subject,Object) exists for key Property and it is the only pair associated to it 4379remove_role_from_tree(P,S,O,RB0,RB1):- 4380 rb_lookup(P,V,RB0), 4381 member((S,O),V), 4382 delete(V,(S,O),V1), 4383 V1==[], 4384 rb_delete(RB0,P,RB1). 4385% ---------------- 4386 4387% remove_edge_from_table(Property,Subject,Object,Tab0,Tab) 4388% removes from T the edge from Subject to Object 4389remove_edge_from_table(_P,S,O,T,T):- 4390 \+ graph_edge(S,O,T). 4391 4392remove_edge_from_table(_P,S,O,T0,T1):- 4393 graph_edge(S,O,T0), 4394 del_edges(T0,[S-O],T1). 4395% ---------------- 4396 4397% remove_node_from_table(Subject,Tab0,Tab) 4398% removes from T the node corresponding to Subject 4399remove_node_from_table(S,T0,T1):- 4400 del_vertices(T0,[S],T1). 4401 4402 4403 4404 4405 4406% =================================== 4407% FUNCTIONS ON ABOX AND TABS 4408% =================================== 4409 4410/*********** 4411 update abox 4412 utility for tableau 4413************/ 4414modify_ABox(_,Tab,sameIndividual(LF),_Expl1,Tab):- 4415 length(LF,1),!. 4416 4417modify_ABox(M,Tab0,sameIndividual(LF),Expl1,Tab):- 4418 get_abox(Tab0,ABox0), 4419 ( ( find((sameIndividual(L),Expl0),ABox0), 4420 sort(L,LS), 4421 sort(LF,LFS), 4422 LS = LFS) -> 4423 ( absent(Expl0,Expl1,Expl), 4424 remove_from_abox(ABox0,[(sameIndividual(L),Expl0)],ABox) 4425 ) 4426 ; 4427 (ABox = ABox0,Expl = Expl1,L = LF) 4428 ), 4429 add_clash_to_tableau(M,Tab0,sameIndividual(LF),Tab1), 4430 set_abox(Tab1,[(sameIndividual(L),Expl)|ABox],Tab). 4431 4432modify_ABox(_,Tab,differentIndividuals(LF),_Expl1,Tab):- 4433 length(LF,1),!. 4434 4435modify_ABox(M,Tab0,differentIndividuals(LF),Expl1,Tab):- 4436 get_abox(Tab0,ABox0), 4437 ( find((differentIndividuals(L),Expl0),ABox0) -> 4438 ( sort(L,LS), 4439 sort(LF,LFS), 4440 LS = LFS,!, 4441 absent(Expl0,Expl1,Expl), 4442 remove_from_abox(ABox0,[(differentIndividuals(L),Expl0)],ABox) 4443 ) 4444 ; 4445 (ABox = ABox0,Expl = Expl1,L = LF) 4446 ), 4447 add_clash_to_tableau(M,Tab0,differentIndividuals(LF),Tab1), 4448 set_abox(Tab1,[(differentIndividuals(L),Expl)|ABox],Tab). 4449 4450modify_ABox(M,Tab0,C,Ind,Expl1,Tab):- 4451 get_abox(Tab0,ABox0), 4452 ( find((classAssertion(C,Ind),Expl0),ABox0) -> 4453 ( absent(Expl0,Expl1,Expl), 4454 remove_from_abox(ABox0,(classAssertion(C,Ind),Expl0),ABox) 4455 ) 4456 ; 4457 (ABox = ABox0,Expl = Expl1) 4458 ), 4459 add_clash_to_tableau(M,Tab0,C-Ind,Tab1), 4460 set_abox(Tab1,[(classAssertion(C,Ind),Expl)|ABox],Tab2), 4461 update_expansion_queue_in_tableau(M,C,Ind,Tab2,Tab). 4462 4463modify_ABox(M,Tab0,P,Ind1,Ind2,Expl1,Tab):- 4464 get_abox(Tab0,ABox0), 4465 ( find((propertyAssertion(P,Ind1,Ind2),Expl0),ABox0) -> 4466 ( absent(Expl0,Expl1,Expl), 4467 remove_from_abox(ABox0,(propertyAssertion(P,Ind1,Ind2),Expl0),ABox) 4468 ) 4469 ; 4470 (ABox = ABox0,Expl = Expl1) 4471 ), 4472 add_clash_to_tableau(M,Tab0,P-Ind1-Ind2,Tab1), 4473 set_abox(Tab1,[(propertyAssertion(P,Ind1,Ind2),Expl)|ABox],Tab2), 4474 update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab2,Tab). 4475 4476/* ************* */ 4477 4478% ------------------- 4479notDifferentIndividuals(M,X,Y,ABox):- 4480 \+ inAssertDifferentIndividuals(M,X,Y), 4481 \+ inABoxDifferentIndividuals(X,Y,ABox). 4482 4483% -------------- 4484 4485inAssertDifferentIndividuals(M,differentIndividuals(X),differentIndividuals(Y)):- 4486 !, 4487 M:differentIndividuals(LI), 4488 member(X0,X), 4489 member(X0,LI), 4490 member(Y0,Y), 4491 member(Y0,LI). 4492 4493inAssertDifferentIndividuals(M,X,sameIndividual(Y)):- 4494 !, 4495 M:differentIndividuals(LI), 4496 member(X,LI), 4497 member(Y0,Y), 4498 member(Y0,LI). 4499 4500inAssertDifferentIndividuals(M,sameIndividual(X),Y):- 4501 !, 4502 M:differentIndividuals(LI), 4503 member(X0,X), 4504 member(X0,LI), 4505 member(Y,LI). 4506 4507inAssertDifferentIndividuals(M,X,Y):- 4508 M:differentIndividuals(LI), 4509 member(X,LI), 4510 member(Y,LI). 4511 4512% ------------------ 4513 4514inABoxDifferentIndividuals(sameIndividual(X),sameIndividual(Y),ABox):- 4515 !, 4516 find((differentIndividuals(LI),_),ABox), 4517 member(X0,X), 4518 member(X0,LI), 4519 member(Y0,Y), 4520 member(Y0,LI). 4521 4522inABoxDifferentIndividuals(X,sameIndividual(Y),ABox):- 4523 !, 4524 find((differentIndividuals(LI),_),ABox), 4525 member(X,LI), 4526 member(Y0,Y), 4527 member(Y0,LI). 4528 4529inABoxDifferentIndividuals(sameIndividual(X),Y,ABox):- 4530 !, 4531 find((differentIndividuals(LI),_),ABox), 4532 member(X0,X), 4533 member(X0,LI), 4534 member(Y,LI). 4535 4536inABoxDifferentIndividuals(X,Y,ABox):- 4537 find((differentIndividuals(LI),_),ABox), 4538 member(X,LI), 4539 member(Y,LI). 4540 4541% -------------------- 4542 4543listIntersection([],_,[]). 4544 4545listIntersection([HX|TX],LCY,TI):- 4546 \+ member(HX,LCY), 4547 listIntersection(TX,LCY,TI). 4548 4549listIntersection([HX|TX],LCY,[HX|TI]):- 4550 member(HX,LCY), 4551 listIntersection(TX,LCY,TI). 4552 4553% --------------- 4554 4555findExplForClassOf(LC,LI,ABox0,Expl):- 4556 member(C,LC), 4557 member(I,LI), 4558 findClassAssertion(C,I,Expl,ABox0). 4559% member((classAssertion(C,I),Expl),ABox0). 4560 4561/* ************ */ 4562 4563 4564/* absent 4565 ========= 4566*/ 4567absent(Expl0,Expl1,Expl):- % Expl0 already present expls, Expl1 new expls to add, Expl the combination of two lists 4568 absent0(Expl0,Expl1,Expl),!. 4569 4570%------------------ 4571absent0(Expl0,Expl1,Expl):- 4572 absent1(Expl0,Expl1,Expl,Added), 4573 dif(Added,0). 4574 4575absent1(Expl,[],Expl,0). 4576 4577absent1(Expl0,[H-CP|T],[H-CP|Expl],1):- 4578 absent2(Expl0,H),!, 4579 absent1(Expl0,T,Expl,_). 4580 4581absent1(Expl0,[_|T],Expl,Added):- 4582 absent1(Expl0,T,Expl,Added). 4583 4584absent2([H-_],Expl):- !, 4585 \+ subset(H,Expl). 4586 4587absent2([H-_|T],Expl):- 4588 \+ subset(H,Expl),!, 4589 absent2(T,Expl). 4590 4591/* **************** */ 4592 4593/* 4594 build_abox 4595 =============== 4596*/ 4597 4598/*build_abox(M,ABox):- 4599 findall((classAssertion(Class,Individual),[classAssertion(Class,Individual)]),classAssertion(Class,Individual),LCA), 4600 findall((propertyAssertion(Property,Subject, Object),[propertyAssertion(Property,Subject, Object)]),propertyAssertion(Property,Subject, Object),LPA), 4601 findall((propertyAssertion(Property,Subject,Object),[subPropertyOf(SubProperty,Property,Subject,Object),propertyAssertion(SubProperty,Subject,Object)]),subPropertyOf(SubProperty,Property),LSPA), 4602 new_abox(ABox0), 4603 add_all_to_tableau(LCA,ABox0,ABox1), 4604 add_all_to_tableau(LPA,ABox1,ABox2), 4605 add_all_to_tableau(LSPA,ABox2,ABox). 4606*/ 4607 4608 4609build_abox(M,Tableau,QueryType,QueryArgs):- 4610 collect_individuals(M,QueryType,QueryArgs,ConnectedInds), 4611 get_axioms_of_individuals(M,ConnectedInds,LCA,LPA,LNA,LDIA,LSIA), 4612 new_abox(ABox0), 4613 new_tabs(Tabs0), 4614 findall(Property,M:lpPropertyAssertion(Property),LPA1), 4615 findall(Class,M:lpClassAssertion(Class),LCA1), 4616 init_expansion_queue(LCA,LCA1,LPA,LPA1,ExpansionQueue), 4617 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0), 4618 %append([LCA,LPA,LDIA],CreateTabsList), 4619 %create_tabs(CreateTabsList,Tableau0,Tableau1), 4620 append([LCA,LPA,LNA,LDIA,LSIA],AddAllList), 4621 add_all_to_tableau(M,AddAllList,Tableau0,Tableau2), 4622 merge_all_individuals(M,LSIA,Tableau2,Tableau3), 4623 add_owlThing_list(M,Tableau3,Tableau), 4624 !. 4625 4626build_abox(M,Tableau,ConnectedInds):- 4627 get_axioms_of_individuals(M,ConnectedInds,LCA,LPA,LNA,LDIA,LSIA), 4628 new_abox(ABox0), 4629 new_tabs(Tabs0), 4630 findall(Property,M:lpPropertyAssertion(Property),LPA1), 4631 findall(Class,M:lpClassAssertion(Class),LCA1), 4632 init_expansion_queue(LCA,LCA1,LPA,LPA1,ExpansionQueue), 4633 init_tableau(ABox0,Tabs0,ExpansionQueue,Tableau0), 4634 %append([LCA,LPA,LDIA],CreateTabsList), 4635 %create_tabs(CreateTabsList,Tableau0,Tableau1), 4636 append([LCA,LPA,LNA,LDIA,LSIA],AddAllList), 4637 add_all_to_tableau(M,AddAllList,Tableau0,Tableau2), 4638 merge_all_individuals(M,LSIA,Tableau2,Tableau3), 4639 add_owlThing_list(M,Tableau3,Tableau), 4640 !. 4641 4642update_abox(M,Tableau0,Tableau,AddAllList,LSIA):- 4643 add_all_to_tableau(M,AddAllList,Tableau0,Tableau2), 4644 merge_all_individuals(M,LSIA,Tableau2,Tableau3), 4645 add_owlThing_list(M,Tableau3,Tableau), 4646 !. 4647 4648 4649get_axioms_of_individuals(M,IndividualsList,LCA,LPA,LNA,LDIA,LSIA):- 4650 ( dif(IndividualsList,[]) -> 4651 ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),(member(Individual,IndividualsList),M:classAssertion(Class,Individual)),LCA), 4652 findall((propertyAssertion(Property,Subject, Object),[[propertyAssertion(Property,Subject, Object)]-[]]),(member(Subject,IndividualsList),M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA), 4653 findall(nominal(NominalIndividual),(member(NominalIndividual,IndividualsList),M:classAssertion(oneOf(_),NominalIndividual)),LNA), 4654 findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),(M:differentIndividuals(Ld),intersect(Ld,IndividualsList)),LDIA), 4655 findall((sameIndividual(L),[[sameIndividual(L)]-[]]),(M:sameIndividual(L),intersect(L,IndividualsList)),LSIA) 4656 ) 4657 ; % all the individuals 4658 ( findall((classAssertion(Class,Individual),[[classAssertion(Class,Individual)]-[]]),M:classAssertion(Class,Individual),LCA), 4659 findall((propertyAssertion(Property,Subject, Object),[[propertyAssertion(Property,Subject, Object)]-[]]),(M:propertyAssertion(Property,Subject, Object),dif('http://www.w3.org/2000/01/rdf-schema#comment',Property)),LPA), 4660 findall(nominal(NominalIndividual),M:classAssertion(oneOf(_),NominalIndividual),LNA), 4661 findall((differentIndividuals(Ld),[[differentIndividuals(Ld)]-[]]),M:differentIndividuals(Ld),LDIA), 4662 findall((sameIndividual(L),[[sameIndividual(L)]-[]]),M:sameIndividual(L),LSIA) 4663 ) 4664 ). 4665 4666 4667/* ********** */ 4668 4669/********************** 4670 4671 Explanation Management 4672 4673***********************/ 4674 4675and_all_f(M,ExplPartsList,E) :- 4676 empty_expl(M,EmptyE), 4677 and_all_f(M,ExplPartsList,EmptyE,E). 4678 4679and_all_f(_,[],E,E) :- !. 4680 4681and_all_f(M,[H|T],E0,E):- 4682 and_f(M,E0,H,E1), 4683 and_all_f(M,T,E1,E). 4684 4685initial_expl(_M,[[]-[]]):-!. 4686 4687empty_expl(_M,[[]-[]]):-!. 4688 4689delete_qp(Expl0,[QPExpl],Expl):- 4690 delete(Expl0,QPExpl,Expl). 4691 4692and_f_ax(M,Axiom,F0,F):- 4693 and_f(M,[[Axiom]-[]],F0,F). 4694 4695and_f(_M,[],[],[]):- !. 4696 4697and_f(_M,[],L,L):- !. 4698 4699and_f(_M,L,[],L):- !. 4700 4701and_f(_M,L1,L2,F):- 4702 and_f1(L1,L2,[],F). 4703 4704and_f1([],_,L,L). 4705 4706and_f1([H1-CP1|T1],L2,L3,L):- 4707 and_f2(H1,CP1,L2,L12), 4708 append(L3,L12,L4), 4709 and_f1(T1,L2,L4,L). 4710 4711and_f2(_,_,[],[]):- !. 4712 4713/* 4714and_f2(L1,CP1,[H2-CP2|T2],[H-CP|T]):- 4715 can_i_and(L1,CP1,H2,CP2),!, 4716 ( subset(L1,H2) -> 4717 H = H2 4718 ; 4719 ( subset(H2,L1) -> 4720 H = L1 4721 ; 4722 append(L1,H2,H) 4723 ) 4724 ), 4725 append(CP1,CP2,CP), 4726 and_f2(L1,CP1,T2,T). 4727*/ 4728 4729 4730and_f2(L1,CP1,[H2-CP2|T2],[H-CP|T]):- 4731 append(L1,H2,H), 4732 append(CP1,CP2,CP), 4733 and_f2(L1,CP1,T2,T). 4734 4735 4736can_i_and(L1,CP1,H2,CP2):- 4737 dif(L1,[]), 4738 dif(H2,[]), 4739 (member(A,CP1), 4740 member(A,CP2)),!. 4741 4742same_cpp_or_not(CP1,CP2):- 4743 (\+ member(cpp(_,_),CP1) ; \+ member(cpp(_,_),CP2)),!. 4744 4745or_f([],E,E). 4746 4747or_f([E0|T],E1,E):- 4748 memberchk(E0,E1),!, 4749 or_f(T,E1,E). 4750 4751or_f([E0|T],E1,[E0|E]):- 4752 or_f(T,E1,E). 4753 4754/* 4755 * merge 4756 * 4757 * Implement the Merge operation of the tableau. Merge two individuals 4758 */ 4759% The first three are needed because T in tabs:(T,RBN,RBR) saves sameIndividuals 4760% as a list instead of a single individual sameIndividual(L). 4761% The addition of sameIndividual is made after, during the update of the ABox. 4762% TODO: it could be improved! 4763/* 4764merge(M,sameIndividual(LX),sameIndividual(LY),Expl,Tableau0,Tableau):- 4765 !, 4766 get_tabs(Tableau0,Tabs0), 4767 merge_tabs(L,Y,Tabs0,Tabs), 4768 get_abox(Tableau0,ABox0), 4769 merge_abox(M,L,Y,Expl,ABox0,ABox), 4770 set_tabs(Tableau0,Tabs,Tableau1), 4771 set_abox(Tableau1,ABox,Tableau). 4772 4773merge(M,sameIndividual(L),Y,Expl,Tableau0,Tableau):- 4774 !, 4775 get_tabs(Tableau0,Tabs0), 4776 merge_tabs(L,Y,Tabs0,Tabs), 4777 get_abox(Tableau0,ABox0), 4778 merge_abox(M,L,Y,Expl,ABox0,ABox), 4779 set_tabs(Tableau0,Tabs,Tableau1), 4780 set_abox(Tableau1,ABox,Tableau). 4781*/ 4782 4783merge(M,X,Y,Expl,Tableau0,Tableau):- 4784 !, 4785 get_tabs(Tableau0,Tabs0), 4786 merge_tabs(X,Y,Tabs0,Tabs), 4787 get_abox(Tableau0,ABox0), 4788 flatten([X,Y],L0), 4789 sort(L0,L), 4790 list_as_sameIndividual(L,SI), 4791 get_clashes(Tableau0,Clashes0), 4792 merge_abox(M,L,SI,Expl,ABox0,ABox,ClashesToCheck), 4793 set_abox(Tableau0,ABox,Tableau1), 4794 check_merged_classes(M,ClashesToCheck,Tableau1,NewClashes), 4795 update_clashes_after_merge(M,L,SI,Tableau1,Clashes0,ClashesAM), 4796 append(NewClashes,ClashesAM,Clashes), 4797 set_tabs(Tableau1,Tabs,Tableau2), 4798 set_clashes(Tableau2,Clashes,Tableau3), 4799 get_expansion_queue(Tableau3,ExpQ0), 4800 update_expansion_queue_after_merge(L,SI,ExpQ0,ExpQ), 4801 set_expansion_queue(Tableau3,ExpQ,Tableau). 4802 4803 4804/* 4805 * merge node in tableau. X and Y single individuals 4806 */ 4807 4808merge_tabs(X,Y,(T0,RBN0,RBR0),(T,RBN,RBR)):- 4809 (neighbours(X,T0,LSX0)*->assign(LSX0,LSX);assign([],LSX)), 4810 (neighbours(Y,T0,LSY0)*->assign(LSY0,LSY);assign([],LSY)), 4811 transpose_ugraph(T0,TT), 4812 (neighbours(X,TT,LPX0)*->assign(LPX0,LPX);assign([],LPX)), 4813 (neighbours(Y,TT,LPY0)*->assign(LPY0,LPY);assign([],LPY)), 4814 % list_as_sameIndividual([X,Y],SI), %TODO 4815 flatten([X,Y],L0), 4816 sort(L0,SI), 4817 set_predecessor(SI,X,LPX,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),!, 4818 set_successor(SI,X,LSX,(T1,RBN1,RBR1),(T2,RBN2,RBR2)),!, 4819 set_predecessor(SI,Y,LPY,(T2,RBN2,RBR2),(T3,RBN3,RBR3)),!, 4820 set_successor(SI,Y,LSY,(T3,RBN3,RBR3),(T4,RBN4,RBR4)),!, 4821 remove_nodes(X,Y,(T4,RBN4,RBR4),(T,RBN,RBR)). 4822 4823remove_nodes(X,Y,Tabs0,Tabs):- 4824 remove_node(X,Tabs0,Tabs1), 4825 remove_node(Y,Tabs1,Tabs). 4826 4827% Collects all the connected in input (LP, predecessor) or in output (LS, successor) for node X 4828% 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)) 4829% 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 4830remove_node(X,(T0,RBN0,RBR0),(T,RBN,RBR)):- 4831 (neighbours(X,T0,LS0)*->assign(LS0,LS);assign([],LS)), 4832 transpose_ugraph(T0,TT), 4833 (neighbours(X,TT,LP0)*->assign(LP0,LP);assign([],LP)), 4834 remove_node1(X,LS,RBN0,RBR0,RBN1,RBR1), 4835 remove_node2(X,LP,RBN1,RBR1,RBN,RBR), 4836 (vertices(T0,VS),member(X,VS)*->del_vertices(T0,[X],T);assign(T0,T)). 4837 4838remove_node1(_,[],RBN,RBR,RBN,RBR). 4839 4840remove_node1(X,[H|T],RBN0,RBR0,RBN,RBR):- 4841 rb_lookup((X,H),V,RBN0), 4842 remove_edges(V,X,H,RBR0,RBR1), 4843 remove_all_nodes_from_tree(_,X,H,RBN0,RBN1), 4844 remove_node1(X,T,RBN1,RBR1,RBN,RBR). 4845 4846remove_node2(_,[],RBN,RBR,RBN,RBR). 4847 4848remove_node2(X,[H|T],RBN0,RBR0,RBN,RBR):- 4849 rb_lookup((H,X),V,RBN0), 4850 remove_edges(V,H,X,RBR0,RBR1), 4851 remove_all_nodes_from_tree(_,H,X,RBN0,RBN1), 4852 remove_node1(X,T,RBN1,RBR1,RBN,RBR). 4853 4854remove_edges([],_,_,RBR,RBR). 4855 4856remove_edges([H|T],S,O,RBR0,RBR):- 4857 remove_role_from_tree(H,S,O,RBR0,RBR1), 4858 remove_edges(T,S,O,RBR1,RBR). 4859 4860 4861set_predecessor(_NN,_,[],Tabs,Tabs). 4862 4863set_predecessor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):- 4864 rb_lookup((H,X),LR,RBN0), 4865 set_predecessor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)), 4866 set_predecessor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)). 4867 4868set_predecessor1(_NN,_H,[],Tabs,Tabs). 4869 4870set_predecessor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):- 4871 add_edge_int(R,H,NN,(T0,RBN0,RBR0),(T1,RBN1,RBR1)), 4872 set_predecessor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)). 4873 4874set_successor(_NN,_X,[],Tabs,Tabs). 4875 4876set_successor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):- 4877 rb_lookup((X,H),LR,RBN0), 4878 set_successor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)), 4879 set_successor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)). 4880 4881set_successor1(_NN,_H,[],Tabs,Tabs). 4882 4883set_successor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):- 4884 add_edge_int(R,NN,H,(T0,RBN0,RBR0),(T1,RBN1,RBR1)), 4885 set_successor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)). 4886 4887/* 4888 merge node in ABox 4889*/ 4890 4891% TODO update 4892merge_abox(_M,_L,_,_,[],[],[]). 4893 4894merge_abox(M,L,SI,Expl0,[(classAssertion(C,Ind),ExplT)|T],[(classAssertion(C,SI),Expl)|ABox],[C-SI|CTC]):- 4895 member(Ind,L),!, 4896 and_f(M,Expl0,ExplT,Expl), 4897 %and_f_ax(M,sameIndividual(L),Expl1,Expl), 4898 merge_abox(M,L,SI,Expl0,T,ABox,CTC). 4899 4900merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,SI,Ind2),Expl)|ABox],CTC):- 4901 member(Ind1,L),!, 4902 and_f(M,Expl0,ExplT,Expl), 4903 %and_f_ax(M,sameIndividual(L),Expl1,Expl), 4904 merge_abox(M,L,SI,Expl0,T,ABox,CTC). 4905 4906merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,Ind1,SI),Expl)|ABox],CTC):- 4907 member(Ind2,L),!, 4908 and_f(M,Expl0,ExplT,Expl), 4909 %and_f_ax(M,sameIndividual(L),Expl1,Expl), 4910 merge_abox(M,L,SI,Expl0,T,ABox,CTC). 4911 4912merge_abox(M,L,SI,Expl0,[H|T],[H|ABox],CTC):- 4913 merge_abox(M,L,SI,Expl0,T,ABox,CTC). 4914 4915 4916/* 4917 check for new clashes due to merge 4918 */ 4919 4920check_merged_classes(_,[],_,[]). 4921 4922check_merged_classes(M,[ToCheck|TC],Tab,[ToCheck|NewClashes]):- 4923 check_clash(M,ToCheck,Tab),!, 4924 check_merged_classes(M,TC,Tab,NewClashes). 4925 4926check_merged_classes(M,[_ToCheck|TC],Tab,NewClashes):- 4927 check_merged_classes(M,TC,Tab,NewClashes). 4928 4929/* 4930 update clashes ofter merge 4931 substitute ind in clashes with sameIndividual 4932 */ 4933 4934update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes):- 4935 update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes,0). 4936 4937% if last argument is 0 -> need to theck clash for sameIndividual/differentIndividual 4938% if there is no clash (check_clash returns false), backtrack to (*) 4939update_clashes_after_merge(M,_,SI,Tableau,[],[SI],0):- 4940 check_clash(M,SI,Tableau),!. 4941 4942% (*) 4943update_clashes_after_merge(_,_,_,_,[],[],_). 4944 4945update_clashes_after_merge(M,L,SI,Tableau,[sameIndividual(LC)|TC0],[SI|TC],0):- 4946 memberchk(I,L), 4947 memberchk(I,LC),!, 4948 update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,1). 4949 4950update_clashes_after_merge(M,L,SI,Tableau,[C-I|TC0],[C-SI|TC],UpdatedSI):- 4951 memberchk(I,L),!, 4952 update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI). 4953 4954update_clashes_after_merge(M,L,SI,Tableau,[C-sameIndividual(LOld)|TC0],[C-SI|TC],UpdatedSI):- 4955 memberchk(I,L), 4956 memberchk(I,LOld),!, 4957 update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI). 4958 4959update_clashes_after_merge(M,L,SI,Tableau,[Clash|TC0],[Clash|TC],UpdatedSI):- 4960 update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI). 4961 4962 4963 4964 4965/* 4966 update expansion queue ofter merge 4967 substitute ind in expansion queue with sameIndividual 4968 */ 4969update_expansion_queue_after_merge(L,SI,[Curr0,ExpQD0,ExpQND0],[Curr,ExpQD,ExpQND]):- 4970 update_expansion_queue_after_merge_int(L,SI,Curr0,Curr), 4971 update_expansion_queue_after_merge_int(L,SI,ExpQD0,ExpQD), 4972 update_expansion_queue_after_merge_int(L,SI,ExpQND0,ExpQND). 4973 4974update_expansion_queue_after_merge_int(_,_,[],[]). 4975 4976update_expansion_queue_after_merge_int(L,SI,[[C,I]|TC0],[[C,IN]|TC]):- 4977 substitute_individual(L,I,SI,IN), 4978 update_expansion_queue_after_merge_int(L,SI,TC0,TC). 4979 4980update_expansion_queue_after_merge_int(L,SI,[[P,S,O]|TC0],[[P,SN,ON]|TC]):- 4981 substitute_individual(L,S,SI,SN), 4982 substitute_individual(L,O,SI,ON), 4983 update_expansion_queue_after_merge_int(L,SI,TC0,TC). 4984 4985 4986/********************** 4987 4988Choice Points Management 4989 4990***********************/ 4991 4992/* 4993 Initializes delta/2 containing the list of choice points and the number of choice points created. 4994 Every choice point is modeled by the predicate cp/5 containing the ID of the choice point, 4995 the individual and the class that triggered the creation of the choice point, 4996 the rule that created the cp: 4997 - or: or_rule 4998 - mr: max_rule 4999 Also it contains the list of possible choices and the explanations for each choice. 5000*/ 5001init_delta(M):- 5002 retractall(M:delta(_,_)), 5003 assert(M:delta([],0)). 5004 5005get_choice_point_id(M,ID):- 5006 M:delta(_,ID). 5007 5008% Creates a new choice point and adds it to the delta/2 set of choice points. 5009create_choice_point(M,Ind,Rule,Class,Choices,ID0):- 5010 init_expl_per_choice(Choices,ExplPerChoice), 5011 M:delta(CPList,ID0), 5012 ID is ID0 + 1, 5013 retractall(M:delta(_,_)), 5014 assert(M:delta([cp(ID0,Ind,Rule,Class,Choices,ExplPerChoice)|CPList],ID)). 5015 5016 5017init_expl_per_choice(Choices,ExplPerChoice):- 5018 length(Choices,N), 5019 init_expl_per_choice_int(0,N,epc{0:[]},ExplPerChoice). 5020 5021init_expl_per_choice_int(N,N,ExplPerChoice,ExplPerChoice). 5022 5023init_expl_per_choice_int(N0,N,ExplPerChoice0,ExplPerChoice):- 5024 ExplPerChoice1 = ExplPerChoice0.put(N0,[]), 5025 N1 is N0 + 1, 5026 init_expl_per_choice_int(N1,N,ExplPerChoice1,ExplPerChoice). 5027 5028 5029% cpp/2 is the choice point pointer. It contains the CP's ID (from the list of choice points delta/2) 5030% and the pointer of the choice maide at the choice point 5031add_choice_point(_,_,[],[]). 5032 5033add_choice_point(_,CPP,[Expl-CP0|T0],[Expl-CP|T]):- %CPP=cpp(CPID,N) 5034 ( 5035 dif(CP0,[]) -> 5036 ( 5037 append([CPP],CP0,CP) 5038 ) 5039 ; 5040 ( 5041 CP = [CPP] 5042 ) 5043 ), 5044 add_choice_point(_,CPP,T0,T). 5045 5046 5047get_choice_point_list(M,CP):- 5048 M:delta(CP,_). 5049 5050extract_choice_point_list(M,CP):- 5051 M:delta([CP|CPList],ID), 5052 retractall(M:delta(_,_)), 5053 assert(M:delta(CPList,ID)). 5054 5055update_choice_point_list(M,ID,Choice,E,CPs):- 5056 M:delta(CPList0,ID0), 5057 memberchk(cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),CPList0), 5058 ExplToUpdate = ExplPerChoice0.get(Choice), 5059 ( % if the set of explanations for the choice is empty it simply adds the new explanation -> union i.e., append([E-CPs],ExplToUpdate,ExplUpdated) 5060 % otherwise it adds only new explanations dropping those that are already present or those that are supersets of 5061 % already present explanations -> absent(ExplToUpdate,[E-CPs],ExplUpdated) 5062 dif(ExplToUpdate,[]) -> 5063 ( 5064 or_f(ExplToUpdate,[E-CPs],ExplUpdated) 5065 ) ; 5066 ( 5067 ExplUpdated=[E-CPs] 5068 ) 5069 ), 5070 ExplPerChoice = ExplPerChoice0.put(Choice,ExplUpdated), 5071 update_choice_point_list_int(CPList0,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,CPList), 5072 retractall(M:delta(_,_)), 5073 assert(M:delta(CPList,ID0)). 5074 5075update_choice_point_list_int([],_,_,[]):- 5076 writeln("Probably something wrong happened. Please report the problem opening an issue on github!"). 5077 % It should never arrive here. 5078 5079update_choice_point_list_int([cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0)|T], 5080 cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice, 5081 [cp(ID,Ind,Rule,Class,Choices,ExplPerChoice)|T]) :- !. 5082 5083update_choice_point_list_int([H|T], 5084 cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice, 5085 [H|T1]):- 5086 update_choice_point_list_int(T,cp(ID,Ind,Rule,Class,Choices,ExplPerChoice0),ExplPerChoice,T1). 5087 5088/********************** 5089 5090 trillo Probability Computation 5091 5092***********************/ 5093/* 5094get_bdd_environment(_M,Env):- 5095 init(Env). 5096 5097clean_environment(_M,Env):- 5098 end(Env). 5099 5100 5101build_bdd(M,Env,[X],BDD):- !, 5102 bdd_and(M,Env,X,BDD). 5103 5104build_bdd(M,Env, [H|T],BDD):- 5105 build_bdd(M,Env,T,BDDT), 5106 bdd_and(M,Env,H,BDDH), 5107 or(Env,BDDH,BDDT,BDD). 5108 5109build_bdd(_M,Env,[],BDD):- !, 5110 zero(Env,BDD). 5111 5112 5113bdd_and(M,Env,[X],BDDX):- 5114 get_prob_ax(M,X,AxN,Prob),!, 5115 ProbN is 1-Prob, 5116 get_var_n(Env,AxN,[],[Prob,ProbN],VX), 5117 equality(Env,VX,0,BDDX),!. 5118 5119bdd_and(_M,Env,[_X],BDDX):- !, 5120 one(Env,BDDX). 5121 5122bdd_and(M,Env,[H|T],BDDAnd):- 5123 get_prob_ax(M,H,AxN,Prob),!, 5124 ProbN is 1-Prob, 5125 get_var_n(Env,AxN,[],[Prob,ProbN],VH), 5126 equality(Env,VH,0,BDDH), 5127 bdd_and(M,Env,T,BDDT), 5128 and(Env,BDDH,BDDT,BDDAnd). 5129 5130bdd_and(M,Env,[_H|T],BDDAnd):- !, 5131 one(Env,BDDH), 5132 bdd_and(M,Env,T,BDDT), 5133 and(Env,BDDH,BDDT,BDDAnd). 5134 5135*/ 5136 5137substitute_individual(L,sameIndividual(LSI),SI,SI):- 5138 memberchk(I,L), 5139 memberchk(I,LSI),!. 5140 5141substitute_individual(_,I,_,I):-!. 5142 5143% ==================================================== 5144% NEW STUFF 5145% ==================================================== 5146 5147update_tabs(M,Axiom) :- 5148 functor(Axiom,Pred,Arity), 5149 member(Pred/Arity,[subClassOf/2, equivalentClasses/1, disjointClasses/1, disjointUnion/2, 5150 subPropertyOf/2, equivalentProperties/1, disjointProperties/1, inverseProperties/2, propertyDomain/2, propertyRange/2, 5151 symmetricProperty/1, transitiveProperty/1, sameIndividual/1, differentIndividuals/1, classAssertion/2, propertyAssertion/3]), 5152 !, 5153 findall(Tab,M:tab_end(Tab),TabsL), 5154 retractall(M:tab_end(_)), 5155 update_tabs_int(M,Axiom,TabsL). 5156 5157update_tabs(_M,_Axiom) :- !. 5158 5159update_tabs_int(_M,_Axiom,[]) :- !. 5160 5161update_tabs_int(M,subClassOf(C1,_),[Tab|TabsL]):- 5162 get_abox(Tab,ABox), 5163 findall((classAssertion(C1,I),_),findClassAssertion(M,C1,I,_,ABox),LCA), 5164 get_expansion_queue(Tab,EQ0), 5165 add_classes_expqueue(LCA,EQ0,EQ), 5166 set_expansion_queue(Tab,EQ,NewTab), 5167 assert(M:tab_end(NewTab)), 5168 update_tabs_int(M,subClassOf(C1,_),TabsL). 5169 5170 5171update_tabs_int(M,equivalentClasses(CL),[Tab|TabsL]):- 5172 get_abox(Tab,ABox), 5173 findall((classAssertion(C1,I),_),(member(C1,CL),findClassAssertion(M,C1,I,_,ABox)),LCA), % maybe it is sufficient to find one 5174 get_expansion_queue(Tab,EQ0), 5175 add_classes_expqueue(LCA,EQ0,EQ), 5176 set_expansion_queue(Tab,EQ,NewTab), 5177 assert(M:tab_end(NewTab)), 5178 update_tabs_int(M,equivalentClasses(CL),TabsL). 5179 5180update_tabs_int(M,disjointClasses(CL),[Tab|TabsL]):- 5181 get_abox(Tab,ABox), 5182 findall((classAssertion(C1,I),_),(member(C1,CL),findClassAssertion(M,C1,I,_,ABox)),LCA), % maybe it is sufficient to find one 5183 get_expansion_queue(Tab,EQ0), 5184 add_classes_expqueue(LCA,EQ0,EQ), 5185 set_expansion_queue(Tab,EQ,NewTab), 5186 assert(M:tab_end(NewTab)), 5187 update_tabs_int(M,disjointClasses(CL),TabsL). 5188 5189update_tabs_int(M,disjointUnion(C,CL),[Tab|TabsL]):- 5190 get_abox(Tab,ABox), 5191 findall((classAssertion(C1,I),_),(member(C1,[C|CL]),findClassAssertion(M,C1,I,_,ABox)),LCA), % maybe it is sufficient to find one 5192 get_expansion_queue(Tab,EQ0), 5193 add_classes_expqueue(LCA,EQ0,EQ), 5194 set_expansion_queue(Tab,EQ,NewTab), 5195 assert(M:tab_end(NewTab)), 5196 update_tabs_int(M,disjointUnion(C,CL),TabsL). 5197 5198update_tabs_int(M,subPropertyOf(P,_),[Tab|TabsL]):- 5199 get_abox(Tab,ABox), 5200 findall((propertyAssertion(P,S,O),_),findPropertyAssertion(M,P,S,O,_,ABox),LPA), 5201 get_expansion_queue(Tab,EQ0), 5202 add_prop_expqueue(LPA,EQ0,EQ1), 5203 findall((classAssertion(C1,I),_),(member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5204 add_classes_expqueue(LCA,EQ1,EQ), 5205 set_expansion_queue(Tab,EQ,NewTab), 5206 assert(M:tab_end(NewTab)), 5207 update_tabs_int(M,subPropertyOf(P,_),TabsL). 5208 5209update_tabs_int(M,equivalentProperties(LP),[Tab|TabsL]):- 5210 get_abox(Tab,ABox), 5211 findall((propertyAssertion(P,S,O),_),(member(P,LP),findPropertyAssertion(M,P,S,O,_,ABox)),LPA), 5212 get_expansion_queue(Tab,EQ0), 5213 add_prop_expqueue(LPA,EQ0,EQ1), 5214 findall((classAssertion(C1,I),_),(member(P,LP),member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5215 add_classes_expqueue(LCA,EQ1,EQ), 5216 set_expansion_queue(Tab,EQ,NewTab), 5217 assert(M:tab_end(NewTab)), 5218 update_tabs_int(M,equivalentProperties(LP),TabsL). 5219 5220update_tabs_int(M,disjointProperties(LP),[Tab|TabsL]):- 5221 get_abox(Tab,ABox), 5222 findall((propertyAssertion(P,S,O),_),(member(P,LP),findPropertyAssertion(M,P,S,O,_,ABox)),LPA), 5223 get_expansion_queue(Tab,EQ0), 5224 add_prop_expqueue(LPA,EQ0,EQ1), 5225 findall((classAssertion(C1,I),_),(member(P,LP),member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5226 add_classes_expqueue(LCA,EQ1,EQ), 5227 set_expansion_queue(Tab,EQ,NewTab), 5228 assert(M:tab_end(NewTab)), 5229 update_tabs_int(M,disjointProperties(LP),TabsL). 5230 5231update_tabs_int(M,inverseProperties(P1,P2),[Tab|TabsL]):- 5232 get_abox(Tab,ABox), 5233 findall((propertyAssertion(P,S,O),_),(member(P,[P1,P2]),findPropertyAssertion(M,P,S,O,_,ABox)),LPA), 5234 get_expansion_queue(Tab,EQ0), 5235 add_prop_expqueue(LPA,EQ0,EQ1), 5236 findall((classAssertion(C1,I),_),(member(P,[P1,P2]),member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5237 add_classes_expqueue(LCA,EQ1,EQ), 5238 set_expansion_queue(Tab,EQ,NewTab), 5239 assert(M:tab_end(NewTab)), 5240 update_tabs_int(M,inverseProperties(P1,P2),TabsL). 5241 5242update_tabs_int(M,propertyDomain(P,_), [Tab|TabsL]):- 5243 get_abox(Tab,ABox), 5244 findall((propertyAssertion(P,S,O),_),findPropertyAssertion(M,P,S,O,_,ABox),LPA), 5245 get_expansion_queue(Tab,EQ0), 5246 add_prop_expqueue(LPA,EQ0,EQ), 5247 set_expansion_queue(Tab,EQ,NewTab), 5248 assert(M:tab_end(NewTab)), 5249 update_tabs_int(M,propertyDomain(P,_),TabsL). 5250 5251update_tabs_int(M,propertyRange(P,_), [Tab|TabsL]):- 5252 get_abox(Tab,ABox), 5253 findall((propertyAssertion(P,S,O),_),findPropertyAssertion(M,P,S,O,_,ABox),LPA), 5254 get_expansion_queue(Tab,EQ0), 5255 add_prop_expqueue(LPA,EQ0,EQ), 5256 set_expansion_queue(Tab,EQ,NewTab), 5257 assert(M:tab_end(NewTab)), 5258 update_tabs_int(M,propertyRange(P,_),TabsL). 5259 5260update_tabs_int(M,symmetricProperty(P),[Tab|TabsL]):- 5261 get_abox(Tab,ABox), 5262 findall((propertyAssertion(P,S,O),_),findPropertyAssertion(M,P,S,O,_,ABox),LPA), 5263 get_expansion_queue(Tab,EQ0), 5264 add_prop_expqueue(LPA,EQ0,EQ1), 5265 findall((classAssertion(C1,I),_),(member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5266 add_classes_expqueue(LCA,EQ1,EQ), 5267 set_expansion_queue(Tab,EQ,NewTab), 5268 assert(M:tab_end(NewTab)), 5269 update_tabs_int(M,symmetricProperty(P),TabsL). 5270 5271update_tabs_int(M,transitiveProperty(P),[Tab|TabsL]):- 5272 get_abox(Tab,ABox), 5273 findall((propertyAssertion(P,S,O),_),findPropertyAssertion(M,P,S,O,_,ABox),LPA), 5274 get_expansion_queue(Tab,EQ0), 5275 add_prop_expqueue(LPA,EQ0,EQ1), 5276 findall((classAssertion(C1,I),_),(member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5277 add_classes_expqueue(LCA,EQ1,EQ), 5278 set_expansion_queue(Tab,EQ,NewTab), 5279 assert(M:tab_end(NewTab)), 5280 update_tabs_int(M,transitiveProperty(P),TabsL). 5281 5282update_tabs_int(M,sameIndividual(L),[Tab|TabsL]):- 5283 merge_all_individuals(M,[(sameIndividual(L),[[sameIndividual(L)]-[]])],Tab,NewTab), 5284 assert(M:tab_end(NewTab)), 5285 update_tabs_int(M,sameIndividual(L),TabsL). 5286 5287update_tabs_int(M,differentIndividuals(L),[Tab|TabsL]):- 5288 get_abox(Tab,ABox), 5289 add_all_to_tableau(M,[(differentIndividuals(L),[[differentIndividuals(L)]-[]])],Tab,Tab1), 5290 findall((classAssertion(C1,I),_),(member(I,L),member(C1,[allValuesFrom(P,_), someValuesFrom(P,_),exactCardinality(_,P,_),minCardinality(_,P,_),maxCardinality(_,P,_),exactCardinality(P,_),minCardinality(P,_),maxCardinality(P,_)]),findClassAssertion(M,C1,I,_,ABox)),LCA), 5291 get_expansion_queue(Tab,EQ0), 5292 add_classes_expqueue(LCA,EQ0,EQ), 5293 set_expansion_queue(Tab1,EQ,NewTab), 5294 assert(M:tab_end(NewTab)), 5295 update_tabs_int(M,differentIndividuals(P),TabsL). 5296 5297update_tabs_int(M,classAssertion(C,I),[Tab|TabsL]):- 5298 get_axioms_of_individuals(M,[I],LCA,LPA,LNA,LDIA,LSIA), 5299 append([[(classAssertion(C,I),[[classAssertion(C,I)]-[]])],LCA,LPA,LNA,LDIA],AddAllList), 5300 add_all_to_tableau(M,AddAllList,Tab,NewTab0), 5301 merge_all_individuals(M,LSIA,NewTab0,NewTab1), 5302 add_owlThing_list(M,NewTab1,NewTab2), 5303 get_expansion_queue(NewTab2,EQ0), 5304 add_classes_expqueue(LCA,EQ0,EQ1), 5305 add_prop_expqueue(LPA,EQ1,EQ), 5306 set_expansion_queue(NewTab2,EQ,NewTab), 5307 assert(M:tab_end(NewTab)), 5308 update_tabs_int(M,classAssertion(C,I),TabsL). 5309 5310update_tabs_int(M,propertyAssertion(P,S,O),[Tab|TabsL]):- 5311 get_axioms_of_individuals(M,[S,O],LCA,LPA,LNA,LDIA,LSIA), 5312 append([[(propertyAssertion(P,S,O),[[propertyAssertion(P,S,O)]-[]])],LCA,LPA,LNA,LDIA],AddAllList), 5313 add_all_to_tableau(M,AddAllList,Tab,NewTab0), 5314 merge_all_individuals(M,LSIA,NewTab0,NewTab1), 5315 add_owlThing_list(M,NewTab1,NewTab2), 5316 get_expansion_queue(NewTab2,EQ0), 5317 add_classes_expqueue(LCA,EQ0,EQ1), 5318 add_prop_expqueue(LPA,EQ1,EQ), 5319 set_expansion_queue(NewTab2,EQ,NewTab), 5320 assert(M:tab_end(NewTab)), 5321 update_tabs_int(M,propertyAssertion(P,S,O),TabsL). 5322 5323 5324% ================================================================================================================== 5325 5326/* 5327sandbox:safe_primitive(trillo:sub_class(_,_)). 5328sandbox:safe_primitive(trillo:sub_class(_,_,_)). 5329sandbox:safe_primitive(trillo:prob_sub_class(_,_,_)). 5330sandbox:safe_primitive(trillo:instanceOf(_,_)). 5331sandbox:safe_primitive(trillo:instanceOf(_,_,_)). 5332sandbox:safe_primitive(trillo:prob_instanceOf(_,_,_)). 5333sandbox:safe_primitive(trillo:property_value(_,_,_)). 5334sandbox:safe_primitive(trillo:property_value(_,_,_,_)). 5335sandbox:safe_primitive(trillo:prob_property_value(_,_,_,_)). 5336sandbox:safe_primitive(trillo:unsat(_)). 5337sandbox:safe_primitive(trillo:unsat(_,_)). 5338sandbox:safe_primitive(trillo:prob_unsat(_,_)). 5339sandbox:safe_primitive(trillo:inconsistent_theory). 5340sandbox:safe_primitive(trillo:inconsistent_theory(_)). 5341sandbox:safe_primitive(trillo:prob_inconsistent_theory(_)). 5342sandbox:safe_primitive(trillo:axiom(_)). 5343sandbox:safe_primitive(trillo:add_kb_prefix(_,_)). 5344sandbox:safe_primitive(trillo:add_kb_prefixes(_)). 5345sandbox:safe_primitive(trillo:add_axiom(_)). 5346sandbox:safe_primitive(trillo:add_axioms(_)). 5347sandbox:safe_primitive(trillo:load_kb(_)). 5348sandbox:safe_primitive(trillo:load_owl_kb(_)). 5349*/ 5350 5351:- multifile sandbox:safe_meta/2. 5352 5353sandbox:safe_meta(trillo:sub_class(_,_),[]). 5354sandbox:safe_meta(trillo:sub_class(_,_,_),[]). 5355sandbox:safe_meta(trillo:sub_class(_,_,_,_),[]). 5356sandbox:safe_meta(trillo:all_sub_class(_,_,_),[]). 5357sandbox:safe_meta(trillo:prob_sub_class(_,_,_),[]). 5358sandbox:safe_meta(trillo:instanceOf(_,_),[]). 5359sandbox:safe_meta(trillo:instanceOf(_,_,_),[]). 5360sandbox:safe_meta(trillo:instanceOf(_,_,_,_),[]). 5361sandbox:safe_meta(trillo:all_instanceOf(_,_,_),[]). 5362sandbox:safe_meta(trillo:prob_instanceOf(_,_,_),[]). 5363sandbox:safe_meta(trillo:property_value(_,_,_),[]). 5364sandbox:safe_meta(trillo:property_value(_,_,_,_),[]). 5365sandbox:safe_meta(trillo:property_value(_,_,_,_,_),[]). 5366sandbox:safe_meta(trillo:all_property_value(_,_,_,_),[]). 5367sandbox:safe_meta(trillo:prob_property_value(_,_,_,_),[]). 5368sandbox:safe_meta(trillo:unsat(_),[]). 5369sandbox:safe_meta(trillo:unsat(_,_),[]). 5370sandbox:safe_meta(trillo:unsat(_,_,_),[]). 5371sandbox:safe_meta(trillo:all_unsat(_,_),[]). 5372sandbox:safe_meta(trillo:prob_unsat(_,_),[]). 5373sandbox:safe_meta(trillo:inconsistent_theory,[]). 5374sandbox:safe_meta(trillo:inconsistent_theory(_),[]). 5375sandbox:safe_meta(trillo:inconsistent_theory(_,_),[]). 5376sandbox:safe_meta(trillo:all_inconsistent_theory(_),[]). 5377sandbox:safe_meta(trillo:prob_inconsistent_theory(_),[]). 5378sandbox:safe_meta(trillo:resume_query(_),[]). 5379sandbox:safe_meta(trillo:compute_query_prob(_),[]). 5380sandbox:safe_meta(trillo:reset_query,[]). 5381sandbox:safe_meta(trillo:axiom(_),[]). 5382sandbox:safe_meta(trillo:kb_prefixes(_),[]). 5383sandbox:safe_meta(trillo:add_kb_prefix(_,_),[]). 5384sandbox:safe_meta(trillo:add_kb_prefixes(_),[]). 5385sandbox:safe_meta(trillo:remove_kb_prefix(_,_),[]). 5386sandbox:safe_meta(trillo:remove_kb_prefix(_),[]). 5387sandbox:safe_meta(trillo:add_axiom(_),[]). 5388sandbox:safe_meta(trillo:add_axioms(_),[]). 5389sandbox:safe_meta(trillo:load_kb(_),[]). 5390sandbox:safe_meta(trillo:load_owl_kb(_),[]). 5391sandbox:safe_meta(trillo:set_tableau_expansion_rules(_,_),[]). 5392 5393:- use_module('./trillo_utility_translation.pl'). 5394 5395user:term_expansion((:- trillo),[]):- 5396 trillo_utility_translation:get_module(M), 5397 set_algorithm(M:trillo), 5398 set_up(M), 5399 trillo_utility_translation:set_up_kb_loading(M), 5400 trillo:add_kb_prefixes(M:[('disponte'='http://ml.unife.it/disponte#'),('owl'='http://www.w3.org/2002/07/owl#')]). 5401 5402user:term_expansion((:- trillop),[]):- 5403 trillo_utility_translation:get_module(M), 5404 set_algorithm(M:trillop), 5405 set_up(M), 5406 trillo_utility_translation:set_up_kb_loading(M), 5407 trillo:add_kb_prefixes(M:['disponte'='http://ml.unife.it/disponte#','owl'='http://www.w3.org/2002/07/owl#']). 5408 5409user:term_expansion((:- tornado),[]):- 5410 trillo_utility_translation:get_module(M), 5411 set_algorithm(M:tornado), 5412 set_up(M), 5413 trillo_utility_translation:set_up_kb_loading(M), 5414 trillo:add_kb_prefixes(M:['disponte'='http://ml.unife.it/disponte#','owl'='http://www.w3.org/2002/07/owl#'])