As more and more applications use ontology to represent semantic information, how to support ontology reuse is becoming more and more important. In the OWL Web Ontology Language, the main primitive for ontology reuse is owl:imports. However, this \copy-andpaste" approach su®ers a number of problems. In this paper, we propose a new import primitive, called semantic import, to facilitate partial ontology reuse. The main contributions of this paper include the semantics of semantic import and reasoning support for TBox reasoning in simple ontology spaces, where an ontology semantically imports vocabulary from another ontology. The semantic import approach provides a brand new way for partial ontology reuse.
Ontologies [
The basic primitive for in the OWL Web ontology language to support reuse
is owl:imports [
sumo:Car v sumo:TransportationDevice Furthermore, we would like to reuse some knowledge which is explicitly stated in or entailed by SUMO:
sumo:Car v 9sumo:capability:(sumo:Transportation)
There are three approaches to reaching the partial ontology reuse through syntactic imports: (i) simply import the whole SUMO ontology into Wppl, and only use some of the axioms, ignoring the others; (ii) only \copy-and-paste" a subset of the SUMO axioms into Wppl; (iii) divide the SUMO ontology into different modules, based on some criteria, and import only the interesting module. All these approaches present some problems, as discussed below.
For (i), when importing the whole ontology and only using some of its axioms the following drawback can raise. Firstly, inconsistency can easily be reached by importing those con°icting axioms from the source ontology. Secondly, there exist partial disagreements in certain axioms; e.g., we might agree that Horses are quadrupeds and mammals, but we do not agree that they are not transportation devices. Thirdly, scalability could become a problem. This means that intention of reusing only a few objects and/or classes in a source ontology would end up importing the whole ontology.
For (ii), in order to import a subset of the axioms, users have to be carefully identify which set of axioms encodes the knowledge he wants to import; otherwise, it will cause information lost. Sometimes, the structure of the ontology is such that this is not possible. For example, given an ontology containing the axioms A v B and B v C, a user wants to import only A v C without committing on B.
Approach (iii) actually is most promising. The main di±culty of (iii) is that
the modularisation of an ontology is far from easily customisable and
generalisable to any ontology. A recent approach in this line is the work by Cuenca-Grau
et al. [
The main contributions of this paper are as follows. Firstly, it proposes
semantic imports, a new mechanism of partial ontology reuse. One distinguished
feature of this new partial reuse mechanism is to allow users to semantically
reuse vocabulary (classes, properties or individuals), while current approaches
allow to reuse axioms. Moreover, semantic imports provide a °exible way to
partially reuse ontologies, by allowing users (in their target ontologies) to agree
or disagree with some subsumption relationships in a distant ontology. More
speci¯cally, in our mechanism all subsumption relations among the semantically
(1)
(2)
(3)
imported named classes in the distant ontology are transferred to the target
ontology. Secondly, the paper address some logical properties and algorithm of a
reasoning problem for a special case in our framework, i.e., semantic imports
in simple ontology spaces, where an ontology semantically imports vocabulary
from another ontology. Based on the notion of local/non-local classes ¯rst
proposed by Cuenca-Grau et al. [
An OWL [
Annotation(imports <http://www.car.org/car#>) Annotation(imports <http://www.xyz.it/vehicle#>) These imports annotations include all the axioms in the two source ontologies into the target ontology.
We extend the notion of ontology by allowing the semantic import of classes,
properties, and individuals from source ontologies. To simplify the presentation,
in this paper we only consider the abstract domain and leave the discussion of
the datatype domain [
De¯nition 1 (Ontology). An ontology is a tuple Wi = hi; Mi; Si; Oii, where 1. i is the identi¯er of the ontology Wi, 2. Mi (called the syntactic import box) is the set of ontology identi¯ers which are syntactically imported by Wi (by the primitive owl:imports), 3. Si (called the semantic import box) is a set of classes, properties and/or individuals symbols which are semantically imported by Wi (by the new primitive owlx:semanticImports). 4. Oi (called the axiom box) contains a set of class, property and individual axioms.
Example 2. Wppl = hppl; Mppl; Sppl; Oppli is an ontology, where Mppl = ; (no syntatic imports), Sppl = fsumo:Car; sumo:Horse; sumo:Transportation,sumo: TransportationDevice ,sumo:capabilityg (Wppl semantically imports the classes sumo:Car, sumo:Horse, sumo:Transportation and sumo:TransportationDevice, the
property sumo:capability). Furthermore, Oppl contains the axioms: sumo:Horse v 9sumo:capability:(sumo:Transportation)(4) 9sumo:capability:(sumo:Transportation) v sumo:TransportationDevice ppl:BelgianDraftHorse v sumo:Horses ppl:Ferrari v sumo:Car (5) (6) (7) They state that horses can be used for transportation (4), that those can be used for transportation are transportation devices (5), that Belgian Draft horses are horses (6), and that Ferrari is a type of car (7), which do not hold in SUMO. Intuitively the fact that Wppl semantically imports sumo:Car means that Wppl \demands" the semantics of sumo:Car from SUMO. In other words, an object of the domain of Wppl cannot be a sumo:Car if it is not a sumo:Car in the domain of the SUMO ontology.
It is worth noting that, in the formal de¯nition, a semantic import box is described as a set of classes, properties, and/or individuals. While in practice, this box can be speci¯ed either by explicitly listing its components, or, in a more intensional way, by, e.g., including all the sub-classes or all the individuals of some given classes. From the theoretical perspective this is clearly irrelevant, while it is very relevant from the usability point of view.
We end this section by clarifying the expected e®ects of semantic imports, which are all satis¯ed by the semantics of semantic imports to be provided in the next section (we assume that 1:A; 1:B; 1:R; 1:o; 1:o2 2 S2): (i) Propagation of class hierarchy : if W1 entails 1:A v1:B, then W2 entails 1:A v1:B. (ii) Propagation of disjoint classes : if W1 entails 1:A v: 1:B, then W2 entails 1:A v: 1:B. (iii) Property Closure: all the 1:R-successors and 1:R-predecessor of 1:o1 are also imported. (iv) Propagation of (in)equality objects : if W1 entails 1:o1 ¼ 1:o2 (1:o1 6= 1:o2), then W2 entails 1:o1 ¼ 1:o2 (1:o1 6= 1:o2). 3
In order to give a formal semantics to semantic imports, we brie°y introduce some basic notions.
De¯nition 2 (Local language). Given an ontology Wi, a local class w.r.t. Wi is a class name in Oi associated with the identi¯er i. Local properties and local individuals are de¯ned analogously. The set of local classes, local properties and local individuals of Wi are denoted by Ci, Ri and Ii. The local language of Wi, i.e., Li, is the union of them.
For example, the local language of Wppl is Lppl, which contains the two classes ppl:BelgianDraftHorse and ppl:Ferrari.
Now we introduce the concept of ontology spaces, in which we consider not only a single ontology but a set of ontologies. As described in the last section, OWL imports annotations do not guarantee the existence of imported ontologies. Similarly, the occurrence of an URIrefs in an axiom does not impose requirement of the existence of an ontological resource associated with such a URIref. For instance, the existence of the axiom car:Car v abc:ExpensiveGood in the ontology Wcar does not guarantee the existence of the ontology Wabc; furthermore, even if Wabc does exist, this axiom does not guarantee that abc:ExpensiveGood is in Labc. When we consider an ontology space, we impose these requirements. De¯nition 3 (Ontology space). Let I be a set of ontology identi¯ers and j 2 I an ontology identi¯er. An ontology space on I is a family of ontologies S = fWigi2I such that (i) for each Wi = hi; Mi; Si; Oii, Mi µ I, (ii) for each j:x occurring in Oi, j:x 2 Si, and (iii) for each j:x 2 Si, j:x appears in Oj, where j 2 I and j 6= i.
Note that, given an ontology space fWigi2I , the above de¯nition requires that: (i) all the imported ontologies of each ontology exist and are in fWigi2I , and (ii) non-local classes, properties and individuals of each ontology in fWigi2I should be introduced by some ontologies in fWigi2I . For example, S = hWsumo; Wppli is an ontology space, where Wppl is de¯ned in Example 2 and Wsumo = hsumo; Msumo, Ssumo; Osumoi with Msumo = ;, Ssumo = ;, (no ontology imports and no semantic import) and with Osumo equal to the set of axioms contained in SUMO.
Based on an ontology space, we introduce the concept of import closure and foreign languages. Intuitively speaking, an import closure of an ontology Wi is the set of axioms considering its syntactic imports, while the foreign language of Wi is the set of names of classes, properties and individuals in an ontology space that are not in its local language.
De¯nition 4 (Import closure). Given an ontology space S = fWigi2I , the import closure of an ontology Wi w.r.t. S, written as OiS, is a set of class, property, and individual axioms recursively de¯ned as follows: 1. Oi µ OiS; 2. if j 2 Mi then OjS µ OiS; 3. nothing else is in OiS.
De¯nition 5 (Foreign language). Given an ontology space S = fWigi2I , the foreign language of Wi w.r.t. S, written as FiS, is the set of classes, properties and individuals of the form j:x (j 6= i) which occur in Si or in OiS.
Intuitively, the semantic for an ontology space is a family of interpretations one for each ontology, such that the axioms of the import closure of each ontology are satis¯ed, and there is an agreement between the interpretations on the semantics of semantically imported symbols, which will be formally de¯ned below. It should be noted that the interpretation domains of the family of interpretations could be disjoint or overlapping with each other.
De¯nition 6 (Interpretation of an ontology space). Let S = fWigi2I be an ontology space on I. An interpretation of S is a family I = fIigi2I , where each Ii, called the local interpretation of Wi, is an interpretation (including hole interpretations) of the local and foreign language of Wi, such that 1. Ii j= OiS; 2. if j:C is a class name in Si, then (j:C)Ii = (j:C)Ij \ ¢Ii ; 3. if j:a is an individual name in Si, then (j:a)Ii = (j:a)Ij ; 4. if j:R is a property name in Si, then forward closure for all d 2 ¢Ii \ ¢Ij , for all d0 2 ¢Ij , hd; d0i 2 (j:R)Ii i® hd; d0i 2 (j:R)Ij ; backward closure for all d 2 ¢Ii \ ¢Ij , for all d0 2 ¢Ij , hd0; di 2 (j:R)Ii i® hd0; di 2 (j:R)Ij .
Example 3. The interpretation I = fIsumo; Ipplg described in Table 1 is an interpretation of S = hWsumo; Wppli.
symbol
> sumo:Car sumo:Horse sumo:TransportationDevice sumo:Transportation
sumo:capability ppl:BelgianDraftHorse
ppl:Ferrari sumo:OrganicObject sumo:Artifact : : :
Isumo Ippl fc; f; h; k; d; t; : : : g fc; f; h; v; d; tg fc; f g fc; f g fh; kg fhg fc; f; dg fc; f; h; vg
ftg ftg ½hc; ti; hh; ti¾ ½hc; ti; hh; ti¾ hf; ti; hd; ti hf; ti; hd; ti undef fhg undef ff g fh; kg undef fc; f; dg undef
: : : undef
It is worth noting the following points: (i) In a local interpretation of Wppl, only symbols in local and foreign languages are considered. That is why local interpretations of Wppl, such as Ippl above, do not have to provide an interpretation mapping for symbols (such as sumo:OrganicObject and sumo:Artifact) that are not in the local or foreign languages of Wppl. (ii) Due to the backward closure, hd; ti is in (sumo:capability)Ippl .
De¯nition 7 (Logical consequence). Let S = fWigi2I be an ontology space on I. An OWL DL axiom ® is a logical consequence of S in Wj, written S j=j ®, i®, for every interpretation I = fIjgj2I of S, Ij j= ®. 4
Note that the framework proposed in the previous sections is very general; e.g., there can be an arbitrary (¯nite) number of ontologies in an ontology space and any ontology involved can semantically vocabulary from any other ontologies in the ontology space. As a ¯rst step, in the rest of this paper we only consider a special kind of ontology spaces, called simple ontology spaces. Informally speaking, a simple ontology space consists of a pair of ontologies Wi and Wj, where there is no syntactic imports, and Wj semantically imports some vocabulary from Wi, and Wi does not (semantically) import anything.
De¯nition 8. A simple ontology space is of the form S = hWj; Wii, where Mj = Mi = ; (no syntactic imports) and Sj = ;.
What is the e®ect on the logical consequence of semantic import? And how such e®ect can be computed? In what follows, we will answer these questions by characterizing the e®ect of class constructors on transferring knowledge (in the form of class subsumptions) from a distant ontology to a target ontology. Let us illustrate our characterization by revisiting our example about hWsumo; Wppli. Example 4. In our example, the subsumption (3) is propagated from Wsumo to Wppl. Intuitively this is because Wppl semantically agrees with Wsumo on the meanings of all the terms of this subsumption. Instead, the subsumption sumo:Horses v :sumo:TransportationDevice which holds in Wsumo, does not hold in Wppl because Wppl disagrees with Wsumo on the meaning of sumo:TransportationDevice (see the di®erent interpretations in table 1).
Generalizing the previous example, one might falsely infer that, if the ontology Wi semantically imports a set of symbols Si from the ontology Wj, then all the class subsumptions in the language of Sj that hold in Wj are propagated to Wi. This is true with an exception, due to the e®ect of coverage axioms. Let us explain this point with an example.
Example 5 (Closure Axioms are not Propagated). 2 Suppose that the ontology Wxyz contains the axiom :xyz:Fast v xyz:Slow: (8) Such an axioms partitions the domain of Wxyz into two sets, the fast objects and the slow objects. Even if Wppl semantically imports all vocabulary from Wxyz, axiom (8) is not propagated form Wxyz to Wppl. The reason is that the domain of ontology Wppl might contain objects which are not in the domain of Wxyz, and these objects could be neither fast nor slow. 4.1
Characterizing Logical Consequence in Simple Ontology Spaces In Sections 2 and 3, we mainly considered subsumption relations among semantically imported named classes. Now we introduce related class descriptions. De¯nition 9 (Semantically imported classes descriptions). The semantically imported class descriptions, or simply semantically imported classes, of an ontology Wi are SHOIN -class descriptions that can be constructed from classes, properties and individuals contained in Si. We say that Wi semantically imports a description X from Wj if X is constructed by the local language of Wj. 2 B. Cuenca-Grau presented this example at the DL-2006 workshop. De¯nition 10. Given S an semantic import box, we say that a class description C (property description R) is S-related if all the vocabulary in C (R, respectively) are in S.
For example, given the semantic box Sppl = fsumo:Car; sumo:Horse; sumo:Transportation, sumo:TransportationDevice (see Example 2), sumo:Car, sumo:capability, and 9(sumo:capability).(sumo:Transportation) are Sppl-related.
On the base of the intuition given in the example presented at the beginning
of Section 4, in the following we will provide a precise class characterization on
which subsumptions propagate as a consequence of semantic imports in simple
ontology spaces. Formally speaking, we accomplish this by using the notion of
local/non-local classes ¯rst proposed by Cuenca-Grau et al. [
De¯nition 11 (Polarity). The polarity of a semantically imported SHOIN classes is de¯ned as follows (let A and B be classes, a an individual and R an object property): any atomic class is positive, ? is positive, > is negative, fag is positive, A u B is positive if either A or B are positive, A t B is positive if both A and B are positive, :A is positive i® A is negative, 9R:A is positive, 8R:A is negative, (¸ 0)R is negative, (¸ n)R with n ¸ 1 is positive, (· n)R is negative, every class which is not positive is negative.
Property 1. For every positive concept semantically imported from Wj, CIi = CIj \ ¢Ii . For every negative concept semantically imported from Wj, CIi = (CIj \ ¢Ii ) [ ¢Ii¡Ij (where ¢Ii¡Ij is a shortcut of ¢Ii n ¢Ij ).
The Property 1 is the same as the property of local/non-local classes
presented in the proof of Theorem 1 of [
Based on the notion of positive/negative (i.e. local/non-local) classes and the
above property, the following De¯nition 12, Theorem 1 and 2 and can be seen
as counterparts (under the semantics of semantic imports) of the Theorem 2 of
[
Intuitively, the subsumption transfer from Wi to Wj is the set of all the possible subsumptions in Wi that are semantically propagated in Wj. The following theorem shows that the subsumption transfer de¯ned above can be used for a sound and complete characterization of logical consequences in simple ontology spaces.
Theorem 1 (Soundness). Let S = hWj; Wii be a simple ontology space. If X and Y are Si-related class descriptions, then
Wi [ Sji(Wj) j= X v Y =)
S j=i X v Y: Theorem 2 (Completeness). Let S = hWj; Wii be a simple ontology space. If X and Y are Si-related class descriptions, then
Wi [ Sji(Wj) j= X v Y (=
S j=i X v Y: Proof. Suppose that Oi [ Sji(Wj) 6j= X v Y and let us build a model for S such that S 6j=i X v Y . If Oi [ Sji(Wj) 6j= X v Y then let Ii be a model of Oi [ Sji(Wj) such that XIi 6µ Y Ii .
Suppose that Oj is unsatis¯able, then for all concept C 2 Si, Oj j= C v ?; for all nominal fxg 2 Sii, Oj j= fxg v ?; for all role R 2 Si, Oj j= > v 8R:?. In all the cases we have that the corresponding subsumptions belongs to Sji(Oj). The fact that Ii j= Sji(Oj), implies that Si does not contains nominals (otherwise Ii j= fxg v ?, which is not possible), and for all C and R in Si, they are interpreted by Ii in the empty set. This implies that the interpretation hIj; Iii with Ij being a hole interpretation, satis¯es S.
Now let us consider the case were Oj is consistent. Let ¢¤ µ ¢Ii be the set 8 > > < > > :
¯¯ x 2 BIi for some B 2 Si or x 2 ¢Ii ¯¯¯¯ hxx=;yfia2gIRi Ifiorfosrosmoemae 2y aSnidorR 2 Si or ¯¯ hy; xi 2 RIi for some y and R 2 Si 9 > > = > > ; If ¢¤ = ; then, the interpretation hIj; Iii where Ii is the hole interpretation is a model of S which does not satisfy X v Y . Suppose, therefore that ¢¤ contains at least an element x0.
Let Wi¤ be obtained by extending the semantic import Si of Wi with the set of constants in ¢¤ (we can suppose with no loss of generality that ¢¤ is disjoint from the language of Wi), and with a new role R0. a new nominal fx0g. Let Ii¤ be the extension of Ii such that xIi¤ = x for all x 2 ¢¤ and xIi¤ be any value in 0 ¢¤. Clearly Ii¤ is an interpretation of Wi¤ that satis¯es Oi¤ = Oi.
Let Wj¤ be obtained by extending Oj of Wj, with the following set of axioms. We denote the resulting set with Oj¤. 1. fx0g v 9R0 fxg for all x 2 ¢¤ 2. fxg v : fyg for every x 6= y 2 ¢¤. 3. fxg v B, if B 2 Si and x 2 BIi ; 4. fxg v 9R: fyg, if R 2 Si and hx; yi 2 RIi .
Consider the ontology space S¤ = hWj¤; Wi¤i, If Oj¤ is consistent, then there is an interpretation Ij¤ for Oj¤ in which xIj¤ = x. Let Ij be the restriction of Ij¤ on the language of Wi, then by construction hIj; Iii is an interpretation for S. 0
If Oj¤ is inconsistent, then, since Oj is consistent, there is a ¯nite subset Oj of the axioms 1{4 added to Oj that make it inconsistent. Let C¤ be the concept t XvY 2Oj0
X u :Y:
Oj j= fx0g v 9R0C¤: We have that Oj [ C¤ v ? is inconsistent. This implies that Notice that both fx0g and 9R0C¤ are positive classes, which implies that fx0g v 9R0C¤ belongs to Sij(Wi) which generates a contradiction. 4.2
Distributed Tableaux for Simple Ontology Spaces
In this section, we consider ontologies represented as ALC [
Tableaux algorithms (¯rst by [
Formally, a completion tree is a tuple T = hx; N; E; Li, where x is the root of T , N and E are the sets of nodes and edges, respectively, of T , and L a function that maps each node y (each edge hy; zi) in T to its label L(y) (L(hy; zi), respectively). Let T be a completion tree, S a semantic import box. We say that a completion tree T is S-related if there exist some S-related class or property descriptions in the labels of all edges and all non-leaf nodes of T . In what follows, we de¯ne the main operation on completion trees we need in our algorithm. De¯nition 13 (Projection of Completion Tree). Let S be a semantic import box and T an S-related clash-free completion tree with root x0. The projection of T w.r.t. S, denoted as ¼S (T ), is a completion tree which 4 Here we assume E is in negation normal form; i.e., negation is only applied to class names. 1. has the same root x0, 2. contains the exact set of nodes and edges as T , and 3. for each label L(x0) (L(hx0; y0i)) of a node x (an edge hx0; y0i, respectively) is the subset of the label L(x) (L(hx; yi), respectively) of the corresponding node x (edge hx; yi, respectively). If all the S-related class descriptions in L(x) is negative, L(x0) = ;; otherwise, L(x0) contains all the S-related class descriptions in L(x) . L(hx0; y0i) contains all the S-related property descriptions in L(hx; yi).
According to Theorem 1 and 2, we do not project any S-related class descriptions in L(x) to L(x0) if all the S-related class descriptions in L(x) are negative.
For a simple ontology space S = hWj; Wii, the procedure S-Tab(i, E) veri¯es the satis¯ability of an ALC class description E in ontology Wi. The procedure Tab(Ox; T ) is a (local) tableaux algorithm to expand T w.r.t. a local ontology Ox. Tab(Ox; T ) has two distinguished features that we need: (i) it takes not only a single node but an arbitrary initial completion tree (see line 8 in Algorithm 1), (ii) the algorithm can cache reasoning states (see line 11 in Algorithm 1). Algorithm 1: S-Tab(i, E) 1: let T :=Tab(Oi; hx0; fx0g; ;; fL(x0) = fEggi) //local expansion w.r.t. Oi 2: repeat 3: if T has a clash then 4: return unsatis¯able 5: end if 6: let T1; : : : ; Tn be the maximal Si-related sub-trees of T with roots x1; :::; xn, repectively 7: T10 := ¼Si (T1); : : : ; Tn0 := ¼Si (Tn) //sub-trees projection 8: T10 := Tab(Oj; T10); : : : ; Tn0 := Tab(Oj; Tn0) //local expansion w.r.t. Oj 9: if any of T10; : : : ; Tn0 has a clash then 10: if T is backtrackable then 11: T :=Tab(Oi; T ; backtrack) //backtrack and expand 12: else 13: return unsatis¯able 14: end if 15: else 16: return satis¯able 17: end if 18: until false
The algorithm needs some explanation and clari¯cation. T is initialised with a root x0 with L(x0) = fEg, and is expanded by local completion rules w.r.t. Oi (line 1). As T might not be Si-related, maximal Si-related sub-trees then should be projected and expanded by local completion rules w.r.t. Oj (lines 6-8). If any of the projected sub-tree has a clash, T needs to be backtracked, expanded and start the checking all over again. In what follows, let us use a simple example to illustrate its main idea of the algorithm.
Example 6. Given the following ontology space S = hWj; Wii, where Wj and Wi are de¯ned as follows: Wj = hj; Mj = ;; Sj = ;; Oj = fj:A v 8j:R:(j:C); j:C v j:Bgi and Wi = hi; Mi = ;; Si = fj:A; j:B; j:Rg; Oi = ;i. We want to check the satis¯ability of the following class j:A u 9j:R:(:j:B) in Wi w.r.t. S.
We use Tab(Oi; hx0; fx0g; ;; fL(x0) = fj:A u 9j:R:(:j:B)ggi) to build a clash-free completed completion tree T . It is obvious that T is Si-related, so there is only one maximal Si-related sub-tree of T , which is itself. Therefore, T 0 consists of two connected nodes x00 and x0 , where x00 is labelled with L(x00) = 1 fj:A u 9j:R:(:j:B); j:A; 9j:R:(:j:B)g, x01 is labelled with L(x01) = f:j:Bg and the edge hx00; x01i is labelled with L(hx00; x01i) = j:R. Then we expand T 0 with mega-constraints:5 we ¯rst expand L(x00) as fj:Au9j:R:(:j:B); j:A; 9j:R:(:j:B), :j:A t 81:R:(j:C); :j:C t j:Bg; for the disjunction :j:A t 8j:R:(j:C) in L(x00), we have to choose 8j:R:(j:C) since j:A 2 L(x00); then we expand L(x01) and add C in it, so L(x01) = f:j:B; :j:A t 8j:R:(j:C); :j:C t j:B; Cg; obviously there is a clash in L(x01) because :j:C t j:B; j:C and :j:B are in L(x01). Hence, T 0 and T are not complete and j:A u 9j:R:(:j:B) is unsatis¯able in Wi w.r.t. S.
To prove the algorithm correct, we need to show that: (1) The algorithm always terminates. (2) The algorithm returns unsatis¯able i® S 6j=i E. (3) The algorithm returns satis¯able i® S j=i E.
Due to limited space, we only provide a brief discussion. For (1), observe that Algorithm 1 does not change T at all and simply invokes backtrack when there exists an external clash. Algorithm 1 terminates because Tab(O; E) terminates. For (2), observe that S 6j=i E either because Oi 6j= E (this would be detected by lines 1-3) or there exists some X v Y 2 Sji s.t. :X t Y is disjoint with a Si-related sub-class of E (this would be detected by lines 7-9). For (3), it can be shown that we can construct an interpretation of E whenever we have a complete T , and vice versa. 5
Ontology reuse has been an important topic [
The semantic for ontology import is an evolution of the semantics C-OWL
language [
Our approach is also related to existing work on reasoning with distributed
Description Logics [
´
Ontology modularisation [
How to support ontology reuse is becoming more and more important. While the
\copy-and-paste" approach su®ers a number of problems, this paper proposes a
new import primitive, called semantic import, to facilitate partial ontology reuse.
In this paper, we have identi¯ed four semantic requirements for semantic import:
propagation of class hierarchy, disjoint classes, property closure and (in)equality
objects. Secondly, we have investigated the logical properties of semantic imports
in simple ontology spaces. Based on the notion of positive/negative classes ¯rst
proposed by Cuenca-Grau et al. [
An important \side e®ect" of introducing semantic import into ontology languages such as OWL DL is to open a door to support the intended usage of URI references, i.e. identifying resources. In OWL DL, the same individual URIref can be interpreted as di®erent objects in di®erent ontologies, where URI references are not really playing a role on identifying resources. In the presence of semantic import, however, the semantic of ontology space guarantees that an semantically imported individual is interpreted as the same object in multiple ontologies. This suggests that semantic import could play a very fundamental role in Web ontologies under the unique identi¯cation assumption.
As for future work, we would like to further investigate logical consequence of more complex ontology spaces and distributed tableaux algorithms for more expressive ontology languages, such as OWL DL.