trill_tableau.pl

    1% ==========================================================================================================
    2% TABLEAU MANAGER
    3% ==========================================================================================================
    4
    5% ======================================================================
    6% As Dict
    7% ======================================================================
    8
    9
   10
   11
   12/* initializers */

new_tabelau(-EmptyTableaus:dict): Initialize an empty tableau. /

   19new_tableau(tableau{
   20                abox:ABox, 
   21                tabs:Tabs, 
   22                clashes:[], 
   23                expq:ExpansionQueue
   24            }):-
   25    new_abox(ABox),
   26    new_tabs(Tabs),
   27    empty_expansion_queue(ExpansionQueue).

init_tabelau(+ABox:abox, +Tabs:tableau, -InitializedTableaus:dict): Initialize a tableau with the elements given in input. /

   35init_tableau(ABox,Tabs,tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}):-
   36    empty_expansion_queue(ExpansionQueue).

init_tabelau(+ABox:abox, +Tabs:tableau, +ExpansionQueue:expansion_queue, -InitializedTableaus:dict): Initialize a tableau with the lements given in input. /

   43init_tableau(ABox,Tabs,ExpansionQueue,tableau{abox:ABox, tabs:Tabs, clashes:[], expq:ExpansionQueue}).

new_abox(-ABox:list): Initialize the ABox as an empty list. /

   50new_abox([]).

new_tabs(-Tableau): Initialize the tableau tableau is composed of: a directed graph T => tableau without label a red black tree RBN => each node is a pair of inds that contains the label for the edge a red black tree RBR => each node is a property that contains the pairs of inds /

   61new_tabs(([],ItR,RtI)):-
   62    rb_new(ItR),
   63    rb_new(RtI).

empty_expansion_queue(-Exp_queue): Initialize the expansion queue as two empty lists /

   70empty_expansion_queue([[],[]]).
   71
   72
   73/* getters and setters for Tableau */
   74
   75get_abox(Tab,ABox):-
   76    ABox = Tab.abox.
   77  
   78set_abox(Tab0,ABox,Tab):-
   79    Tab = Tab0.put(abox,ABox).
   80
   81get_tabs(Tab,Tabs):-
   82    Tabs = Tab.tabs.
   83
   84set_tabs(Tab0,Tabs,Tab):-
   85    Tab = Tab0.put(tabs,Tabs).
   86
   87get_clashes(Tab,Clashes):-
   88    Clashes = Tab.clashes.
   89
   90set_clashes(Tab0,Clashes,Tab):-
   91    Tab = Tab0.put(clashes,Clashes).
   92
   93get_expansion_queue(Tab,ExpansionQueue):-
   94    ExpansionQueue = Tab.expq.
   95      
   96set_expansion_queue(Tab0,ExpansionQueue,Tab):-
   97    Tab = Tab0.put(expq,ExpansionQueue).
   98
   99
  100
  101% --------------------------------------------------------------------------------
  102
  103absence_of_clashes(Tab):-
  104    get_clashes(Tab,Clashes),
  105    Clashes=[].
  106  
  107  
  108  
  109  extract_from_expansion_queue(Tab0,EA,Tab):-
  110    get_expansion_queue(Tab0,EQ0),
  111    extract_from_expansion_queue_int(EQ0,EA,EQ),
  112    set_expansion_queue(Tab0,EQ,Tab).
  113  
  114  extract_from_expansion_queue_int([[],[EA|T]],EA,[[],T]).
  115  
  116  extract_from_expansion_queue_int([[EA|T],NonDetQ],EA,[T,NonDetQ]).
  117  
  118  expansion_queue_is_empty(Tab):-
  119    get_expansion_queue(Tab,EQ),
  120    empty_expansion_queue(EQ).
  121  
  122  
  123  same_tableau(Tab1,Tab2):-
  124    get_abox(Tab1,ABox),
  125    get_abox(Tab2,ABox),
  126    get_tabs(Tab1,Tabs),
  127    get_tabs(Tab2,Tabs).
  128  
  129  
  130  
  131  
  132  % ===================================
  133  % ABOX
  134  % ===================================
  135  
  136  /* abox as a list */
  137  
  138  
  139  
  140   
  141  /* add El to ABox */
  142  add_to_tableau(Tableau0,El,Tableau):-
  143    get_abox(Tableau0,ABox0),
  144    add_to_abox(ABox0,El,ABox),
  145    set_abox(Tableau0,ABox,Tableau).
  146  
  147  remove_from_tableau(Tableau0,El,Tableau):-
  148    get_abox(Tableau0,ABox0),
  149    remove_from_abox(ABox0,El,ABox),
  150    set_abox(Tableau0,ABox,Tableau).
  151  
  152  add_clash_to_tableau(M,Tableau0,ToCheck,Tableau):-
  153    check_clash(M,ToCheck,Tableau0),!,
  154    get_clashes(Tableau0,Clashes0),
  155    add_to_clashes(Clashes0,ToCheck,Clashes),
  156    set_clashes(Tableau0,Clashes,Tableau).
  157  
  158  add_clash_to_tableau(_,Tableau,_,Tableau).
  159  
  160  assign(L,L).
  161  /*
  162    find & control (not find)
  163  */
  164  find(El,ABox):-
  165    member(El,ABox).
  166  
  167  control(El,ABox):-
  168    \+ find(El,ABox).
  169  
  170  /* end of abox as a list */
  171  
  172  /* abox as a red-black tree */
  173  /*new_abox(T):-
  174    rb_new(T).
  175  
  176  add(A,(Ass,Ex),A1):-
  177    rb_insert(A,(Ass,Ex),[],A1).
  178  
  179  find((Ass,Ex),A):-
  180    rb_lookup((Ass,Ex),_,A).
  181  */
  182  /* end of abox as a rb tree */
  183  
  184  
  185  add_to_abox(ABox,El,[El|ABox]).
  186  
  187  remove_from_abox(ABox0,El,ABox):-
  188    delete(ABox0,El,ABox).
  189  
  190  
  191  add_to_clashes(Clashes,'http://www.w3.org/2002/07/owl#Nothing'-_,[owlnothing|Clashes]):-!.
  192  
  193  add_to_clashes(Clashes,El,[El|Clashes]).
  194  
  195  remove_from_abox(Clashes0,El,Clashes):-
  196    delete(Clashes0,El,Clashes).
  197  
  198  /*
  199    add_all_to_tableau(M,L1,L2,LO).
  200    add in L2 all item of L1
  201  */
  202  add_all_to_tableau(M,L,Tableau0,Tableau):-
  203    get_abox(Tableau0,ABox0),
  204    get_clashes(Tableau0,Clashes0),
  205    add_all_to_abox_and_clashes(M,L,Tableau0,ABox0,ABox,Clashes0,Clashes),
  206    set_abox(Tableau0,ABox,Tableau1),
  207    set_clashes(Tableau1,Clashes,Tableau).
  208  
  209  add_all_to_abox_and_clashes(_,[],_,A,A,C,C).
  210  
  211  add_all_to_abox_and_clashes(M,[(classAssertion(Class,I),Expl)|T],Tab0,A0,A,C0,C):-
  212    check_clash(M,Class-I,Tab0),!,
  213    add_to_abox(A0,(classAssertion(Class,I),Expl),A1),
  214    add_to_clashes(C0,Class-I,C1),
  215    set_abox(Tab0,A1,Tab),
  216    add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
  217  
  218  add_all_to_abox_and_clashes(M,[(sameIndividual(LI),Expl)|T],Tab0,A0,A,C0,C):-
  219    check_clash(M,sameIndividual(LI),Tab0),!,
  220    add_to_abox(A0,(sameIndividual(LI),Expl),A1),
  221    add_to_clashes(C0,sameIndividual(LI),C1),
  222    set_abox(Tab0,A1,Tab),
  223    add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
  224  
  225  add_all_to_abox_and_clashes(M,[(differentIndividuals(LI),Expl)|T],Tab0,A0,A,C0,C):-
  226    check_clash(M,differentIndividuals(LI),Tab0),!,
  227    add_to_abox(A0,(differentIndividuals(LI),Expl),A1),
  228    add_to_clashes(C0,differentIndividuals(LI),C1),
  229    set_abox(Tab0,A1,Tab),
  230    add_all_to_abox_and_clashes(M,T,Tab,A1,A,C1,C).
  231  
  232  add_all_to_abox_and_clashes(M,[H|T],Tab0,A0,A,C0,C):-
  233    add_to_abox(A0,H,A1),
  234    set_abox(Tab0,A1,Tab),
  235    add_all_to_abox_and_clashes(M,T,Tab,A1,A,C0,C).
  236  
  237  add_all_to_abox([],A,A).
  238  
  239  add_all_to_abox([H|T],A0,A):-
  240    add_to_abox(A0,H,A1),
  241    add_all_to_abox(T,A1,A).
  242  
  243  /* ************** */
  244  
  245  
  246  
  247  % ===================================
  248  % EXPANSION QUEUE
  249  % ===================================
  250  
  251  
  252  
  253  % ------------
  254  % Utility for rule application
  255  % ------------
  256  update_expansion_queue_in_tableau(M,C,Ind,Tab0,Tab):-
  257    get_expansion_queue(Tab0,ExpansionQueue0),
  258    update_expansion_queue(M,C,Ind,ExpansionQueue0,ExpansionQueue),
  259    set_expansion_queue(Tab0,ExpansionQueue,Tab).
  260  
  261  update_expansion_queue_in_tableau(M,P,Ind1,Ind2,Tab0,Tab):-
  262    get_expansion_queue(Tab0,ExpansionQueue0),
  263    update_expansion_queue(M,P,Ind1,Ind2,ExpansionQueue0,ExpansionQueue),
  264    set_expansion_queue(Tab0,ExpansionQueue,Tab).
  265  
  266  
  267  
  268  update_expansion_queue(_,unionOf(L),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
  269    delete(NDQ0,[unionOf(L),Ind],NDQ1),
  270    append(NDQ1,[[unionOf(L),Ind]],NDQ).
  271  
  272  update_expansion_queue(_,maxCardinality(N,S,C),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
  273    delete(NDQ0,[maxCardinality(N,S,C),Ind],NDQ1),
  274    append(NDQ1,[[maxCardinality(N,S,C),Ind]],NDQ).
  275  
  276  update_expansion_queue(_,maxCardinality(N,S),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
  277    delete(NDQ0,[maxCardinality(N,S),Ind],NDQ1),
  278    append(NDQ1,[[maxCardinality(N,S),Ind]],NDQ).
  279  
  280  update_expansion_queue(_,exactCardinality(N,S,C),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
  281    delete(NDQ0,[exactCardinality(N,S,C),Ind],NDQ1),
  282    append(NDQ1,[[exactCardinality(N,S,C),Ind]],NDQ).
  283  
  284  update_expansion_queue(_,exactCardinality(N,S),Ind,[DQ,NDQ0],[DQ,NDQ]):-!,
  285    delete(NDQ0,[exactCardinality(N,S),Ind],NDQ1),
  286    append(NDQ1,[[exactCardinality(N,S),Ind]],NDQ).
  287  
  288  update_expansion_queue(_,C,Ind,[DQ0,NDQ],[DQ,NDQ]):-!,
  289    delete(DQ0,[C,Ind],DQ1),
  290    append(DQ1,[[C,Ind]],DQ).
  291  
  292  update_expansion_queue(_,P,Ind1,Ind2,[DQ0,NDQ],[DQ,NDQ]):-!,
  293    delete(DQ0,[P,Ind1,Ind2],DQ1),
  294    append(DQ1,[[P,Ind1,Ind2]],DQ).
  295  
  296  
  297  init_expansion_queue(LCA,LPA,EQ):-
  298    empty_expansion_queue(EmptyEQ),
  299    add_classes_expqueue(LCA,EmptyEQ,EQ0),
  300    add_prop_expqueue(LPA,EQ0,EQ).
  301  
  302  add_classes_expqueue([],EQ,EQ).
  303  
  304  add_classes_expqueue([(classAssertion(C,I),_)|T],EQ0,EQ):-
  305    update_expansion_queue(_,C,I,EQ0,EQ1),
  306    add_classes_expqueue(T,EQ1,EQ).
  307  
  308  add_prop_expqueue([],EQ,EQ).
  309  
  310  add_prop_expqueue([(propertyAssertion(P,S,O),_)|T],EQ0,EQ):-
  311    update_expansion_queue(_,P,S,O,EQ0,EQ1),
  312    add_prop_expqueue(T,EQ1,EQ).
  313  
  314  
  315  
  316  
  317  % ===================================
  318  % TABS
  319  % ===================================
  320  
  321  
  322  
  323  /*
  324    adds nodes and edges to tabs given axioms
  325  */
  326  create_tabs(L,Tableau0,Tableau):-
  327    get_tabs(Tableau0,Tabs0),
  328    create_tabs_int(L,Tabs0,Tabs),
  329    set_tabs(Tableau0,Tabs,Tableau).
  330  
  331  
  332  create_tabs_int([],G,G).
  333    
  334  create_tabs_int([(propertyAssertion(P,S,O),_Expl)|T],Tabl0,Tabl):-
  335    add_edge_int(P,S,O,Tabl0,Tabl1),
  336    create_tabs_int(T,Tabl1,Tabl).
  337    
  338  create_tabs_int([(differentIndividuals(Ld),_Expl)|Tail],(T0,RBN,RBR),Tabs):-
  339    add_vertices(T0,Ld,T1),
  340    create_tabs_int(Tail,(T1,RBN,RBR),Tabs).
  341  
  342  create_tabs_int([(classAssertion(_,I),_Expl)|Tail],(T0,RBN,RBR),Tabs):-
  343    add_vertices(T0,[I],T1),
  344    create_tabs_int(Tail,(T1,RBN,RBR),Tabs).
  345  
  346  
  347  /*
  348    add edge to tableau
  349  
  350    add_edge(Property,Subject,Object,Tab0,Tab)
  351  */
  352  add_edge(P,S,O,Tableau0,Tableau):-
  353    get_tabs(Tableau0,Tabs0),
  354    add_edge_int(P,S,O,Tabs0,Tabs),
  355    set_tabs(Tableau0,Tabs,Tableau).
  356  
  357  add_edge_int(P,S,O,(T0,ItR0,RtI0),(T1,ItR1,RtI1)):-
  358    add_node_to_tree(P,S,O,ItR0,ItR1),
  359    add_role_to_tree(P,S,O,RtI0,RtI1),
  360    add_edge_to_tabl(P,S,O,T0,T1).
  361  
  362  add_node_to_tree(P,S,O,RB0,RB1):-
  363    rb_lookup((S,O),V,RB0),
  364    \+ member(P,V),!,
  365    rb_update(RB0,(S,O),[P|V],RB1).
  366  
  367  add_node_to_tree(P,S,O,RB0,RB0):-
  368    rb_lookup((S,O),V,RB0),
  369    member(P,V),!.
  370  
  371  add_node_to_tree(P,S,O,RB0,RB1):-
  372    \+ rb_lookup([S,O],_,RB0),!,
  373    rb_insert(RB0,(S,O),[P],RB1).
  374  
  375  add_role_to_tree(P,S,O,RB0,RB1):-
  376    rb_lookup(P,V,RB0),
  377    \+ member((S,O),V),!,
  378    rb_update(RB0,P,[(S,O)|V],RB1).
  379  
  380  add_role_to_tree(P,S,O,RB0,RB0):-
  381    rb_lookup(P,V,RB0),
  382    member((S,O),V),!.
  383  
  384  add_role_to_tree(P,S,O,RB0,RB1):-
  385    \+ rb_lookup(P,_,RB0),!,
  386    rb_insert(RB0,P,[(S,O)],RB1).
  387  
  388  add_edge_to_tabl(_R,Ind1,Ind2,T0,T0):-
  389    graph_edge(Ind1,Ind2,T0),!.
  390  
  391  add_edge_to_tabl(_R,Ind1,Ind2,T0,T1):-
  392    add_edges(T0,[Ind1-Ind2],T1).
  393  
  394  
  395  
  396  /*
  397    check for an edge
  398  */
  399  graph_edge(Ind1,Ind2,T0):-
  400    edges(T0, Edges),
  401    member(Ind1-Ind2, Edges),!.
  402  
  403  %graph_edge(_,_,_).
  404  
  405  /*
  406    remove edges and nodes from tableau
  407  
  408    To remove a node from the tableau use remove_node(Node,Tabs0,Tabs)
  409  */
  410  
  411  % remove_all_nodes_from_tree(Property,Subject,Object,RBN0,RBN)
  412  % removes from RBN the pair key-values with key (Subject,Object)
  413  % key (Subject,Object) exists
  414  remove_all_nodes_from_tree(_P,S,O,RB0,RB1):-
  415    rb_lookup((S,O),_,RB0),
  416    rb_delete(RB0,(S,O),RB1).
  417  
  418  % key (Subject,Object) does not exist
  419  remove_all_nodes_from_tree(_P,S,O,RB0,_RB1):-
  420    \+ rb_lookup((S,O),_,RB0).
  421  % ----------------
  422  
  423  % remove_role_from_tree(Property,Subject,Object,RBR0,RBR)
  424  % remove in RBR the pair (Subject,Object) from the value associated with key Property
  425  % pair (Subject,Object) does not exist for key Property
  426  remove_role_from_tree(P,S,O,RB,RB):-
  427    rb_lookup(P,V,RB),
  428    \+ member((S,O),V).
  429  
  430  % pair (Subject,Object) exists for key Property but it is not the only pair associated to it
  431  remove_role_from_tree(P,S,O,RB0,RB1):-
  432    rb_lookup(P,V,RB0),
  433    member((S,O),V),
  434    delete(V,(S,O),V1),
  435    dif(V1,[]),
  436    rb_update(RB0,P,V1,RB1).
  437  
  438  % pair (Subject,Object) exists for key Property and it is the only pair associated to it
  439  remove_role_from_tree(P,S,O,RB0,RB1):-
  440    rb_lookup(P,V,RB0),
  441    member((S,O),V),
  442    delete(V,(S,O),V1),
  443    V1==[],
  444    rb_delete(RB0,P,RB1).
  445  % ----------------
  446  
  447  % remove_edge_from_table(Property,Subject,Object,Tab0,Tab)
  448  % removes from T the edge from Subject to Object
  449  remove_edge_from_table(_P,S,O,T,T):-
  450    \+ graph_edge(S,O,T).
  451  
  452  remove_edge_from_table(_P,S,O,T0,T1):-
  453    graph_edge(S,O,T0),
  454    del_edges(T0,[S-O],T1).
  455  % ----------------
  456  
  457  % remove_node_from_table(Subject,Tab0,Tab)
  458  % removes from T the node corresponding to Subject
  459  remove_node_from_table(S,T0,T1):-
  460    del_vertices(T0,[S],T1).
  461  
  462  
  463  
  464  
  465  
  466  % ===================================
  467  % FUNCTIONS ON ABOX AND TABS
  468  % ===================================
  469  
  470  /*
  471   * merge
  472   * 
  473   * Implement the Merge operation of the tableau. Merge two individuals
  474   */
  475  % The first three are needed because T in tabs:(T,RBN,RBR) saves sameIndividuals
  476  % as a list instead of a single individual sameIndividual(L).
  477  % The addition of sameIndividual is made after, during the update of the ABox.
  478  % TODO: it could be improved!
  479  /*
  480  merge(M,sameIndividual(LX),sameIndividual(LY),Expl,Tableau0,Tableau):-
  481    !,
  482    get_tabs(Tableau0,Tabs0),
  483    merge_tabs(L,Y,Tabs0,Tabs),
  484    get_abox(Tableau0,ABox0),
  485    merge_abox(M,L,Y,Expl,ABox0,ABox),
  486    set_tabs(Tableau0,Tabs,Tableau1),
  487    set_abox(Tableau1,ABox,Tableau).
  488  
  489  merge(M,sameIndividual(L),Y,Expl,Tableau0,Tableau):-
  490    !,
  491    get_tabs(Tableau0,Tabs0),
  492    merge_tabs(L,Y,Tabs0,Tabs),
  493    get_abox(Tableau0,ABox0),
  494    merge_abox(M,L,Y,Expl,ABox0,ABox),
  495    set_tabs(Tableau0,Tabs,Tableau1),
  496    set_abox(Tableau1,ABox,Tableau).
  497  */
  498  
  499  merge(M,X,Y,Expl,Tableau0,Tableau):-
  500    !,
  501    get_tabs(Tableau0,Tabs0),
  502    merge_tabs(X,Y,Tabs0,Tabs),
  503    get_abox(Tableau0,ABox0),
  504    flatten([X,Y],L0),
  505    sort(L0,L),
  506    list_as_sameIndividual(L,SI),
  507    get_clashes(Tableau0,Clashes0),
  508    merge_abox(M,L,SI,Expl,ABox0,ABox,ClashesToCheck),
  509    set_abox(Tableau0,ABox,Tableau1),
  510    check_merged_classes(M,ClashesToCheck,Tableau1,NewClashes),
  511    update_clashes_after_merge(M,L,SI,Tableau1,Clashes0,ClashesAM),
  512    append(NewClashes,ClashesAM,Clashes),
  513    set_tabs(Tableau1,Tabs,Tableau2),
  514    set_clashes(Tableau2,Clashes,Tableau3),
  515    get_expansion_queue(Tableau3,ExpQ0),
  516    update_expansion_queue_after_merge(L,SI,ExpQ0,ExpQ),
  517    set_expansion_queue(Tableau3,ExpQ,Tableau).
  518  
  519  
  520  /*
  521   * merge node in tableau. X and Y single individuals
  522   */
  523  
  524  merge_tabs(X,Y,(T0,RBN0,RBR0),(T,RBN,RBR)):-
  525    (neighbours(X,T0,LSX0)*->assign(LSX0,LSX);assign([],LSX)),
  526    (neighbours(Y,T0,LSY0)*->assign(LSY0,LSY);assign([],LSY)),
  527    transpose_ugraph(T0,TT),
  528    (neighbours(X,TT,LPX0)*->assign(LPX0,LPX);assign([],LPX)),
  529    (neighbours(Y,TT,LPY0)*->assign(LPY0,LPY);assign([],LPY)),
  530    % list_as_sameIndividual([X,Y],SI), %TODO
  531    flatten([X,Y],L0),
  532    sort(L0,SI),
  533    set_predecessor(SI,X,LPX,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),!,
  534    set_successor(SI,X,LSX,(T1,RBN1,RBR1),(T2,RBN2,RBR2)),!,
  535    set_predecessor(SI,Y,LPY,(T2,RBN2,RBR2),(T3,RBN3,RBR3)),!,
  536    set_successor(SI,Y,LSY,(T3,RBN3,RBR3),(T4,RBN4,RBR4)),!,
  537    remove_nodes(X,Y,(T4,RBN4,RBR4),(T,RBN,RBR)).
  538  
  539  remove_nodes(X,Y,Tabs0,Tabs):-
  540    remove_node(X,Tabs0,Tabs1),
  541    remove_node(Y,Tabs1,Tabs).
  542  
  543  % Collects all the connected in input (LP, predecessor) or in output (LS, successor) for node X
  544  % 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))
  545  % 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
  546  remove_node(X,(T0,RBN0,RBR0),(T,RBN,RBR)):-
  547    (neighbours(X,T0,LS0)*->assign(LS0,LS);assign([],LS)),
  548    transpose_ugraph(T0,TT),
  549    (neighbours(X,TT,LP0)*->assign(LP0,LP);assign([],LP)),
  550    remove_node1(X,LS,RBN0,RBR0,RBN1,RBR1),
  551    remove_node2(X,LP,RBN1,RBR1,RBN,RBR),
  552    (vertices(T0,VS),member(X,VS)*->del_vertices(T0,[X],T);assign(T0,T)).
  553  
  554  remove_node1(_,[],RBN,RBR,RBN,RBR).
  555  
  556  remove_node1(X,[H|T],RBN0,RBR0,RBN,RBR):-
  557    rb_lookup((X,H),V,RBN0),
  558    remove_edges(V,X,H,RBR0,RBR1),
  559    remove_all_nodes_from_tree(_,X,H,RBN0,RBN1),
  560    remove_node1(X,T,RBN1,RBR1,RBN,RBR).
  561  
  562  remove_node2(_,[],RBN,RBR,RBN,RBR).
  563  
  564  remove_node2(X,[H|T],RBN0,RBR0,RBN,RBR):-
  565    rb_lookup((H,X),V,RBN0),
  566    remove_edges(V,H,X,RBR0,RBR1),
  567    remove_all_nodes_from_tree(_,H,X,RBN0,RBN1),
  568    remove_node1(X,T,RBN1,RBR1,RBN,RBR).
  569  
  570  remove_edges([],_,_,RBR,RBR).
  571  
  572  remove_edges([H|T],S,O,RBR0,RBR):-
  573    remove_role_from_tree(H,S,O,RBR0,RBR1),
  574    remove_edges(T,S,O,RBR1,RBR).
  575  
  576  
  577  set_predecessor(_NN,_,[],Tabs,Tabs).
  578  
  579  set_predecessor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
  580    rb_lookup((H,X),LR,RBN0),
  581    set_predecessor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
  582    set_predecessor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
  583  
  584  set_predecessor1(_NN,_H,[],Tabs,Tabs).
  585  
  586  set_predecessor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
  587    add_edge_int(R,H,NN,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
  588    set_predecessor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
  589  
  590  set_successor(_NN,_X,[],Tabs,Tabs).
  591  
  592  set_successor(NN,X,[H|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
  593    rb_lookup((X,H),LR,RBN0),
  594    set_successor1(NN,H,LR,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
  595    set_successor(NN,X,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
  596  
  597  set_successor1(_NN,_H,[],Tabs,Tabs).
  598  
  599  set_successor1(NN,H,[R|L],(T0,RBN0,RBR0),(T,RBN,RBR)):-
  600    add_edge_int(R,NN,H,(T0,RBN0,RBR0),(T1,RBN1,RBR1)),
  601    set_successor1(NN,H,L,(T1,RBN1,RBR1),(T,RBN,RBR)).
  602  
  603  /*
  604    merge node in ABox
  605  */
  606  
  607  % TODO update
  608  merge_abox(_M,_L,_,_,[],[],[]).
  609  
  610  merge_abox(M,L,SI,Expl0,[(classAssertion(C,Ind),ExplT)|T],[(classAssertion(C,SI),Expl)|ABox],[C-SI|CTC]):-
  611    member(Ind,L),!,
  612    and_f(M,Expl0,ExplT,Expl),
  613    %and_f_ax(M,sameIndividual(L),Expl1,Expl),
  614    merge_abox(M,L,SI,Expl0,T,ABox,CTC).
  615  
  616  merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,SI,Ind2),Expl)|ABox],CTC):-
  617    member(Ind1,L),!,
  618    and_f(M,Expl0,ExplT,Expl),
  619    %and_f_ax(M,sameIndividual(L),Expl1,Expl),
  620    merge_abox(M,L,SI,Expl0,T,ABox,CTC).
  621  
  622  merge_abox(M,L,SI,Expl0,[(propertyAssertion(P,Ind1,Ind2),ExplT)|T],[(propertyAssertion(P,Ind1,SI),Expl)|ABox],CTC):-
  623    member(Ind2,L),!,
  624    and_f(M,Expl0,ExplT,Expl),
  625    %and_f_ax(M,sameIndividual(L),Expl1,Expl),
  626    merge_abox(M,L,SI,Expl0,T,ABox,CTC).
  627  
  628  merge_abox(M,L,SI,Expl0,[H|T],[H|ABox],CTC):-
  629    merge_abox(M,L,SI,Expl0,T,ABox,CTC).
  630  
  631  
  632  /*
  633    check for new clashes due to merge
  634   */
  635  
  636  check_merged_classes(_,[],_,[]).
  637  
  638  check_merged_classes(M,[ToCheck|TC],Tab,[ToCheck|NewClashes]):-
  639    check_clash(M,ToCheck,Tab),!,
  640    check_merged_classes(M,TC,Tab,NewClashes).
  641  
  642  check_merged_classes(M,[_ToCheck|TC],Tab,NewClashes):-
  643    check_merged_classes(M,TC,Tab,NewClashes).
  644  
  645  /*
  646   update clashes ofter merge
  647   substitute ind in clashes with sameIndividual
  648   */
  649  
  650  update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes):-
  651    update_clashes_after_merge(M,L,SI,Tableau,Clashes0,Clashes,0).
  652  
  653  % if last argument is 0 -> need to theck clash for sameIndividual/differentIndividual
  654  % if there is no clash (check_clash returns false), backtrack to (*)
  655  update_clashes_after_merge(M,_,SI,Tableau,[],[SI],0):-
  656    check_clash(M,SI,Tableau),!.
  657  
  658  % (*)
  659  update_clashes_after_merge(_,_,_,_,[],[],_).
  660  
  661  update_clashes_after_merge(M,L,SI,Tableau,[sameIndividual(LC)|TC0],[SI|TC],0):-
  662    memberchk(I,L),
  663    memberchk(I,LC),!,
  664    update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,1).
  665  
  666  update_clashes_after_merge(M,L,SI,Tableau,[C-I|TC0],[C-SI|TC],UpdatedSI):-
  667    memberchk(I,L),!,
  668    update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
  669  
  670  update_clashes_after_merge(M,L,SI,Tableau,[C-sameIndividual(LOld)|TC0],[C-SI|TC],UpdatedSI):-
  671    memberchk(I,L),
  672    memberchk(I,LOld),!,
  673    update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
  674  
  675  update_clashes_after_merge(M,L,SI,Tableau,[Clash|TC0],[Clash|TC],UpdatedSI):-
  676    update_clashes_after_merge(M,L,SI,Tableau,TC0,TC,UpdatedSI).
  677  
  678  
  679  
  680  
  681  /*
  682   update expansion queue ofter merge
  683   substitute ind in expansion queue with sameIndividual
  684   */
  685  update_expansion_queue_after_merge(L,SI,[ExpQD0,ExpQND0],[ExpQD,ExpQND]):-
  686    update_expansion_queue_after_merge_int(L,SI,ExpQD0,ExpQD),
  687    update_expansion_queue_after_merge_int(L,SI,ExpQND0,ExpQND).
  688  
  689  update_expansion_queue_after_merge_int(_,_,[],[]).
  690  
  691  update_expansion_queue_after_merge_int(L,SI,[[C,I]|TC0],[[C,IN]|TC]):-
  692    substitute_individual(L,I,SI,IN),
  693    update_expansion_queue_after_merge_int(L,SI,TC0,TC).
  694  
  695  update_expansion_queue_after_merge_int(L,SI,[[P,S,O]|TC0],[[P,SN,ON]|TC]):-
  696    substitute_individual(L,S,SI,SN),
  697    substitute_individual(L,O,SI,ON),
  698    update_expansion_queue_after_merge_int(L,SI,TC0,TC).
  699  
  700  substitute_individual(L,sameIndividual(LSI),SI,SI):-
  701    memberchk(I,L),
  702    memberchk(I,LSI),!.
  703  
  704  substitute_individual(_,I,_,I):-!.
  705  
  706  
  707  
  708  % ==================================================================================================================