=Paper=
{{Paper
|id=Vol-477/paper-51
|storemode=property
|title=Exponential Speedup in UL Subsumption Checking relative to general TBoxes for the Constructive Semantics
|pdfUrl=https://ceur-ws.org/Vol-477/paper_8.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/MendlerS09
}}
==Exponential Speedup in UL Subsumption Checking relative to general TBoxes for the Constructive Semantics==
https://ceur-ws.org/Vol-477/paper_8.pdf
Exponential Speedup in U L Subsumption
Checking Relative to General TBoxes for the
Constructive Semantics
Michael Mendler and Stephan Scheele
Informatics Theory Group
University of Bamberg, Germany
{michael.mendler,stephan.scheele}@uni-bamberg.de
Abstract. The complexity of the subsumption problem in description
logics can vary widely with the choice of the syntactic fragment and
the semantic interpretation. In this paper we show that the constructive
semantics of concept descriptions, which includes the classical descriptive
semantics as a special case, offers exponential speed-up in the existential-
disjunctive fragment UL of ALC.
1 Introduction
One of the key reasoning tasks in the application of DL formalisms is the sub-
sumption problem relative to a set of terminological axioms, called a TBox. The
complexity of the decision procedure depends on (i) the language fragment used
for concept descriptions, (ii) the structure of the TBox, i.e., whether it is acyclic,
cyclic or even permits general concept inclusions (GCIs) and finally (iii) the se-
mantic interpretation of the logical operators. E.g., to deal with cyclic TBoxes
the standard extensional (so-called ‘descriptive’) semantics which considers all
fixed points of TBoxes has been made more intensional by restricting to greatest
fixed points and least fixed points [17]. Many result have been obtained in ex-
ploring the options in all these dimensions, discovering complexities all the way
from PTime to NExpTime completeness.
Regarding the full language ALC [5] it has been shown for the descriptive
semantics that subsumption without TBox as well as with acyclic TBoxes is
PSpace complete, while it is ExpTime complete for general TBoxes (see [5]).
Since many applications do not need all the operators of ALC, restricted lan-
guages have been considered for which lower complexity levels can be derived,
even down to PTime. There seem to be two main strands among these so-called
sub-boolean formalisms, the FL-type languages starting from the fragment FL0
consisting of {∀, u} and the EL-type languages which build on the operator set
{∃, u}. Among these, the latter tend to be much better behaved (e.g., more effi-
cient and less sensitive to extensions) than the former. For instance, it is known
that subsumption checking in FL0 is PTime for empty TBoxes [14], coNP
complete for acyclic TBoxes [17], while for cyclic TBoxes it is PSpace complete
under the descriptive semantics [13] as well as greatest and least fixed point
2 M. Mendler, S. Scheele
semantics [1] and it becomes ExpTime complete for general TBoxes (descrip-
tive semantics) [12, 4]. On the other side, subsumption in EL remains in PTime
for cyclic and acyclic TBoxes under all three semantics [3] and even for general
descriptive TBoxes [8, 12]. There are several extensions to the EL language one
can make without losing tractability, such as adding ⊥, >, nominals, concrete
domains and more [6]. The addition of disjunction t, which brings back Boolean
expressiveness, results in coNP hardness [8] for empty TBoxes, PSpace for
acyclic and ExpTime completeness for cyclic and general TBoxes [4]. See [11]
for an overview on the EL family.
Presumably it is fair to assume that applications of logic-based knowledge
engineering, in particular those involving mass data or real-time interaction, will
tend to sacrifice expressiveness for higher performance of reasoning services. The
search for tractable fragments below ALC is not only expedient from a practical
perspective, it still appears there is quite some playground left to be explored.
On the one hand, the existing fragments FL and EL represent only two of the
four corners of the Aristotelian classification square: FL0 with {∀, u} permits
us to make general statements of the form “all S are P” while EL with {∃, u}
corresponds1 to “some S are P”. Less attention has been given to the so-called
contraries “no S is P” and “not all S are P” which correspond to fragments {∀, t}
and {∃, t}. Are these also useful as a basis in specific applications and if so what
are their complexities? On the other hand, there is the semantics issue: The stan-
dard descriptive semantics which follows a classical Tarskian model-theory is not
the only reasonable way of interpreting concept description languages. There is
the Scottian least fixed or greatest fixed point view for cyclic TBoxes introduced
by Nebel [18] or the automata-theoretic interpretation of Baader [1]. Also, the
concept algebras introduced by Dionne et al. [19, 10] provide alternative ways
of giving intensional semantics to concept descriptions and TBoxes. Depending
on application and language fragment some of these may be more appropriate
than the classical descriptive semantics. The semantics issue, too, leaves room
for further systematical investigations.
The aim of this paper is to show that the choice of semantics can play a de-
cisive role for the complexity of the subsumption problem in certain fragments
of ALC. Specifically, we will show that for the {∃, t} fragment, here named UL,
there is an exponential gap between the classical descriptive semantics which
gives ExpTime-complete subsumption checking while for the constructive se-
mantics [16] the problem lies in PTime. Like Dionne et al.’s concept algebras,
the constructive interpretation is intensional but is based on a modal extension
of Heyting algebras which are more general and also cover full ALC. They admit
an elementary presentation using Kripke models which enrich the traditional
descriptive interpretation naturally by a reflexive and transitive refinement re-
lation for concept abstraction and refinement. The idea behind the constructive
1
To see this consider conjunction u as representing generic affirmative statements
with > as nullary case and disjunction t as a generic refutative statement with ⊥
as the degenerated case. Of course, the refutation about t consists in giving choices,
thus avoiding commitment.
Constructive UL is PTIME 3
semantics [16] is that concepts must not be taken as absolute references for
clearly delineated sets of object instances but as intensional descriptions that
are subject to context and negotiation. This is important for situations in which
knowledge is incomplete or evolving such as business auditing, where the data
populating the concepts are produced in continuous streams which are poten-
tially infinite. In this case role filling may involve actions that brings data into
existence only at auditing time. There, the open world assumption of classical
descriptions is too weak, since it is not dynamic, while the constructive semantics
is robust. In [16] a number of examples are given to illustrate the issue. Showing
that it turns the classically intractable problem for UL tractable further justifies
the interest in the constructive semantics.
2 Constructive Semantics for ALC
Concept descriptions are built from role names NR and concept names NC as
follows
C, D ::= A | > | ⊥ | ¬C | C u D | C t D | C v D | ∃R.C | ∀R.C,
where A ∈ NC and R ∈ NR . This syntax is more general than standard ALC in
that it includes subsumption v as a concept–forming operator. The fact that v
can be nested will be irrelevant for the purposes of this paper. Still, we present
the constructive semantics for the full system:
Definition 1 ([16]). A constructive interpretation of ALC is a structure I =
(∆I , I , ⊥I , ·I ) consisting of
– a non-empty set ∆I of entities;
– a refinement pre-ordering I on ∆I (reflexive and transitive);
– a subset ⊥I ⊆ ∆I of fallible entities closed under refinement and role filling,
i.e., x ∈ ⊥I and x I y or xRI y implies y ∈ ⊥I for all R ∈ NR ; also x ∈ ⊥I
means that for all R ∈ NR there exists y ∈ ∆I such that xRI y;
– finally an interpretation function ·I mapping each role name R ∈ NR to a
binary relation RI ⊆ ∆I × ∆I and each concept name A ∈ NC to a set
⊥I ⊆ AI ⊆ ∆I which is closed under refinement, i.e., x ∈ AI and x I y
implies y ∈ AI .
I is lifted from constant ⊥ and concept names A to arbitrary concepts as seen
below, where ∆Ic =df ∆I \ ⊥I is the set of non-fallible elements in I:
>I =df ∆I
(¬C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ y 6∈ C I }
(C u D)I =df C I ∩ DI
(C t D)I =df C I ∪ DI
(C v D)I =df {x | ∀y ∈ ∆Ic . (x I y & y ∈ C I ) ⇒ y ∈ DI }
(∃R.C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ ∃z ∈ ∆I . (y, z) ∈ RI & z ∈ C I }
(∀R.C)I =df {x | ∀y ∈ ∆Ic . x I y ⇒ ∀z ∈ ∆I . (y, z) ∈ RI ⇒ z ∈ C I }.
4 M. Mendler, S. Scheele
Entities in ∆I are partial descriptions representing incomplete information
about individuals. Read a b as saying that b “is a refinement of ” a. The differ-
ence to the classical descriptive semantics is the refinement dimension I and
the universal quantification ∀y ∈ ∆Ic . x I y ⇒ . . . in the clauses of Definition 1.
If I trivialises to the identity relation, i.e., each entity refines only itself, and
if ⊥I = ∅, then the constructive semantics coincides with the classical descriptive
semantics of ALC. Therefore, the constructive semantics includes the classical
one.
Let cALC be ALC under the constructive interpretation. Then cALC is re-
lated to the constructive modal logic CK (Constructive K) [20, 7, 15] as ALC is
related to the classical modal system K [9]. In cALC the classical principles of
the Excluded Middle C t ¬C ≡ >, Double Negation ¬¬C ≡ C, the dualities
∃R.C ≡ ¬∀R.¬C, ∀R.C ≡ ¬∃R.¬C and Disjunctive Distribution ∃R.(C t D) ≡
∃R.C t∃R.D are no longer tautologies but non-trivial TBox statements (cf. [16]).
In particular, consider Disjunctive Distribution: Imagine a dynamic data model
so that role filling for R is a process which involves accessing a remote data
base. Then role filling is a computation which interacts with the environment to
access/generate the data. In this case the disjunctive decision C t D can only
be made once the (R-filler) context to access the data has been established.
This means that the data model may well guarantee ∃R.(C t D), yet it would
be rather strong to assume it also satisfies ∃R.C t ∃R.D where the decision is
outside the scope of R and thus available before the R-filler is even requested.
Before we can embark on the main technical developments we need to intro-
duce some pieces of notation. First, it will be convenient (to save indices) to use
a semantic validity relation |= as follows: Write I; x |= C to abbreviate x ∈ C I
in which case we say that entity x satisfies concept C in the interpretation I.
Further, I is a model of C, written I |= C iff ∀x ∈ ∆I . I; x |= C. All uses of
|= are extended to sets Φ of concepts, I; x |= Φ, I |= Φ in the usual universal
fashion. Let Θ be a set of TBox axioms, and Γ a set of concept descriptions.
We write Θ; Γ |= C if for all models I of Θ it is the case that every entity
x ∈ ∆I which satisfies all axioms in Γ must also satisfy concept C. Formally,
∀I.∀x ∈ ∆I . (I |= Θ & I; x |= Γ ) ⇒ I; x |= C. The reasoning task which we are
interested in here is subsumption in the presence of TBox axioms: The statement
Θ; {C} |= D expresses that concept C is subsumed by concept D in the presence
of terminology Θ, i.e., for all models I |= Θ we have C I ⊆ DI ; Unlike in the
classical semantics of ALC, we cannot reduce subsumption to non-satisfiability
since Θ; {C, ¬D} |= ⊥ is not the same as Θ; {C} |= D. For convenience, the
latter will be written Θ; C |= D saving the braces. Note that subsumption is
defined relative to all constructive models. If we wish to restrict to the classical
models we write Θ; C |=cl D, meaning that for all classical models I |= Θ we
have C I ⊆ DI .
In the following we will consider TBoxes Θ which consist entirely of subsump-
tions C v D such that both C, D are v-free. These are usually called general
TBoxes. We will investigate subsumption checking relative to general TBoxes
for the existential-disjunctive fragment of ALC, called UL. This is the class of
Constructive UL is PTIME 5
concept descriptions formed as
C, D :: = > | ⊥ | A | C t D | ∃R.C
with A ∈ NC and R ∈ NR . Notice that in this fragment we can have uncon-
ditional negative and positive axioms C and ¬C included in TBoxes, viz. as
subsumptions C v ⊥ and > v C. The PTime result will hold for the guarded
fragment of UL. A concept description C is (existentially) guarded if it is not a
disjunction, or equivalently, if all disjunctions appearing in C are guarded behind
existential quantifiers. A general UL TBox Θ is called (existentially) guarded if
in every C v D ∈ Θ the conclusion D is guarded.
3 Guarded U L0 is ExpTime hard for Classical Descriptive
Semantics
We reduce subsumption in the language FL0 consisting of operators {∀, u} to
subsumption in UL under classical descriptive semantics. In fact, we will reduce
subsumption in FL0 to the fragment UL0 , which is UL without the constants
>, ⊥, and relative to guarded UL0 TBoxes. Let Θ be a general TBox in FL0 and
C, D two FL0 concept descriptions. For simplicity we assume that NC contains
exactly the concept names appearing in Θ or C, D. The first step in our re-
duction dualises the problem under the classical descriptive semantics, replacing
u 7→ t and ∀ 7→ ∃ and swapping left and right-hand sides of subsumptions. For-
mally, define the dual d (C) of a FL0 concept description recursively as follows:
d (A) =df A, d (C u D) =df d (C) t d (D), d (∀R.C) =df ∃R.d (C). Further, the
dual of the TBox is d (Θ) =df {d (D) v d (C) | C v D ∈ Θ}. Then, one shows
Θ; C |=cl D ⇐⇒ d (Θ); d (D) |=cl d (C). Obviously, the dualised FL0 concepts
d (D), d (C) are now UL0 expressions and d (Θ) is a general TBox of UL0 . d (Θ)
need not be existentially guarded, though. However, this can be fixed.We intro-
duce a new role τ to guard the TBox inclusions making sure that the effect of
τ can be compensated for by choosing the right classical interpretations. Given
an UL0 TBox Θ we define its expansion
exp(Θ) =df {C v ∃τ.D | C v D ∈ Θ}
∪ { ∃R.X v ∃τ.∃R.X, ∃τ.∃R.X v ∃R.X | ∃R.X ∈ Sf(Θ)}
∪ {A v ∃τ.A, ∃τ.A v A | A ∈ NC },
where Sf(Θ) denotes the set of sub-concepts of Θ. Clearly, all subsumptions
in exp(Θ) are guarded. Because of the additional axioms, the new role τ is
semantically “silent” and does not add any information. Observing Θ; C |=cl
D iff exp(Θ); C |=cl D, classical subsumption checking for Θ in FL0 is now
reduced to exp(Θ) in guarded UL0 :
Lemma 1. Let C, D be FL0 concept descriptions and Θ a general TBox of FL0 .
Then, Θ; C |=cl D iff exp(d (Θ)); d (D) |=cl d (C).
6 M. Mendler, S. Scheele
Lemma 1 gives a linear-time reduction of the FL0 problem to that in UL0 ,
where the simulating TBox exp(d (Θ)) is existentially guarded. Since subsump-
tion checking in FL0 for general TBoxes and classical descriptive semantics is
ExpTime hard [12, 4] we have the following theorem:
Theorem 1. UL0 subsumption checking under the classical semantics and rel-
ative to existentially guarded (general) TBoxes is ExpTime hard.
It is important to realise that the reduction behind Thm. 1 depends crucially
on the classical nature of the semantics, the DeMorgan dualities and the exis-
tential distribution |=cl ∃R.(C t D) ≡ (∃R.C t ∃R.D). As has been pointed out
by Hofmann [12] the presence and absence of such distributive laws can make
the difference between ExpTime and PTime complexity. In ExpTime FL0 the
operators {u, ∀} distribute while in the PTime fragment {u, ∃} [2, 12] they do
not.
4 Guarded U L is in PTime for Constructive Descriptive
Semantics
In the following we will show that subsumption checking in UL under the con-
structive semantics and relative to existentially guarded TBoxes is in PTime. We
obtain a PTime decision procedure for UL by the calculus presented in Fig. 1.
The calculus is formulated in the style of Gentzen with left introduction rules
tL, vL, ∃LR, ⊥L and right introduction rules tR1 , tR2 , ∃LR, >R for each
logical connective of UL. We will show that the calculus is sound and complete
for UL under the constructive semantics.
Let I be a constructive interpretation and a ∈ ∆I an entity in I. We say
that the pair (I, a) satisfies a sequent Θ; C ` D if I is a model of Θ, i.e., I |=
Θ, and I; a |= C as well as I; a 6|= D. A sequent Θ; C ` D is (constructively)
satisfiable, iff there exists (I, a) which satisfies the sequent. This is equivalent to
non-subsumption Θ; C 6|= D (see page 4). Completeness of the calculus of Fig. 1
means that if no proof can be found for Θ; C ` D then the sequent is satisfiable.
Soundness means that whenever Θ; C ` D is derivable then Θ; C |= D, i.e. C is
subsumed by D. While soundness is easy to establish completeness requires a
number of auxiliary tools which we introduce next.
Definition 2. A concept description P is called (constructively) prime in a
TBox Θ if for all D1 , D2 ∈ Sf(Θ) ∪ Sf(P ), whenever Θ; P |= D1 t D2 then
Θ; P |= D1 or Θ; P |= D2 .
The trouble for the classical semantics is that TBoxes have only very few
if any prime concepts. Instead, the TBox must be saturated by adding and
manipulating instances in terms of sets of concepts. Such sets of concepts are
needed to pin down a hypothetical individual sufficiently for going through all the
case analyses needed to decide a given subsumption in the context of Θ. On the
other hand, constructive TBoxes have more prime elements, i.e., single concept
Constructive UL is PTIME 7
Ax ⊥L >R
Θ; C ` C Θ; ⊥ ` C Θ; C ` >
Θ; E ` C Θ; E ` D Θ; C ` F Θ; D ` F
tR1 tR2 tL
Θ; E ` C t D Θ; E ` C t D Θ; C t D ` F
Θ; E ` C Θ; D ` F Θ; C ` D
vL ∃LR
Θ, C v D; E ` F Θ; ∃R.C ` ∃R.D
Fig. 1. Gentzen sequent rules for UL.
descriptions which are able to capture a whole set of individuals completely.
The striking feature of constructive ALC is that existential concepts are always
constructively prime for the empty TBox.
Proposition 1. Every existentially guarded UL concept description C is con-
structively prime for the empty TBox.
Proof. By induction on the structure of C and the definition of |= for the con-
structive semantics (see page 4). t
u
Proposition 1 is the reason why for existentially guarded UL the constructive
calculus for ALC [16] can be restricted to the simple form of sequents Θ; C ` D
manipulated in Fig. 1 without losing completeness. The following Props. 2 and 3
will be instrumental for proving this.
Proposition 2 (Cut Admissibility). In the proof system of Fig. 1 the cut
rule is admissible, i.e., if Θ; C ` D and Θ; D ` E then Θ; C ` E.
Proof. Given derivations for Θ; C ` D and for Θ; D ` E we show Θ; C ` E by
induction on the derivations and the cut formula D. t
u
Proposition 3 (Provable Primes). Let Θ be an existentially guarded TBox
and P, C1 , C2 concept descriptions. If P is existentially guarded then Θ; P ` C1 t
C2 implies Θ; P ` C1 or Θ; P ` C2 .
Proof. We proceed by induction on the derivation for Θ; P ` D1 t D2 . Since P
is not a disjunction, the last rule in this derivation cannot be Ax , tL, ∃LR or
>R. If the last rule is ⊥L or one of tR1 , tR2 the claim follows immediately.
The only interesting case is when the derivation ends in an application of vL,
i.e., it looks like
.. ..
. π1 . π2
Θ; P ` E Θ; F ` D1 t D2
vL
Θ, E v F ; P ` D1 t D2
By assumption on our TBox from which E v F is drawn, F is guarded. Hence
we may invoke the induction hypothesis on the sub-derivation π2 . This gives a
8 M. Mendler, S. Scheele
derivation π20 for Θ; F ` Di for some i = 1, 2, from which we get
.. .. 0
. π1 . π2
Θ; P ` E Θ; F ` Di
vL
Θ, E v F ; P ` Di
as desired. t
u
The next observation we need to make is that all concept descriptions in a
UL TBox Θ can be decomposed and fully covered by the guarded elements of
Sf(Θ). Define a relation C D P iff P is a (maximal) guarded sub-expression of
C. If C is guarded then C D C. Otherwise, C = C1 t C2 is a disjunction and
one of Ci must contain the guarded sub-expression P .
Lemma 2 (Coverings). Let C be a concept description in UL and Θ a TBox.
Then,
(i) If C D P and Θ; C ` E then Θ; P ` E
(ii) If Θ; P ` E for all C D P then Θ; C ` E.
Proof. (i) The proof depends on cut admissibility and the fact that if C D P
then Θ; P ` C. This can be proved easily by induction on C. (ii) Again, this
is by induction on the structure of C. For constants >, ⊥, concept names and
existentials the statement is trivial, since for these C D C. For disjunctions we
notice that C1 t C2 D P iff C1 D P or C2 D P . Hence, if Θ; P ` E for all
C1 t C2 D P we have Θ; Ci ` E for both i = 1, 2 by induction hypothesis and
thus Θ; C1 t C2 ` E by way of rule tL. t
u
From now on we will assume that the UL TBox Θ is existentially guarded.
We build a constructive interpretation I based on guarded concept descriptions
by letting ∆I consist of the set of pairs (C, ΨC ) where C is guarded and ΨC is a
finite map associating with each role R ∈ NR a set ΨC (R) ⊆ Sf(Θ) of concept de-
scriptions such that the formal (intensional) consistency requirementF Θ; C 6` ΨC
holds. This consistency condition is an abbreviation for Θ; C 6` ∃R. X∈ΨC (R) X
for all R ∈ NR such that ΨC (R) 6= ∅. The guarded concept description C in a
pair (C, ΨC ) records the extensional information characterising the entity repre-
sented by (C, ΨC ) while the second component ΨC encodes additional intensional
information. Each entry X ∈ ΨC (R) specifies the R-fillers in the sense that every
entity consistent with the concepts in ΨC (R) will be an R-filler of (C, ΨC ). In
our case we can further restrict the structure to ΨC = ∅ or ΨC = [R 7→ X], i.e.
ΨC (R) = ∅ for all R ∈ NR or for exactly one R ∈ NR we have ΨC (R) = {X},
respectively. Note that the pair (C, ∅) is always consistent regardless of C and
that (C, [R 7→ X]) is consistent iff Θ; C 6` ∃R.X.
Constructive UL is PTIME 9
The canonical model I is given by an interpretation of concept names, filler
and refinement relations RI and I on I, respectively, as follows:
(C, ΨC ) ∈ AI ⇐⇒ Θ; C ` A
(C, ΨC ) ∈ ⊥I ⇐⇒ Θ; C ` ⊥
(C, ΨC ) RI (D, ΨD ) ⇐⇒ ∀X ∈ ΨC (R). Θ; D 6` X
(C, ΨC ) I (D, ΨD ) ⇐⇒ Θ; D ` C.
Observe that the constructive semantics distinguishes between two kinds of con-
sistencies, viz. extensional consistency, if (C, ΨC ) 6∈ ⊥I and intensional consis-
tency, if Θ; C 6` ΨC . Our canonical I contains only intensionally consistent ob-
jects, though they may be extensionally inconsistent. In such an entity (C, ΨC ) ∈
⊥I we must necessarily have ΨC (R) = ∅ for all R ∈ NR . For if ΨC (R) = {X} for
some R and X then Θ; ⊥ ` ∃R.X by rule ⊥L which by the assumption Θ; C ` ⊥
and cut admissibility would yield Θ; C ` ∃R.X in contradiction to intensional
consistency of (C, ΨC ). But ΨC (R) = ∅ means the entity (C, ΨC ) does not ex-
clude any R-fillers, i.e. (C, ΨC ) RI (D, ΨD ) for every intensionally consistent pair
(D, ΨD ). Notice again that every pair (C, ∅) is intensionally consistent and thus
an object in I.
Clearly, I is reflexive because of rule Ax and transitive because of cut ad-
missibility Prop. 2. It is not antisymmetric, though, due to the slack in the second
component ΨD which has no influence on I . In fact, it contains cycles since,
e.g., (C, ΨC ) I (C, ∅) and also (C, ∅) I (C, ΨC ) for all ΨC . Truth valuations
⊥I and AI are closed under I due to cut admissibility. Extensionally inconsis-
tent objects ⊥I partake in all UL concept descriptions, i.e., for all UL concepts,
⊥I ⊆ C I . Thus, I is a constructive model according to Def. 12 .
Lemma 3. Let Θ be an existentially guarded TBox and E an arbitrary UL
concept description. Then, for every (C, ΨC ) ∈ I, we have I; (C, ΨC ) |= E iff
Θ; C ` E.
Proof. We proceed by induction on E. For concept names and ⊥ the statement
follows directly from the definition of AI . For > we need to use rule >R. The
interesting cases are existentials and disjunction:
Let (C, ΨC ) ∈ I and suppose Θ; C 6` ∃R.E, which in particular implies Θ; C 6` ⊥
by cut admissibility and ⊥L. Then the pair (C, [R 7→ E]) is intensionally and
extensionally consistent. The latter follows from Θ; C 6` ⊥ and the former from
Θ; C 6` ∃R.E. Thus, (C, [R 7→ E]) is an entity in I and also (C, [R 7→ E]) I
(C, [R 7→ E]) with (C, [R 7→ E]) ∈ ∆Ic = ∆I \⊥I . Consider any R-filler (C, [R 7→
E]) RI (D, ΨD ) which must satisfy Θ; D 6` E by definition. Now we use the in-
duction hypothesis to infer I; (D, ΨD ) 6|= E which proves I; (C, ΨC ) 6|= ∃R.E
according to Def. 1, all in all. Vice versa, suppose that Θ; C ` ∃R.E and let
(C, ΨC ) I (D, ΨD ) ∈ ∆Ic be given arbitrarily, which means Θ; D ` C and by
2
To be fully compatible also with the constructive semantics of ¬, ∀R we should also
make sure that all R-fillers of objects in ⊥I are themselves extensionally inconsistent.
This is not needed for the existential-disjunctive fragment at hand.
10 M. Mendler, S. Scheele
cut admissibility Θ; D ` ∃R.E. We claim that there exists a guarded compo-
nent P of E such that (P, ∅) is an R-filler of (D, ΨD ). If ΨD (R) = ∅ we can
take any guarded E D P and have (D, ΨD ) RI (P, ∅) for trivial reasons. Oth-
erwise, if ΨD (R) = {X} we must find a guarded component P of E such that
Θ; P 6` X. We proceed by contradiction. Suppose, Θ; P ` X for every P with
E D P . By Lem. 2 (ii) this implies Θ; E ` X. From there, an application of ∃LR
gives Θ; ∃R.E ` ∃R.X and further cut admissibility Θ; D ` ∃R.X which would
contradict consistency of (D, ΨD ). Thus, as claimed, (D, ΨD ) RI (P, ∅) for some
guarded component P of E. By Lem. 2 (i) we have Θ; P ` E from which the
induction hypothesis tells us that I; (P, ∅) |= E which completes the proof that
I; (C, ΨC ) |= ∃R.E according to Def. 1.
Now assume I; (C, ΨC ) |= E1 tE2 , i.e., I; (C, ΨC ) |= Ei for some i = 1, 2. The
induction hypothesis obtains Θ; C ` Ei and thus Θ; C ` E1 t E2 by virtue of rule
tR1 (for i = 1) or tR2 (for i = 2). In the other direction, given Θ; C ` E1 t E2 ,
we get Θ; C ` E1 or Θ; C ` E2 based on the fact that C is guarded (Prop. 3).
In either case we can use the induction hypothesis to conclude I; (C, ΨC ) |= Ei
from which I; (C, ΨC ) |= E1 t E2 follows as required. t
u
Lemma 3 means that I is a constructive model of the TBox Θ. To see this
let F v E ∈ Θ and (C, ΨC ) I (D, ΨD ) such that I; (D, ΨD ) |= F . Therefore,
Θ; D ` F because of Lem. 3. From here we get Θ; D ` E by way of rules vL and
Ax , which implies I; (D, ΨD ) |= E by Lem. 3. Hence, overall, I; (C, ΨC ) |= F v
E.
Proposition 4. The rules in Fig. 1 are sound for constructive subsumption in
UL and complete relative to existentially guarded (general) TBoxes Θ.
Proof. Soundness, viz. that Θ; C ` D implies Θ; C |= D, is proved by induc-
tion on derivations. Regarding completeness, let a subsumption Θ; C |= D be
constructively valid. Consider the canonical model I constructed above which
satisfies I |= Θ. Take any guarded component C D P of C. By Lem. 2 (i) and
rule Ax we have Θ; P ` C. Hence, I; (P, ∅) |= C because of Lem. 3. But then
the assumption Θ; C |= D implies I; (P, ∅) |= D which means Θ; P ` D again
by Lem. 3. Since P with C D P was arbitrary we have shown that Θ; C ` D by
virtue of Lem. 2 (ii). t
u
Theorem 2. Subsumption checking in UL under the constructive semantics and
relative to existentially guarded (general) TBoxes is in PTime.
Proof. Let Θ be an existential TBox and C and D concept descriptions in UL.
We want to decide the subsumption C v D relative to Θ. Due to Prop. 4 we
can decide Θ; C |= D by proof search in the calculus of Fig. 1. Because of the
sub-formula property each possible node in a derivation tree is determined by
a pair of concept descriptions in Sf(Θ ∪ {C, D}). Thus the number of possible
nodes in a tree is at worst quadratic in the size of Θ. We may systematically
tabulate all pairs (X, Y ) ∈ Sf(Θ ∪ {C, D})2 such that Θ; X ` Y using dynamic
programming memorisation techniques and thus decide any fixed subsumption
in polynomial time. t
u
Constructive UL is PTIME 11
5 Conclusion and Future Work
This paper highlights the dramatic effect that the choice of semantic interpreta-
tion can have on the complexity of reasoning in DL. Arguably, as long as there
is no application domain identifiable for the UL fragment these results may only
have theoretical interest. Perhaps our results can be extended to more expres-
sive DLs that may eventually support practical applications. Note that from the
expressiveness point of view the constructive semantics genuinely enriches the
classical descriptive interpretation, so that the low complexity of UL is some-
what unexpected. However, as discussed in [16], the constructive semantics has
useful applications which are independent of this complexity result.
We can see some immediate ways to generalise our results. The main results
carry over to all TBoxes in which every C ∈ Sf(Θ) has a non-empty prime cover
Cov(C) ⊆ Sf(Θ) satisfying the conditions of Prop. 3 and Lem. 2. We have ex-
ploited this here for guarded TBoxes in the UL language where every concept
has a prime cover. We conjecture that the PTime result extends directly to UL−
which is UL plus limited universal quantification ∀R.⊥. For other extensions like
(i) permitting negated atoms ¬A, (ii) adding conjunctions u we expect coNP
hardness, but hopefully not more since the Boolean reasoning should remain
safely contained between the levels of existentials so that the Boolean combi-
natorics does not spill over quantifiers (exploiting that in constructive logic ∀¬
is not the same as ¬∃, etc.). One of our referees has pointed out that if we
remove the guardedness restriction then we could express Disjunctive Distribu-
tion in the TBox which suggests that complexity might rise to ExpTime. Since
we apply constructive rather than classical semantics it is not clear whether
such Disjunctive Distribution in TBoxes necessarily lead to exponentially large
TBoxes/derivations or they can be eliminated in terms of an exponential number
of polynomially sized TBoxes. We leave these investigations to future work.
Finally, it is worthwhile to add that the dualising reduction from FL0 to UL0
used in Section 3 can also be applied to axiomatic (cyclic or non-cyclic) TBoxes
so that several other complexity results for the classical descriptive semantics
should follow in a similar fashion. E.g., all the hardness/completeness results for
EL (see, e.g., [11]) should carry over to the “no S is P” fragment {∀, t} under
the classical semantics. Similarly, coNP-hardness for FL0 in acyclic TBoxes
should imply coNP-hardness for UL0 , PSpace-hardness of FL0 should give
PSpace-hardness of UL0 in cyclic TBoxes. Of course, this applies to the classical
descriptive semantics. For the constructive semantics the situation is open since
DeMorgan-style dualisation does not work.
Acknowledgements This work has been funded by the German Research
Council (DFG) under ME 1427/4-1. The authors would like to thank the anony-
mous reviewers for their suggestions to improve the presentation of this paper.
12 M. Mendler, S. Scheele
References
1. F. Baader. Using automata theory for characterizing the semantics of terminolog-
ical cycles. Annals of Math. and Artificial Intelligence, pages 175–219, 1996.
2. F. Baader. Computing the least common subsumer in the description logic EL
w.r.t. terminological cycles with descriptive semantics. In Proc. Int’l Conf. on
Conceptual Structures (ICCS2003), pages 117–130. Springer LNAI 2746, 2003.
3. F. Baader. Terminological cycles in a description logic with existential restrictions.
In Proc. 18th Int’l Joint Conf. on Artificial Intelligence, pages 325–330. Morgan
Kaufmann, 2003.
4. F. Baader, S. Brandt, and C. Lutz. Pushing the EL-envelope. In Proc. 19th Joint
Conf. on Artificial Intelligence (IJCAI 2005), pages 364–369, 2005.
5. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. Patel-Schneider, edi-
tors. The Description Logic Handbook: Theory, Implementations and Applications.
Cambridge University Press, 2003.
6. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope
further. In Kendall Clark and Peter F. Patel-Schneider, editors, In Proceedings of
the OWLED 2008 DC Workshop on OWL: Experiences and Directions, 2008.
7. G. Bellin, V. de Paiva, and E. Ritter. Extended Curry-Howard correspondence for
a basic constructive modal logic. In Methods for Modalities II, November 2001.
8. S. Brandt. Polynomial time reasoning in a description logic with existential re-
strictions, GCI axioms, and – what else? In R. López de Mantáras and L. Saitta,
editors, Proc. Eur. Conf. on Artificial Intelligence (ECAI-2004), pages 298–302,
2004.
9. V. de Paiva. Constructive description logics: what, why and how. In Context
Representation and Reasoning, Riva del Garda, August 2006.
10. R. Dionne, E. Mays, and F. J. Oles. The equivalence of model-theoretic and
structural subsumption in description logics. In Proc. 13th Int’l Joint Conf. on
Artificial Intelligence (IJCAI’93), pages 710–718, 1993.
11. Ch. Haase and C. Lutz. Complexity of subsumption in the EL family of description
logics: acyclic and cyclic TBoxes. In Proc. Europ. Conf. on Artificial Intelligence
ECAI 2008, 2008.
12. M. Hofmann. Proof-theoretic approach to description-logic. In Proc. Logic in
Computer Science LICS 2005, 2005.
13. Y. Kazakov and H. de Nivelle. Subsumption of concepts in FL0 for (cyclic) termi-
nologies with respect to descriptive semantics is PSPACE complete. In Proc. Int’l
Workshop Description Logics (DL 2003), volume 81 of CEUR Electronic workshop
proceedings, 2003.
14. H. J. Levesque and R. J. Brachman. Expressiveness and tractability in knowledge
representation and reasoning. Computational Intelligence, 3:78–93, 1897.
15. M. Mendler and V. de Paiva. Constructive CK for contexts. In L. Serafini
and P. Bouquet, editors, Context Representation and Reasoning (CRR-2005), vol-
ume 13 of CEUR Proceedings, July 2005. Also presented at the Association for
Symbolic Logic Annual Meeting, Stanford University, USA, 22nd March 2005.
16. M. Mendler and S. Scheele. Towards constructive description logics for abstraction
and refinement. In 21st Int’l Workshop on Description Logics (DL2008). CEUR
Workshop proceedings 353, May 2008.
17. B. Nebel. Terminological reasoning is inherently intractable. Artificial Intelligence,
pages 235–249, 1990.
Constructive UL is PTIME 13
18. B. Nebel. Terminological cycles: Semantics and computational properties. In J. F.
Sowa, editor, Principles of Semantic Networks. Morgan Kaufmann, 1991.
19. F. J. Oles R. Dionne, E. Mays. A non-well-founded approach to terminological
cycles. In Proc. 10th Nat’l Conf. of the Americ. Assoc. for Artificial Intelligence
(AAAI’92), 1992.
20. D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic,
50:271–301, 1990.