We study possibilities of combining (fragments) of the lightweight description logics FL0 and E L, and identify classes of subsumption problems in a combination of E L and Horn-FL0, which can be checked in PSPACE resp. PTIME. Since FL0 allows universal role restrictions and E L 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 [
A combination of E L and (fragments of) F L0 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, E L and F L0 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 E L and (fragments of) F L0. 2
The central notions in description logics are concepts and roles. In any description logic a set NC of concept names and a set NR of roles is assumed to be given. Complex concepts are defined starting with the concept names in NC , 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 ∈ NC to a set CI ⊆ ΔI and each role name r ∈ NR to a binary relation rI ⊆ Δ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. Terminology. A terminology (TBox, for short) is a finite set of primitive concept definitions of the form C ≡ D, where C is a concept name and D a concept description; and general concept inclusions (GCI) of the form C ⊑ D, where C and D are concept descriptions. A TBox which only contains primitive concept definitions and every concept name is defined at most once is called standard. (As definitions can be expressed as double inclusions, by TBox (or general TBox) we will refer to a TBox consisting of general concept inclusions only.) An interpretation I is a model of a TBox T if it satisfies: – all concept definitions in T , i.e. CI =DI for all definitions C≡D ∈ T ; – all general concept inclusions in T , i.e. CI ⊆DI for every C⊑D ∈ T . Constraint Box. A constraint box (CBox, for short) consists of a TBox T and a set RI of role inclusions of the form r1 ◦ · · · ◦ rn ⊑ s. (We will view CBoxes as unions GCI ∪ RI of general concept inclusions (GCI) and role inclusions (RI).) An interpretation I is a model of the CBox C = GCI ∪RI if it is a model of GCI and satisfies all role inclusions in C, i.e. r1I ◦ . . . ◦rnI ⊆ sI for all r1◦ . . . ◦rn⊆s∈RI. Definition 1. Let C1, C2 be two concept descriptions.
– If T is a TBox, we say that C1 is subsumed by C2 w.r.t. T (denoted C1 ⊑T
C2) iff C1I ⊆ C2I for every model I of T .
– If C is a CBox, then C1 ⊑C C2 iff C1I ⊆ C2I 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. [
We now define the fragments of the description logics F L0 used in this paper
as well as the description logic E L. 3
The Description Logic F L0. F L0 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 [
The Description Logic E L+. The description logic E L [
A ⊑ C A ⊓ B ⊑ C R(i, j) ⊤ ⊑ C A ⊑ ⊥ A(i)
R ⊑ T R ◦ S ⊑ T i ≈ j
A ⊑ ∀R.C Let NC be a set of concept names, and NR, NR′ be disjoint sets of role names. We propose a combination of EL (with roles in NR) and F L0 (with roles in NR′ ). 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 NR and universal restriction only for roles in NR′ ) w.r.t. mixed TBoxes, consisting of an EL part and an F L0 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 NR ∩ NR′ = ∅ 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 = TE ∪ TF which consists of two distinct parts: A set TE of EL GCI (with role names NR), and a set TF of F L0 GCI (with role names NR′ ), each respecting the syntactic restrictions imposed by their logic. In a mixed TBox with acyclic F L0 part, TF is a standard acyclic TBox; in a mixed TBox with standard F L0 part, TF is a standard TBox. We will use the names EL-TBox and F L-TBox to denote the set of EL (resp. Horn-F L0) inclusion axioms in a mixed TBox. 3
We assume known notions such as partially-ordered set, semilattice, lattice and
Boolean algebra. For further information cf. [
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
4 This follows from the fact that ALEU can simulate ALC [
Consider the following classes of algebras: – BAONR, the class of all Boolean algebras with operators (B, ∨, ∧, ¬, 0, 1, {f∃r, f∀r}r∈NR), where • f∃r is a join-hemimorphism, i.e. f∃r(x ∨ y) = f∃r(x) ∨ f∃r(y), f∃r(0) = 0; • f∀r is a meet-hemimorphism, i.e. f∀r(x ∧ y)=f∀r(x) ∧ f∀r(y), f∀r(1)=1; • f∀r(x) = ¬f∃r(¬x) for every x ∈ B. – BAO∃NR the class of boolean algebras with operators
(B, ∨, ∧, ¬, 0, 1, {f∃r}r∈NR), such that f∃r is a join-hemimorphism. – BAO∀NR′ the class of boolean algebras with operators
(B, ∨, ∧, ¬, 0, 1, {f∀r}r∈NR′ ), such that f∀r is a meet-hemimorphism. – SLO∃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∀NR′ the class of all ∧-semilattices with operators
(S, ∧, 0, 1, {f∀r}r∈NR′ ), such that f∀r is a meet-hemimorphism and f∀r(1)=1. – SLO∃∀
NR,NR′ the class of all ∧-semilattices with operators (S, ∧, 0, 1, {f∃r}r∈NR, {f∀r}r∈NR′ ), 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. [
Let RI, RI′ be sets of axioms of the form r⊑s and r1◦r2⊑r, with r, s, r1, r2∈NR (resp. r, s, r1, r2∈NR′). We associate with RI, RI′ the following set of axioms: RIa = {∀x (f∃r2 ◦ f∃r1)(x) ≤ f∃r(x) | r1 ◦ r2 ⊑ r ∈ RI} ∪ {∀x f∃r(x) ≤ f∃s(x) | r ⊑ s ∈ RI} {∀x f∀r(x) ≥ f∀s(x) | r ⊑ s ∈ RI′} ′
RIa = {∀x (f∀r2 ◦ f∀r1)(x) ≥ f∀r(x) | r1 ◦ r2 ⊑ r ∈ RI′} ∪ 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 RIa, and BAO∀NR′ (RI′) (resp. SLO∀NR′ (RI′)) be the subclass of BAO∀NR′ (SLO∀NR′ ) consisting of the algebras satisfying RIa′.
In [
Theorem 1 ([
Theorem 2 Assume that the only concept constructors are intersection and universal restriction. Then for all concept descriptions D1, D2 and every F L0+ CBox C=GCI∪RI, with concept names NC = {C1, . . . , Cn}: D1⊑CD2 iff SLO∀NR′ (RI) |= ∀C1 . . . Cn((VC⊑D∈GCI C≤D) → D1≤D2).
Algebraic Semantics for a Combination of EL and F L0 Theorem 3 Assume the only concept constructors are intersection, existential restriction over roles in NR and universal restriction over roles in NR′ . Let T be a mixed TBox consisting of an E L-TBox TE (with roles in NR) and an F L0TBox TF (with roles in NR′ ), where NR ∩ NR′ = ∅. Then for all concept descriptions D1, D2 in the combined language, with concept names NC = {C1, . . . , Cn}: D1⊑T D2 iff SLO∃N∀R,NR′ |= ∀C1 . . . Cn((VC⊑D∈T C≤D) → D1≤D2). Note: The results can be extended in a natural way to E L+, F L0+ and CBoxes (we will then take the combination of the role inclusions RI, RI′, and the corresponding subclass SLO∃∀
NR,NR′ (RI, RI′) satisfying the axioms RIa ∪ RIa′).
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,NR′ to satisfiability tasks w.r.t. SLO∀NR′ which can in general be solved in EXPTIME. We obtain the following finer grained results: – If TF is a standard TBox, the subsumption tasks are in PSPACE; – If TF is in the Horn-F L0 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. 4
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 T0 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 T1 of T0 with signature Π = (Σ, Pred), where Σ = Σ0 ∪ Σ1 (i.e. the signature is extended by new function symbols). We assume that T1 is obtained from T0 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 T1 = T0 ∪ 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 T0 ⊆ T0 ∪ K is local if satisfiability of a set G of clauses w.r.t. T0 ∪ K only depends on T0 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 T1∪G |=⊥ iff T0∪K[G]∪G |=⊥ where K[G] = {Cσ | C ∈ K, for each subterm f (t) of C, with f ∈ Σ1, f (t)σ ∈ st(K, G), and for each variable x which does not occur below a function symbol in Σ1, σ(x) = x}.
Hierarchical Reasoning. In local theory extensions hierarchical reasoning is
possible. All clauses in K[G] ∪ G have the property that the function symbols in
Σ1 have as arguments only ground terms. Therefore, K[G] ∪ G can be purified
(i.e. the function symbols in Σ1 are separated from the other symbols) by
introducing, in a bottom-up manner, new constants ct for subterms t = f (g1, . . . , gn)
with f ∈ Σ1, gi ground Σ0 ∪ Σc-terms (where Σc is a set of constants which
contains the constants introduced by flattening, resp. purification), together with
corresponding definitions ct ≈ t. The set of clauses thus obtained has the form
K0 ∪G0 ∪D, where D is a set of ground unit clauses of the form f (g1, . . . , gn) ≈ c,
where f ∈ Σ1, c is a constant, g1, . . . , gn are ground terms without function
symbols in Σ1, and K0 and G0 are clauses without function symbols in Σ1.
For the sake of simplicity in what follows we will always first flatten and then
purify K[G] ∪ G. Thus we ensure that D consists of ground unit clauses of the
form f (c1, . . . , cn) ≈ c, where f ∈ Σ1, and c1, . . . , cn, c are constants.
Theorem 4 ([
n N0 = { ^ ci ≈ di → c ≈ d | f (c1, . . . , cn) ≈ c, f (d1, . . . , dn) ≈ d ∈ D}.
i=1
Theorem 5 ([
NR,NR′ (RI, RI′) to proof tasks in SLO∀NR′ (RI′).
The Combination of EL and F L0 We consider the subsumption problem for the combination of EL and F L0 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. 6
We 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 L0 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 TBoxes). In what follows, C[∃R.C′] is a notation indicating that C is a concept description in the combination of EL and F L0 containing a subterm of the form ∃R.C′, R ∈ NR; the notation C[C′′] indicates the concept description obtained by replacing ∃R.C′ with C′′ in C.
Theorem 6 Consider the subsumption problem C[∃R.C′] ⊑T D (where C′ is an EL concept description) w.r.t. a mixed TBox T = TE ∪ TF and the subsumption problem C[C′′] ⊑T ′ D w.r.t. the extension T ′ of T with a new concept name C′′ together with its definition C′′ ≡ ∃R.C′. Then the following are equivalent: (1) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2) → C[∃R.C′] ≤ D (2) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2 ∧ C′′ ≈ ∃R.C′) → C[C′′] ≤ D This also holds for subsumption problems of the form C ⊑ D[∃R.D′]. Theorem 7 Consider the subsumption problem C[∀S.C′] ⊑T D (where C′ is an F L0 concept description) w.r.t. a mixed TBox T = TE ∪TF and the subsumption problem C[C′′] ⊑T ′ D w.r.t. the extension T ′ of T with a new concept name C′′ and a definition for it (C′′ ≡ ∀S.C′). Then the following are equivalent: (1) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2) → C[∀S.C′] ≤ D (2) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2 ∧ C′′ ≈ ∀S.C′) → C[C′′] ≤ D. This also holds for subsumption problems of the form C ⊑ D[∀S.D′]. F L0 with Standard TBoxes. Assume that we consider a combination of EL with the fragment of F L0 with standard TBoxes. Then TF is a standard F L0TBox, hence also TF ∪ {C′′ ≡ ∀S.C′} is a standard TBox.
F L0 with Acyclic TBoxes. Assume that we consider a combination of EL with the fragment of F L0 with acyclic standard TBoxes, i.e. TF is a standard 6 The results can be extended to combinations of EL+ and FL0+ and to subsumption tasks w.r.t. CBoxes. Due to space constraints this extension is not presented here. acyclic TBox {Ai ≡ Ci | i = 1, ..., k}. Assume that C′ does not contain any of the atomic concept names Ai. Since C′′ is a new concept name, the F L0-TBox TF ∪ {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 L0-TBox (which is acyclic only if additional acyclicity assumptions are made on TE ).
Horn-F L0. The restriction imposed on the form of the TBox axioms in HornF L0 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: Theorem 8 Consider the subsumption problem C[∀S.C′] ⊑T D (where C′ is an F L0 concept description) w.r.t. a mixed TBox T = TE ∪TF , and the subsumption problem C[C′′] ⊑T ′ D w.r.t. the extension T ′ of T with a new concept name C′′ and an inclusion of the form (C′′ ⊑ ∀S.C′). Then the following are equivalent: (1) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2) → C[∀S.C′] ≤ D. (2) SLO∃∀
NR,NR′ |= (VC1⊑C2∈TE∪TF C1 ≤ C2 ∧ C′′ ≤ ∀S.C′) → C[C′′] ≤ D. 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 TE 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 M0 be the set of corresponding instances of monotonicity axioms:
M0 = {C1 ≤ C2 → C∃R.C1 ≤ C∃R.C2 | C∃R.Ci = ∃R.Ci ∈ Def}.
Let (TE)0 be the purified form of TE. By Theorem 4, the following are equivalent: (i) SLO∀∃
NR,NR′ |= V(D⊑D′)∈T D ≤ D′ → C1 ≤ C2. (ii) G0 ∧ M0 is unsatisfiable in SLO∀NR′ , where G0 = (TE)0 ∧ TF ∧ (¬(C1 ≤ C2))0. Note that in the presence of the monotonicity axioms, the instances of the congruence axioms in N0 (cf. notation in Theorem 4) are redundant. Theorem 9 Assume that the only concept constructors are intersection and existential restrictions over roles in NR and universal restrictions over roles in NR′. Assume that we have a mixed TBox, consisting of an EL-TBox TE (with roles in a set NR) and an F L0-TBox TF (with roles in a set NR′ ), where NR ∩ NR′ = ∅. Then for all concept descriptions D1, D2 with concept names NC = {C1, . . . , Cn} over this signature, the following hold: (1) If TF is a standard TBox, then: (a) For any subsumption problem purification yields a new mixed TBox T ′ = TE′ ∪ TF′ = TE ∧ Def ∧ TF with a standard F L0 part, and after the elimination of ∃R.C concepts, (TE′ )0 ∪ TF′ is a standard F L0 TBox. (b) Checking whether D1⊑TE∪TF D2 can be done in PSPACE. (2) If TF is a Horn-F L0 TBox and C is an arbitrary concept description in the combined language and D does not contain terms of the form ∃R.D1, where R ∈ NR with subterms of the form ∀S.D2, S ∈ NR′ , then: (a) Purification yields a new mixed TBox with a Horn-F L0 part; after the elimination of ∃R.C concepts, (TE′ )0 ∪ TF′ is a Horn-F L0 TBox. Since (i) C ⊑T D1 ⊓ D2 iff (C ⊑T D1 and C ⊑T D2), and (ii) ∀S commutes with intersections, we can consider, w.l.o.g. only subsumption problems D1 ⊑T ∀S1. . . . ∀Sn.D, n ≥ 0, where D2, D are concept names. (b) Checking whether D1⊑TE∪TF D2 where D2 = ∀S1. . . . ∀Sn.D (where n ≥ 0 and C, D are concept names) can be done in PTIME.
Proof. (1)(a) and (2)(a) are simple consequences of the purification procedure. Consider the purified form of the problem By Theorems 3 and 4, D1⊑TE∪TF D2 iff SLO∀∃
NR,NR′ |= VD⊑D′∈T (D ≤ D′ → D1 ≤ D2 iff G0 ∧ M0 is unsatisfiable in SLO∀NR′ , where G0 = (TE )0 ∧ TF ∧ (¬(C1 ≤ C2))0. In order to test the unsatisfiability of the latter problem we proceed as follows. We first note that, due to the convexity of SLO∀NR′ , if G0 ∧ M0 |=⊥, then there exists a clause C = (c1 ≤ d1 → c ≤ d) ∈ M0 such that G0 |= c1 ≤ d1 and G0∧{c ≤ d}∧M0\{C} |=⊥. By iterating the argument above we can always successively entail sufficiently many premises of monotonicity axioms in order to ensure that there exists a set {C1, . . . , Cn} of clauses in M0 with Cj = (cj1 ≤ dj1 → cj ≤ dj ), such that for all k n k ∈ {0, . . . , n − 1}, G0 ∧ Vj=1(cj ≤ dj ) |= V cik+1 ≤ dk+1 and G0 ∧ Vj=1(cj ≤ i dj ) |=⊥ . Conversely, if the last condition holds, then G0 ∧ M0 |=⊥. This means that in order to test satisfiability of G0 ∧ M0 we need to: (i) test entailment of the premises of M0 from G0; when all premises of some clause are provably true we delete the clause and add its conclusion to G0, and (ii) in the end check n whether G0 ∧ Vj=1(cj ≤ dj ) |=⊥ .
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), T0 = (TE )0 ∪ TF and G0 are in Horn F L0. Therefore, every entailent task in (i) above can be done in PTIME. The task (ii) - for the case that G0 is derived from a subsumption problem of the form C ⊑T ∀S1. . . . ∀Sn.D, where n ≥ 0, and C, D are concept names, can be translated to a satisfiability test in Horn-F L0, so it can be done in PTIME. 2 6
We identified a class of subsumption problems in a combination of E L and HornF L0, which can be checked in PTIME. Since F L0 allows universal role restriction and E L 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).