Aspects of Distributed and Modular Ontology Reasoning
Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence. Pages 570-574.
© 2005 International Joint Conferences on Artificial Intelligence
Abstract
We investigate a formalism for reasoning with multiple local ontologies, connected by directional semantic mappings. We propose: (1) a relatively small change of semantics which localizes inconsistency (thereby making unnecessary global satisfiability checks), and preserves directionality of “knowledge import”; (2) a characterization of inferences using a fixed-point operator, which can form the basis of a cache-based implementation for local reasoners; (3) a truly distributed tableaux algorithm for cases when the local reasoners use subsets of SHIQ. Throughout, we indicate the applicability of the results to several recent proposals for knowledge representation and reasoning that support modularity, scalability and distributed reasoning.
- F. Baader, D. Calvanese, D. McGuinness, D. Nardi, P.F. Patel-Schneider, editors. The Description Logic Hand- book, Cambridge University Press, 2003.
- A. Borgida and L. Serafini. "Distributed description log- ics: Assimilating information from peer sources", J. of Data Semantics 1(1), pp.153-184, 2003.
- P. Bouquet, F. Giunchiglia, F. van Harmelen, L. Serafini, and H. Stuckenschmidt. "Contextualizing ontologies", J. of Web Semantics 1(4), 2004.
- B. Cuenca Grau, B. Parsia, E. Sirin. "Working with Mul- tiple Ontologies on the Semantic Web", Proc. ISWC'04, LNCS vol.3298, pp.620-634. 2004.
- C. Ghidini and F. Giunchiglia. "Local model semantics, or contextual reasoning = locality + compatibility", Artifi- cial Intelligence, 127(2):221-259, 2001.
- C. Ghidini and L. Serafini. "Distributed first order log- ics", Proc. Frontiers of Combining Systems, pp.121-139, 2000.
- I. Horrocks, U. Sattler, and S. Tobies. A description logic with transitive and converse roles, role hierarchies and qualifying number restriction. Technical Report 99- 08, Technische Universität Dresden, LTCS, 1999.
- M-C. Rousset. "Small can be beautiful in the Semantic Web", Proc. ISWC'04, LNCS vol.3298, pp.6-16, 2004.
- H. Stuckenschmidt and M. Klein. "Integrity and change in modular ontologies", IJCAI'03, pp.900-908, 2003. IJCAI
- D. Calvanese, G. De Giacomo, M. Lenzerini, R. Rosati. "Logical foundations of peer-to-peer data integration", PODS'04, pp.241-251, 2004.
References were extracted automatically from the PDF and may contain errors.
Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.
1 Introduction
In applications ranging from information and service integration to the semantic web, it is expected that ontologies will be fragmented and distributed, rather than monolithic. Moreover, there are well-known advantages to breaking up a large ontology into modules (e.g., see [9]). Recently, there have been a number of proposals for systems supporting modularized ontologies, where one can have a localized view either by "importing" specific information [9; 3] or by distributing reasoning [8; 4; 10].
Distributed Description Logics (DDLs) [2] are a particular formalization of the notion of distributed ontology and reasoning, which starts from local T-boxes, and expresses semantic connections between them as "bridge rules" between pairs of connects. This paper contributes to the study of DDLs, with the hope of shedding light both on the semantic and the implementation aspects of all similar mechanisms.
In particular, the claimed contributions of the paper are three-fold. First, on the semantic front, we propose a new semantics for DDLs, which better captures the properties of localized inconsistency and directionality. According to the directionality property, semantic mappings have a direction from a source ontology to a target ontology, and support knowledge propagation only in such a direction. According
Andrei Tamilin
DIT - University of Trento Via Sommarive 14 38050 Trento, Italy
tamilin@dit.unitn.it
to localized inconsistency, the inconsistency in one component T-box, or in some subgroup of connected components, should not automatically render the entire system inconsistent. These properties are desirable for all multi-module ontologies, and we discuss how our results apply to other proposals, such as [9; 3; 8].
Second, we examine an approach which views the bridge rules connecting two local ontologies as describing an operator that propagates knowledge in the form of DL subsumption axioms. This is used as the basis of a characterization of distributed DL reasoning using a fixed point operator, which does forward-propagation of axioms. In addition to its intrinsic interest, as part of a syntactic characterization of the DDL consequence relation, this result can be used to extend the caching technique described in [9] to a sound and complete one.
The third contribution is a sound and complete distributed tableaux algorithm that determines the satisfiability of a SHIQ concept in the context of the local axioms of an ontology and the extra knowledge imparted by the bridge rules. This algorithm is the basis of a peer-to-peer implementation of a proof mechanism for checking concept subsumption in a distributed manner.
The rest of the paper is organized as follows. In Section 2 we review the formal framework of DDLs. In Section 3 we introduce the notion of inconsistent local interpretation that allows us to model partially inconsistent distributed ontologies, and show exactly how the new and old entailments are related. The new semantics is also used in Section 4 to characterize the knowledge flow induced by bridge rules, and in Section 5 to present a sound and complete distributed tableaux algorithm that computes satisfiability/subsumption.
2 Distributed Description Logics
We briefly recall the definition of DDL as given by Borgida and Serafini [2].
Syntax Given a non-empty set I of indexes, used to enumerate local ontologies, let {DLi}i∈I be a collection of description logics. 1 For each i ∈ I, let us denote a T-box of DLi as Ti. 2 To make every description D distinct, we will prefix it with the index of ontology it belongs to, as in i : C. We use i : C ⊑ D to say that C ⊑ D is being considered in the i-th ontology.
1 We assume the reader is familiar with description logics and related reasoning systems, as described in [1].


Semantic mappings between different ontologies are expressed via bridge rules. A bridge rule from i to j is an expression, which in this paper is restricted to being one of the following two forms:
where x and y are concepts. The derived bridge rule i : x ≡ -→ j : y can be defined as the conjunction the corresponding into and onto bridge rule.
Bridge rules from i to j express relations between i and j viewed from the subjective point of view of the j-th ontology.
For example, the into-bridge rule i : C ⊑ -→ j : D intuitively says that, from the j-th point of view, the individuals in concept C in i correspond (via an approximation introduced by an implicit semantic domain relation) to a subset of the individuals in its local concept D. Therefore, bridge rules from i to j provide the possibility of translating into j's ontology some of the concepts of a foreign ontology i.
A distributed T-box (DTBox) T = 〈{Ti}i∈I,B〉 therefore consists of a collection of T-boxes {Ti}i∈I, and a collection of bridge rules B = {Bij}i̸=j∈I between them.
Example 2.1 Figure 1 shows fragments of class hierarchies from two ontologies, SWRC 3 and SHOE 4 , available from the DAML on-line library. These can be viewed as local T-boxes. For the sake of demonstrating the value of mappings, we considered oversimplified SHOE ontology without imports. The following are examples of bridge rules from SWRC to SHOE:
2 We assume that a T-box will contain all the information necessary to define the terminology of a domain, including not just concept and role definitions, but also general axioms relating descriptions, as well as declarations such as the transitivity of certain roles. This is in keeping with the intent of the original paper introducing the terms T-box and A-box.
3 www.semanticweb.org/ontologies/swrc-onto-2000-09-10.daml
4 www.cs.umd.edu/projects/plus/DAML/onts/univ1.0.daml
SWRC : Publication ≡ -→ SHOE : Publication (1) SWRC : InProceedings ⊑ -→ SHOE : ConferencePaper ⊔WorkshopPaper (2) SWRC : InBook ⊒ -→ SHOE : BookArticle (3)
Semantics DDL semantics is a customization of the Local Models Semantics for Multi Context Systems [5; 6]. Each ontology Ti is locally interpreted by a standard DL interpretation Ii = 〈ΔIi , ·Ii 〉. Since local domains may be heterogeneous (e.g., time may be represented by Rationals and Integers in two ontologies), we need relations that model semantic correspondences between heterogeneous domains. A domain relation rij fromΔIi toΔIj is a subset ofΔIi ×ΔIj . For example, if ΔI1 and ΔI2 are the Rationals and the Naturals, then r12 could be the round-off function. We use rij(d) to denote {d′ ∈ ΔIj | 〈d, d′ 〉 ∈ rij}; for D ⊆ ΔIi , we use rij (D) for ⋃d∈D rij (d).
A distributed interpretation I = 〈{Ii}i∈I, {rij}i̸=j∈I〉 of a DTBox T therefore combines the above two notions and is said to satisfy (written I ⊨d) the elements of T if
1. Ii ⊨d A ⊑ B for all A ⊑ B in Ti 2. I ⊨d i : x ⊑ -→ j : y, if rij(xIi ) ⊆ yIj 3. I ⊨d i : x ⊒ -→ j : y, if rij(xIi ) ⊇ yIj
- I ⊨d T, if for every i, j ∈ I, I ⊨d Ti and I ⊨d Bij
Finally, T ⊨d i : C ⊑ D (read as "T d-entails i : C ⊑ D") if for every I, I ⊨d T implies I ⊨d i : C ⊑ D. We say T is satisfiable if there exists a I such that I ⊨d T. Concept i : C is satisfiable with respect to T if there is a I such that I ⊨d T and C Ii ̸= ∅.
On injective domain correspondences A key novelty of the semantic mappings in DDL is support for multiple levels of granularity and perspective: allowing individuals to be related using arbitrary binary relations rather than just bijection. For example, while it is traditional to state correspondences such as "Wife in Ontology 1 corresponds to Moglie in Ontology 2", DDLs support domain correspondences that are general binary relations, so that one can say that "Husband and Wife in ontology 1 correspond to Couple in Ontology 2", which can be formalized by using onto-bridge rules {1 : Wife ⊒ -→ 2 : Couple, 1 : Husband ⊒ -→ 2 : Couple}. In [4], DDLs are faulted because the collection of bridge rules {1 : Bird ⊒ -→ 2 : Penguin, 1 : ¬Fly ⊒ -→ 2 : Penguin} do not render Penguin unsatifiable even if Bird is subsumed by Fly in Ontology 1. As the example involving Couple shows, the general formal pattern is correct in some cases, so this is actually a problem of incomplete modeling.
In the case of Penguins, the extra information is that the domain relation is one-to-one. In such cases, one should also have added bridge rules stating that non-birds and flying ob-
jects are non-penguins: {1 : ¬Bird ⊑ -→ 2 : ¬Penguin, 1 :
Fly ⊑ -→ 2 : ¬Penguin}. This would indeed lead to the conclusion T |=d 2 : Penguin ⊑ ⊥.
Since the property that the domain relation is one-one over some concept B arises quite frequently, we might consider adding a new kind of bridge rule to express it, writing something like ≤1 -→ Penguin. Interestingly, it can be proven that in the context of DDLs, such rules can be eliminated by syntactically manipulating the DTBox, so that whenever ≤1 -→ G and A ⊒ -→ H are present, a new bridge rule ¬A ⊑ -→ ¬(H ⊓ G) is added. The tableaux technique in Section 5 could however use such rules more efficiently without the encoding.
Properties and Desiderata for DDL We first give some basic ways in which subsumption and a combination of onto- and into-bridge rules allows to propagate subsumptions across ontologies.
Thus, in Example 2.1, the subsumption SHOE : BookArticle ⊑ Publication can be inferred in DDL through bridge rules (1) and (3), and the subsumption InBook ⊑ Publication contained in TSWRC.
If the local languages support disjunction as a concept constructor then a more general form of propagation can occur:
Additional properties would be desirable for DDL entailment. In particular, since the intended meaning is that bridge rules Bij constitute a semantic channel which allows ontology j to access and import knowledge from ontology i, we want information flow to be "directional" in some sense. To express this, we first introduce the notion of bridge graph.
Definition 2.1 The bridge graph GT of a DTBox T is a directed graph with an arc from i to j exactly when the set of bridge rules Bij is non-empty.
We can then state the main property we are looking for as:
Directionality desideratum If in GT there is no path from i to j, then T |=d j : A ⊑ B if and only if T′ |=d j : A ⊑ B, where T′ is obtained by removing Ti, Bki, and Bik fromT.
This says that knowledge is propagated only through bridge rules, so that if there are no bridge rules that go from i towards j, then j is not affected by i. The following two isolation properties are special cases of this:
- Isolation 1 A T-box without incoming bridge rules is not affected by other T-boxes. (Formally, if Bki = ∅ for all k ̸= i ∈ I, then T |=d i : A ⊑ B =⇒ Ti ⊨ A ⊑ B)
- Isolation 2 A T-box without outgoing bridge rules does not affect the other T-boxes.
Unfortunately, property Isolation 1 does not always hold, because of onto-rules. Indeed, in the presence of onto-rule
1 : A ⊒ -→ 2 : G from T-box T1 to T2, if T2 entails ⊤ ⊑ G, then 1 : A cannot be empty according to DDL semantics, and so, for example, an inconsistency would be generated if T1 entails A ⊑ ⊥. This is despite the fact that the bridge rules are toward T2.
Property Isolation 2 may also not hold. Indeed, if T1 is unsatisfiable, then T2 |=d 2 : X ⊑ Y for every X, Y , even if there are no bridge rules connecting T1 with T2, because there are no satisfying distributed interpretations at all. Note that in a DDL, inconsistency may arise in a connected group of Tboxes even if each T-box is locally consistent; e.g., consider the case in the hypothesis of Lemma 2.1, when Tj |= ⊤ ⊑ G and Tj |= H ⊑⊥.
This is a significant problem, because a localized inconsistency spreads and contaminates reasoning in all other local ontologies, even in the absence of connections to them, because there will be no satisfying distributed interpretation, and hence every statement about them is true, as usual in logic. This problem plagues all modular and distributed representation systems.
In the following section we propose an extension of the initial semantics in order to fix this problem.
3 Inconsistency in DDL
There are a number of possible approaches to handle the problem of inconsistency propagation.
- Define d-entailment in a 2-step manner, first eliminating local T-boxes that are inconsistent, and then using the standard definition. The problem with this approach is that it is non-monotonic, and it does not deal with cases where the inconsistency arises due to several connected local sources.
- Use some variant of a multi-modal epistemic semantics, which allows for models of even inconsistent knowledge in the case when the set of accessible worlds is empty. Such an approach was used in [6] for Distributed First Order Logics, but its computational complexity/decidability aspects are quite worrisome, and the precise impact of such non-standard semantics on logical consequences is hard to explain in an intuitive manner to users.
- Introduce some special interpretation, called a "hole" in [2], whose role is to interpret even inconsistent local T-boxes. We pursue this latter option.
Definition 3.1 A hole for a T-box T is an interpretation I ϵ = 〈∅, ·ϵ 〉, where the domain is empty.
Of course, the important property of holes is that I ϵ |= X ⊑ Y for every X and Y , since both sides are interpreted as the empty set. 5 We will however continue to refer to T-boxes as "inconsistent/unsatisfiable" in case there are no interpretations other than I ϵ which satisfy all the axioms in it.
Let us extend the notion of d-entailment |=d, obtaining the |=ϵ relation, by also allowing holes as interpretations for local T-boxes. Note that now even if some local T-box Ti is inconsistent, we still have an interpretation for the whole DTBox: one that uses I ϵ to satisfy Ti.
Properties of the semantics with holes First, the new semantics does the intended job:
Theorem 3.1 The earlier-stated "directionality desideratum" holds for |=ϵ.
5 We are indebted to XXX for pointing out an earlier error, and to YYY referee for suggesting the empty domain.
Non-standard semantics (such as multivalued logics) can however distort the meaning of the original semantics in unpredictable ways. The following results should be reassuring in this respect.
For any T and any i ∈ I, let T(ϵi) (the distributed T-box with the i-th local T-box viewed as inconsistent) be obtained by removing Ti, Bij and Bji form T, and by extending each Tj with the set of axioms {G ⊑ ⊥|i : A ⊒ -→ j : G ∈ Bij}. For any finite set J = {i1, . . . , in}, such that J ⊂ I, let T(ϵJ) be T(ϵi1 ) . . . (ϵin ). (If J is empty T(ϵJ) = T.) The following then precisely characterizes the relationship of |=d and |=ϵ:
Proposition 3.1 T |=ϵ i : X ⊑ Y if and only if for every subset J ⊆ I not containing i, T(ϵJ) |=d i : X ⊑ Y .
Moreover, in acyclic cases the relationship is even clearer: Proposition 3.2 Let T = 〈T1, T2, B12〉 be a DTBox. Then
- (i) if T1 is consistent, then for j ∈ {1, 2}, T |=ϵ j : X ⊑ Y if and only if T |=d j : X ⊑ Y .
Application to Other Frameworks As noted earlier, the problem of local inconsistency polluting the inferences of all the modules in a modular representation is quite general. We examine how the approach presented here can be applied to two previously proposed schemes.
[9] proposes an elegant notion of modular ontology which starts from the semantic framework of DDLs, but restricts bridge rules to "identities" defining new local names j : N using concepts i : C from T-box i, modulo a semantic domain correspondence exactly like rij for DDLs. 6 This can be modeled by replacing every definition i : C ≡ j : N by the composed bridge rule i : C ≡ -→ j : N, Therefore the semantics involving holes introduced in the previous section can be applied to this approach, in order to localize inconsistencies in modules.
The Somewhere Peer Data Management System [8] consists of a collection of peers which maintain local ontologies, including repositories of "extensional data". Peers are acquainted with neighbors, whose concepts they can use, and query processing involves intensional distributed reasoning for query rewriting. Since this reasoning is (semantically) based on a single global interpretation, it is subject to the above mentioned difficulties due to inconsistency. In fact, for completeness, a global consistency check, involving even unconnected peers, would be required. We would suggest adopting a distributed semantics with holes, such as that of DDL. In particular, current peer links in Somewhere can be reduced to subsumption expressions like 1 : C ⊓ 3 : D ⊑ 2 : E. A DDL can be constructed from this by replacing occurrences of i : C in peer j by new, local symbol Ci, and adding bridge rules i : C ≡ -→ j : Ci and i : ¬C ≡ -→ j : ¬Ci. Our semantics then provides for directionality and locality, and the next section provides a distributed satisfiability testing algorithm for the semantics with holes.
6 Although [9] originally defines imported names using conjunctive queries over concepts and roles in T-box j, it then says that these can be "rolled up" into descriptions. Although this may in fact not always be doable, we will deal here with exactly those definitions for which this roll-up holds.
Finally, the C-OWL [3] proposal for contextualized ontologies, uses a similar model theory as DDL. The only difference concerns the definition of hole, which, in C-OWL was defined on a non empty set. Those notion of hole supports directionality in all the cases except the case of presence of i : ⊥ ⊒ -→ j : ⊥ rule, which allows to propagate back inconsistency. The particular version of "holes" given in this paper gives to C-OWL the directionality property, in addition to the localized inconsistency it already had.
4 Fixed-point semantics of bridge rules
As we saw earlier, combinations of bridge rules allow the propagation of subsumptions across T-boxes. To better understand how this propagation happens, we will associate with a set Bij of bridge rules an operator of the same name, which extends the j-th T-box with a set of subsumption axioms that are the transformation via bridge rules of subsumptions in the i-th T-box.
Before proceeding further, we need to introduce the concept of disjoint union for interpretations. To begin with, we define as usual the disjoint union of two, possibly overlapping sets S and T as S ⊎ T = (S × {#}) ∪ (T × {@}), where the values are distinguished by tupling with two discriminant symbols -# and @, in this case. This is generalized to the disjoint union ⊎i∈K Si of a collection of sets {Si}i∈K indexed with (possibly infinite) K, by using the indeces i as the discriminants.
Definition 4.1 Given two interpretations I = 〈ΔI, ·I 〉 and J = 〈ΔJ , ·J 〉 of the same language L, the disjoint union of I and J , denoted by I ⊎ J , is 〈ΔI⊎J , ·I⊎J 〉, where:
- ΔI⊎J =ΔI ×{#} ∪ΔJ ×{@}
- for concept A, (A)I⊎J = AI ×{#} ∪AJ ×{@}
- for role R, RI⊎J = {〈(x,#), (y,#)〉 | 〈x, y〉 ∈ RI } ∪ {〈(w, @), (z, @)〉 | 〈w, z〉 ∈ RJ }
Disjoint union for interpretations ⊎k∈K Ik can similarly be generalized to the case of a sets. Intuitively the interpretation I ⊎J is interpretation that is composed of two unrelated subparts one is isomorphic to I and the other to J .
Definition 4.2 A description logic family DL has the disjoint union satisfiability property if E I ′ = ⊎k∈K EIk holds for all concepts and roles E over DL, and for all interpretations I ′ = ⊎k∈K Ik.
Lemma 4.1 SHIQ, and its sub-languages, have the distributed union satisfiability property.
On the other hand, languages that support nominals (such as OWL), or A-boxes do not have this property.
The bridge operator The bridge operator essentially applies generalized subsumption propagation Lemma 2.2, to find new subsumptions:
Definition 4.3 Given a set of bridge rules B12 from DL1 to DL2, the bridge operator B12(·), taking as input a T-box in DL1 and producing a T-box in DL2, is defined as follows:
(Notationally, ⊔0k=1 Dk denotes ⊥.)
It is remarkable that these are essentially all the inferences that one can get, if we use the semantics with holes:
Theorem 4.1 Let T12 = 〈T1, T2,B12〉 be a distributed Tbox. If DL1 and DL2 have the distributed union satisfiability property then:
For any family B = {Bij}i,j∈I of bridge rules, we can combine these into a new operator B on a family of T-boxes as follows:
If I is finite and each Bij is finite, then there is a positive integer b such that for every family of T-boxes T, B b (T) = Bb+1 (T). Let us then define B∗ (T) as Bb (T), where b is the first positive integer such that Bb (T) = Bb+1 (T). Furthermore let Bb+1 (T)i, be the i-th T-box in Bb+1 (T).
Theorem 4.2 For every T = 〈T,B〉, T |=ϵ j : X ⊑ Y if and only if the j-th T-box of B∗ (T) entails X ⊑ Y .
Applications to Caching A number of researchers have considered the idea of caching locally the necessary information from the imported ontology Tother , since this is assumed to be both more efficient (there is no need to interrupt local reasoning, while waiting for answers from the other ontology), and more prespicuous from the point of view of the local user: in order to understand an imported concept F, it is not necessary to understand all of Tother , only the locally cached part, which is presumed to be much smaller. (This idea is also known as "subsetting", and there is considerable research on this topic in the ontology community .)
Theorem 4.2 above indicates that it is possible to finitely pre-compile in a sound and complete manner the subsumption information imported into a local ontology Tj by the bridge rules in a DTBox T: compute and store it.
In a similar vein, [9] takes the set of imported concept definitions {Nk ≡ other : Dk | k = 1, . . . , n}, and then computes and caches the subsumption hierarchy of the {Nk}. Since we have explained in Section 3 that the module mechanism in [9] can be represented as a DDL, Lemma 2.2 indicates that if the language contains at least ALC, and if if it is possible to ask subsumption queries about complex concepts composed using the imported definitions, then it is not sufficient to cache only subsumptions of the form Dk1 ⊑ Dk2, since there may be additional subsumptions entailed, involving disjunctions. On the other hand, by Theorem 4.2 it is sufficient to cache all subsumptions of the form Nk ⊑ Nk1 ⊔ . . . ⊔ Nkm , whose definitions satisfy the condition 7 Tother |= Dk ⊑ Dk1 ⊔ . . . ⊔Dkm .
5 A distributed tableaux algorithm for DDL
In this section we describe a tableaux-based decision procedure for T |=ϵ i : X ⊑ Y , for DTBoxes whose bridge graph GT is acyclic. The cyclic case is left for future work, pending the identification of a loop blocking strategy that preserves the independence of the local proofs.
To simplify the description, we suppose that local ontologies are expressed in (a subset of) the SHIQ language - one of the most widely known DLs. Also, we will assume that the consequences of bridge rules are atomic names. (This condition can easily be achieved by introducing, through definitions, names for the consequent concepts.). We need the usual notion of axiom internalization, as in [7]: given a T-box Ti, the concept CTi is defined as CTi = bigsqcapE⊑D∈Ti ¬E ⊔ D; also, the role hierarchy RTi contains the role axioms of Ti, plus additional axioms P ⊑ U, for each role P of Ti, with U some fresh role.
The algorithm for testing j-satisfiability of a concept expression X (i.e., checking T ̸|=ϵ j : X ⊑ ⊥) builds, as usual, a finite representation of a distributed interpretation I, by running local autonomous SHIQ tableaux procedures to find each local interpretation Ii of I.
Definition 5.1 For each j ∈ I, the function DTabj takes as input a concept X and tries to build a representation of Ij with X Ij ̸= ∅ (called a completion tree [7]) for the concept X ⊓ CTj ⊓ ∀U.CTj , using the SHIQ expansion rules, w.r.t. the role hierarchy RTj , plus the following additional "bridge" expansion rules
Unsat-Bij -rule
New-Bij -rule
if 1. G ∈ L(x), i : A ⊒ -→ j : G ∈ Bij, and 2. B⊆ {B|i : B ⊑ -→ j : H ∈ Bij}, and 3. for no B′ ⊆B is IsSati(A⊓¬ ⊔ B′ ) = False, and 4. for no B′ ⊇B is IsSati(A⊓¬ ⊔ B′ ) = True , then if DTabi(A⊓¬ ⊔ B) = Satisfiable then IsSati(A ⊓ ¬ ⊔ B) = True else IsSati(A ⊓ ¬ ⊔ B) = False
The idea, inspired by bridge operator Bij(·), is that whenever DTabj encounters a node x that contains a label G which is a consequence of an onto-bridge rule, then if G ⊑ ⊔H is entailed by the bridge rules, the label ⊔ H, is added to x. To determine if G ⊑ ⊔H is entailed by bridge rules Bij , DTabj invokes DTabi on the satisfiability of the concept A⊓¬(⊔B). DTabi will build (independently from DTabj) an interpretation Ii, as illustrated in Figure 2. To avoid redundant calls, DTabj caches the calls to DTabi in a data structure IsSati, which caches the subsumption propagations that have been computed so far. Specifically, for every C, IsSati(C) will be set to True/False whenever T ̸|=ϵ i : C ⊑ ⊥ is determined.
7 There is no need to iterate if we assume that imported names cannot be used in additional axioms of the local ontology - only for labeling information on the semantic web, for example.

Theorem 5.1 (Termination) For any acyclic DTBox T and for any SHIQ concept X, DTabj(X) terminates.
Theorem 5.2 (Soundness and completeness) j :X is satisfiable in T if and only if DTabj(X) can generate a complete and clash-free completion tree.
Note that the construction of the distributed interpretation can be parallelized, as each local tableau procedure can run independently from the others, without checking for blocking conditions with nodes generated by the other local tableaux. The distributed tableaux proposed above has been implemented in a peer-to-peer setting, and is available for download. Some preliminary experiments have been done to see how distributed algorithm performs w.r.t. a global tableaux algorithm based on the encoding described in [2].
Example 5.1 To clarify how DTabj works, Table 1 reports the trace of DTabshoe invokation for satisfiability test of SHOE : BookArticle ⊓ ¬Publication from Example 2.1. Notice that at step (3) DTabshoe applies the new-Bij-rule and invokes DTabswrc, using the bridge rules (1) and (3).
| Step | tree | labeling and IsSat | rule |
|---|---|---|---|
| (1) | x | L(x) = {BookArticle ⊓¬Publication} IsSat = {} | initial node |
| (2) | x | L(x) = {BookArticle, ¬Publication} IsSat = {} | ⊓-rule |
| (3∗ ) | x | L(x) = {BookArticle, ¬Publication} IsSat = {InBook ⊓¬Publication = False} | new-Bij-rule |
| (4) | x | L(x) = { BookArticle, ¬Publication Publication } IsSat = {InBook ⊓¬Publication = False} | Unsat-Bij-rule |
| (5) | x | L(x) = {Clash} IsSat = {InBook ⊓¬Publication = False} | Clash-rule |
| DTabswrc(InBook ⊓ ¬Publication) | |||
|---|---|---|---|
| Step | tree | labeling and IsSat | rule |
| (1) | x | L(x) = {InBook ⊓¬Publication} IsSat = {} . | initial node |
| (n) | x | . . L(x) = {Clash} | SHIQ-rules Clash-rule |
6 Conclusions
This paper has focused on the properties of a KR&R formalism that supports multiple, local knowledge bases connected by semantic mappings. It has proposed a minor modification to the semantics of DDL, which has the salutary effect of localizing inconsistency to the connected component of a distributed reasoner in which it occurs, and of making "knowledge import" be directional. This resolves a problem left open in [2]. Not only is the new semantics easy to explain, but so are its effect on the inferences that continue to be valid. We believe that these features are desirable for all distributed and modular KR&R formalisms, and we provide several such applications [9; 3; 8]. We note here that although the e-connections formalism, and its perspectival restriction [4], can simulate DDLs, their fundamental goal is to obtain hybrid logics, and in such situations there is no motivation for localizing inconsistency.
The same semantics forms the foundation of a fixed-point characterization of the formulas entailed by DDL, which can be used as the basis of a sound and complete cache-based solution to the problem of distributed reasoning. It is also the standard with respect to which one can prove the completeness (as well as, of course, soundness) of a distributed tableaux reasoner which we have implemented in a peer-topeer setting.
@inproceedings{ijcai2005p87,
title = {Aspects of Distributed and Modular Ontology Reasoning},
author = {Serafini, Luciano and Borgida, Alexander and Tamilin, Andrei},
booktitle = {Proceedings of the Nineteenth International Joint Conference on
Artificial Intelligence, {IJCAI-05}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Leslie Pack Kaelbling and Alessandro Saffiotti},
pages = {570--574},
year = {2005},
url = {https://ijcai.org/proceedings/2005/87},
}
TY - CPAPER TI - Aspects of Distributed and Modular Ontology Reasoning AU - Serafini, Luciano AU - Borgida, Alexander AU - Tamilin, Andrei T2 - Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05 PB - International Joint Conferences on Artificial Intelligence PY - 2005 SP - 570 EP - 574 UR - https://ijcai.org/proceedings/2005/87 ER -Copied
Machine-readable versions of this paper, for tools and AI agents: