We study possibilities of combining (fragments) of the lightweight description logics FL0 and EL, and identify classes of subsumption problems in a combination of EL and Horn-FL0, which can be checked in PSPACE resp. PTIME. Since FL0 allows universal role restrictions and EL allows existential role restrictions, we thus have a framework where subsumption between expressions including both types of role restrictions (but for disjoint sets of roles) can be checked in polynomial space or time.
Description logics [5] are a family of knowledge representation formalisms that can model the terminological knowledge of a given domain; they are, for instance, the logical foundation of the W3C language for the Semantic Web. Their most interesting feature is that they aim at maximizing expressive power while retaining decidability. However, with the size of the ontologies appearing in many applications, decidability alone is not enough because the complexity of the reasoning procedures combined with the size of the ontologies makes reasoning too costly. This consideration triggered the development of lightweight sub-families of description logics. Among them, we mention EL (which only allows the use of conjunction and existential role restrictions) [1] and some of its extensions such as EL + and EL ++ [2,4,3]. These logics can model some very interesting domains sufficiently well to be used widely, for example in the SNOMED ontology [16]. Another lightweight description logic is F L 0 (which only allows the use of conjunction and universal role restrictions). While subsumption without TBoxes in F L 0 is decidable in PTIME, its subsumption problem is in PSPACE for standard terminologies and EXPTIME for general terminologies [8,4]. Since some very interesting forms of knowledge require universal restrictions in order to be modeled adequately, recent research has identified tractable fragments of F L 0 , such as the Horn-F L 0 fragment (defined by syntactic restrictions) for which the subsumption problem is in PTIME [9].
A combination of EL and (fragments of) F L 0 is clearly interesting because of the added expressivity it offers. At the same time, if we allow an unrestricted combination we lose the lower complexity of the components. In this paper we present a way to combine these description logics such that we can verify subsumption between two mixed concept expressions w.r.t. TBoxes efficiently, and identify situations in which this can be done in PSPACE, resp. PTIME.
Structure of the Paper. In Sect. 2 we give general definitions and introduce the description logics ALC, EL and F L 0 and their combination. Sect. 3 presents the algebraic semantics for each logic and their combination. Sect. 4 presents generalities on local theory extensions and hierarchical reasoning (which we use in our approach). These methods are used in Sect. 5, where we present possibilities of hierarchical reasoning in a combination of EL and (fragments of) F L 0 .
The central notions in description logics are concepts and roles. In any description logic a set N C of concept names and a set N R of roles is assumed to be given. Complex concepts are defined starting with the concept names in N C , with the help of a set of concept constructors. The semantics of description logics is defined in terms of interpretations I = (∆ I , • I ), where ∆ I is a non-empty set, and the function • I maps each concept name C ∈ N C to a set C I ⊆ ∆ I and each role name r ∈ N R to a binary relation r I ⊆ ∆ I × ∆ I . Table 1 shows the constructor names used in ALC and their semantics. The extension of • I to concept descriptions is inductively defined using the semantics of the constructors. -If T is a TBox, we say that C 1 is subsumed by
for every model I of C. The simplest propositionally closed description logic is ALC which allows for conjunction, disjunction, negation and existential and universal role restrictions. For description logics that allow full negation, subsumption tests w.r.t. TBoxes or CBoxes are reducible to satisfiability testing for concepts (i.e. checking if there exists a model of the TBox resp. CBox for which the interpretation of the concept is non-empty). It is well-known that for ALC subsumption checking (w.r.t. TBoxes and CBoxes) is in EXPTIME (cf. [5]). For lightweight description logics which do not allow negation, things are different: The main reasoning task is subsumption testing, which is the problem we consider in this paper.
We now define the fragments of the description logics F L 0 used in this paper as well as the description logic EL. 3The Description Logic F L 0 . F L 0 is a lightweight description logic that only allows as concept constructors conjunction, universal role restrictions, and top concept. The subsumption problem w.r.t. general TBoxes is known to be in EXPTIME [4]. Fragments of F L 0 resp. specific classes of subsumption for which the complexity is known to be lower include:
-Subsumption w.r.t. standard TBoxes has PSPACE complexity [8].
-Subsumption w.r.t. acyclic TBoxes is co-NP complete (where an acyclic TBox is a standard TBox that does not contain concept definitions
). -Horn-F L + 0 [9] is a variant of F L 0 that both extends and restricts its expressivity in such a way that the subsumption problem remains in PTIME. It restricts F L 0 axioms to the form shown in Table 2. The form of the axioms is limited in such a way that they can be rewritten into 3-variable function-free Horn-logic. It follows from this correspondence that verifying consistency of a Horn-F L + 0 knowledge base can be done in polynomial time. A Horn-F L 0 TBox (CBox) consists only of inclusions of the form indicated in the first two lines of Table 2.
The Description Logic EL + . The description logic EL [1] allows as concept constructors only conjunction, existential role restrictions, and the bottom concept. EL + [2, 4, 3] additionally allows for nominals and role composition. For EL + , checking CBox subsumption can be done in PTIME [4,2].
Table 2. Normal form for Horn F L + 0 . A, B, C are names of atomic concepts; R, S, T are (possibly inverse) role names.
Let N C be a set of concept names, and N R , N R ′ be disjoint sets of role names. We propose a combination of EL (with roles in N R ) and F L 0 (with roles in N R ′ ). The problem we study for such combinations is subsumption between concept expressions using constructs from both logics (such that existential restriction is used only for roles in N R and universal restriction only for roles in N R ′ ) w.r.t. mixed TBoxes, consisting of an EL part and an F L 0 part. We allow these TBoxes to share concept names (but the role names used in each type of axioms have to be disjoint). We have to impose the restriction that N R ∩ N R ′ = ∅ in order to be sure that fine-grained complexity results can be obtained for TBox subsumption in such combinations, since the description logic combining these features freely, ALEU , has an EXPTIME complexity for the subsumption problem w.r.t. TBox4 . Definition 2. A mixed TBox is a TBox T = T E ∪ T F which consists of two distinct parts: A set T E of EL GCI (with role names N R ), and a set T F of F L 0 GCI (with role names N R ′ ), each respecting the syntactic restrictions imposed by their logic. In a mixed TBox with acyclic F L 0 part, T F is a standard acyclic TBox; in a mixed TBox with standard F L 0 part, T F is a standard TBox.
We will use the names EL-TBox and F L-TBox to denote the set of EL (resp. Horn-F L 0 ) inclusion axioms in a mixed TBox.
We assume known notions such as partially-ordered set, semilattice, lattice and Boolean algebra. For further information cf. [11]. We define a translation of concept descriptions into terms in a signature naturally associated with the set of constructors. For every role name r, we introduce unary function symbols, f ∃r , f ∀r . The renaming is inductively defined by:
There exists a one-to-one correspondence between interpretations I = (D, • I ) and Boolean algebras of sets (P(D), ∪, ∩, ¬, ∅, D, {f ∃r , f ∀r } r∈NR ), together with valuations v : N C → P(D), where f ∃r , f ∀r are defined, for every U ⊆ D, by:
Consider the following classes of algebras:
-BAO NR , the class of all Boolean algebras with operators (B, ∨, ∧, ¬, 0, 1, {f ∃r , f ∀r } r∈NR ), where
NR the class of boolean algebras with operators (B, ∨, ∧, ¬, 0, 1, {f ∃r } r∈NR ), such that f ∃r is a join-hemimorphism.
NR the class of all ∧-semilattices with operators (S, ∧, 0, 1, {f ∃r } r∈NR ), such that f ∃r is monotone and f ∃r (0) = 0.
-SLO ∀ N R ′ the class of all ∧-semilattices with operators (S, ∧, 0, 1, {f ∀r } r∈N R ′ ), such that f ∀r is a meet-hemimorphism and f ∀r (1)=1.
-SLO ∃∀ NR,N R ′ the class of all ∧-semilattices with operators (S, ∧, 0, 1, {f ∃r } r∈NR , {f ∀r } r∈N R ′ ), such that f ∃r is monotone and f ∃r (0) = 0, and f ∀r is a meet-hemimorphism and f ∀r (1)=1.
It is known that the TBox subsumption problem for ALC can be expressed as a uniform word problem for Boolean algebras with suitable operators (cf. e.g. [6]).
Let RI, RI ′ be sets of axioms of the form r⊑s and r 1 •r 2 ⊑r, with r, s, r 1 , r 2 ∈N R (resp. r, s, r 1 , r 2 ∈N R ′ ). We associate with RI, RI ′ the following set of axioms:
where f • g denotes the composition of the functions f, g. Let BAO ∃ NR (RI) (resp. SLO ∃ NR (RI)) be the subclass of BAO ∃ NR (SLO ∃ NR ) consisting of those algebras which satisfy RI a , and
) consisting of the algebras satisfying RI ′ a . In [13] we studied the link between TBox subsumption in EL and uniform word problems in the corresponding classes of semilattices with monotone functions, and in [14] we studied an extension to EL + . We will present these results here, together with an algebraic semantics for F L 0 .
Theorem 1 ( [13]) Assume that the only concept constructors are intersection and existential restriction. Then for all concept descriptions D 1 , D 2 and every EL + CBox C=GCI∪RI, with concept names N C = {C 1 , . . . , C n }:
We give a similar result for F L + 0 .
Theorem 2 Assume that the only concept constructors are intersection and universal restriction. Then for all concept descriptions D 1 , D 2 and every F L + 0 CBox C=GCI∪RI, with concept names N C = {C 1 , . . . , C n }:
Note: The results can be extended in a natural way to EL + , F L + 0 and CBoxes (we will then take the combination of the role inclusions RI, RI ′ , and the corresponding subclass SLO ∃∀ NR,N R ′ (RI, RI ′ ) satisfying the axioms RI a ∪ RI ′ a ). In what follows we show that we can reduce, in polynomial time and with a polynomial increase in the length of the formulae, the validity tasks w.r.t. SLO ∃∀ NR,N R ′ to satisfiability tasks w.r.t. SLO ∀ N R ′ which can in general be solved in EXPTIME. We obtain the following finer grained results:
-If T F is a standard TBox, the subsumption tasks are in PSPACE; -If T F is in the Horn-F L 0 fragment, the reduction generates formulae whose satisfiability can be checked in PTIME.
For obtaining these results, we use the notion of local theory extensions, which is briefly introduced in what follows.
We here consider theories specified by their sets of axioms, and extensions of theories, in which the signature is extended by new function symbols. Let T 0 be a theory with signature Π 0 = (Σ 0 , Pred), where Σ 0 a set of function symbols, and Pred a set of predicate symbols. We consider extensions T 1 of T 0 with signature Π = (Σ, Pred), where Σ = Σ 0 ∪ Σ 1 (i.e. the signature is extended by new function symbols). We assume that T 1 is obtained from T 0 by adding a set K of (universally quantified) clauses in the signature Π, each of them containing at least a function symbol in Σ 1 and denote this by writing T 1 = T 0 ∪ K.
Locality. Let K be a set of (universally quantified) clauses in the signature Π.
In what follows, when referring to sets G of ground clauses we assume they are in the signature Π c = (Σ ∪ Σ c , Pred) where Σ c is a set of new constants. An extension T 0 ⊆ T 0 ∪ K is local if satisfiability of a set G of clauses w.r.t. T 0 ∪ K only depends on T 0 and those instances K[G] of K in which the terms starting with extension functions are in the set st(K, G) of ground terms which already occur in G or K, i.e. if condition (Loc) is satisfied:
(Loc) For every finite set G of ground clauses (1) T 0 ∪K∪G |=⊥.
(
Theorem 5 ([15]) The extension of any semilattice-ordered theory with monotone functions is local. In particular, the extension
Thus, the method for hierarchical reasoning described in Theorem 4 can be used in this context to reduce the proof tasks in SLO ∃∀ NR,N R ′ to proof tasks in SLO ∀ N R ′ . We describe the approach in the next section. For the sake of simplicity, in what follows we use the notation ∃R.C for f ∃R (C) and ∀S.D for f ∀S (D). 5We consider the subsumption problem for the combination of EL and F L 0 introduced in Section 3.1 and illustrate the way hierarchical reasoning can be used for reasoning in this combination, and for identifying fragments of this combination and subsumption tasks which can be checked in PSPACE/PTIME. 6We first have to purify the expressions for which we want to verify subsumption. Consider for instance the subsumption C ⊑ ∃R.D, where C and D are resp. an F L 0 and an EL concept description. To purify it, we add the axiom D ′ ≡ ∃R.D to the EL-TBox (where D ′ is a new concept name) and rewrite the subsumption as C ⊑ D ′ . We apply this process in an "inside-out" fashion such that the final result is checking subsumption between concept names w.r.t. to an augmented TBox. This procedure does not affect complexity when we use new names for EL concept descriptions (EL allows for equalities and inequalities (1)
This also holds for subsumption problems of the form C ⊑ D[∀S.D ′ ].
F L 0 with Standard TBoxes. Assume that we consider a combination of EL with the fragment of F L 0 with standard TBoxes. Then T F is a standard F L 0 -TBox, hence also T F ∪ {C ′′ ≡ ∀S.C ′ } is a standard TBox.
F L 0 with Acyclic TBoxes. Assume that we consider a combination of EL with the fragment of F L 0 with acyclic standard TBoxes, i.e. T F is a standard acyclic TBox {A i ≡ C i | i = 1, ..., k}. Assume that C ′ does not contain any of the atomic concept names A i . Since C ′′ is a new concept name, the F L 0 -TBox T F ∪ {C ′′ ≡ ∀S.C ′ } is an acyclic TBox. After the elimination of ∃R.C concepts and introduction of new concept names and definitions, the resulting TBox is a standard F L 0 -TBox (which is acyclic only if additional acyclicity assumptions are made on T E ).
Horn-F L 0 . The restriction imposed on the form of the TBox axioms in Horn-F L 0 prevents purification by adding definitions of the form C ′′ ≡ ∀S.C ′ (we cannot allow universal restriction on the left-hand side of an axiom). For the case where we have to purify the left-hand side that causes no problem since if ∀S.C ′ occurs on the left-hand side we only need to add C ′′ ⊑ ∀S.C ′ to the TBox: (1)
However, we cannot replace universal restriction on the right-hand side with a name in general which prevents us to purify arbitrary expressions.
Hierarchical Reasoning. Consider the purified form of the problem. We replace all terms of the form ∃R.C in T E with a new constant, say C ∃R.C . Let Def be the set of all definitions for these new constants, of the form C ∃R.C ≡ ∃R.C. Let M 0 be the set of corresponding instances of monotonicity axioms:
Let (T E ) 0 be the purified form of T E . By Theorem 4, the following are equivalent:
Note that in the presence of the monotonicity axioms, the instances of the congruence axioms in N 0 (cf. notation in Theorem 4) are redundant.
Theorem 9 Assume that the only concept constructors are intersection and existential restrictions over roles in N R and universal restrictions over roles in N R ′ . Assume that we have a mixed TBox, consisting of an EL-TBox T E (with roles in a set N R ) and an F L 0 -TBox T F (with roles in a set N R ′ ), where N R ∩ N R ′ = ∅. Then for all concept descriptions D 1 , D 2 with concept names N C = {C 1 , . . . , C n } over this signature, the following hold: and G 0 ∧ n j=1 (c j ≤ d j ) |=⊥ . Conversely, if the last condition holds, then G 0 ∧ M 0 |=⊥. This means that in order to test satisfiability of G 0 ∧ M 0 we need to: (i) test entailment of the premises of M 0 from G 0 ; when all premises of some clause are provably true we delete the clause and add its conclusion to G 0 , and (ii) in the end check whether G 0 ∧ n j=1 (c j ≤ d j ) |=⊥ . Under the assumptions in (1), every entailment task in (i) and the test in (ii) are in PSPACE. Since space can be reused, the process terminates and is in PSPACE. Under the assumptions in (2), T 0 = (T E ) 0 ∪ T F and G 0 are in Horn F L 0 . Therefore, every entailent task in (i) above can be done in PTIME. The task (ii) -for the case that G 0 is derived from a subsumption problem of the form C ⊑ T ∀S 1 . . . . ∀S n .D, where n ≥ 0, and C, D are concept names, can be translated to a satisfiability test in Horn-F L 0 , so it can be done in PTIME. 2
We identified a class of subsumption problems in a combination of EL and Horn-F L 0 , which can be checked in PTIME. Since F L 0 allows universal role restriction and EL allows existential role restrictions, we thus have a framework where subsumption between expressions including both types of role restrictions (but for disjoint sets of roles) can be checked in polynomial space or time.
Acknowledgments. We thank the referees for their helpful comments. This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS) (see also www.avacs.org).