Beth Definability in Expressive Description Logics

1 Introduction

We address the Beth definability property [Beth, 1953] in the context of description logics (DLs). The Beth definability property relates two notions of definability in a logic L , implicit definability and explicit definability. Implicit definability is a semantic notion: it asks whether the interpretation of a given L-concept C is fully determined by the universe of discourse and the interpretation of some given predicates Σ (concept and/or role names) in all models of a theory (TBox). Explicit definability on the other hand is more syntactic: it asks whether there is some L -concept D over the set of predicates Σ that is equivalent to C under T . Clearly, explicit definability implies implicit definability. If the converse holds as well, then the logic L is said to have the Beth definability property. Since the Beth definability property connects the model-theoretic notion of implicit definability to explicit

∗The author is supported by the NSF grant IIS-0905276.

†The author is also affiliated with Universit¨at Bremen.

˙Inanc¸ Seylan†

Free University of Bozen-Bolzano

seylan@inf.unibz.it

definability, logics having this property are considered to be well-balanced in terms of their syntax and semantics.

Besides the theoretical interest, there are two useful applications of this property in DLs which are concerned with rewritings. The first one is related to extracting an equivalent terminology from a general TBox [Baader et al., 2003; ten Cate et al., 2006]. A terminology consists only of acyclic definitions for concept names and they are of particular interest because reasoning with them is 'easier' than with general TBoxes. For example, satisfiability of an ALC-terminology is a PSPACE-complete problem whereas the same problem for general ALC-TBoxes is EXPTIME-complete [Baader et al., 2003]. The second use case is related to computing the certain answers of a concept query given a database (DB) instance (also referred to as 'DBox' in this context) and a TBox that may speak about more predicates than the DB instance [Seylan et al., 2009]. Here the idea is to find an equivalent rewriting of the original query in terms of the predicates that appear in the DB instance. If such a rewriting exists then determining the certain answers of the query can be done efficiently because the problem is reduced to query answering in relational DBs.

Both use cases involve computing explicit definitions on the basis of implicit definitions. A vital question is what is the complexity of this task, both in terms of the time needed to compute the explicit definitions, and in terms of the size of the explicit definitions obtained. This question was first studied by ten Cate et al. for a weaker Beth definability property which considers only concept names in the signature [ten Cate et al., 2006]. In this paper we are interested in the more general Beth definability property that takes into account role names in the signature. We believe that this is more natural for DLs because in a DL knowledge base, role names are considered to be a part of the signature.

Our contributions in this paper are as follows.

• We obtain a complete classification of the Beth definability property for extensions of ALC with transitive roles, inverse roles, role hierarchies, and/or functionality restrictions, both on arbitrary structures (BP) and on finite structures (BPF). These results are summarized in Table 1. Note that the finite model property (FMP) of all sublogics of SHOQ follows from [Lutz et al., 2005]; FMP of all sublogics of SHIO+ follows from [Duc and Lamolle, 2010]; the failure of FMP in ALCFI and all its extensions

follows from [Baader et al., 2003].

• We present a constructive algorithm based on tableaux to compute explicit definitions in ALC and all of its considered extensions having the Beth definability property. This algorithm runs in 2-EXPTIME and computes in the worst case an explicit definition of double exponential size if the concept is implicitly definable. In this respect, the algorithm is optimal because we also show that the smallest explicit definition of an implicitly defined concept may be double exponentially long in the size of the input TBox for each of these DLs.
• We consider the case where explicit definitions are allowed to be expressed in first-order logic. This is particularly relevant for the use case for computing certain answers of a query given a DB instance and a TBox. We present an algorithm that computes a first-order explicit definition of an implicitly defined concept in single EXPTIME for all DLs with BP or BPF.

2 Preliminaries

We assume familiarity with the DLs ALC and SHIF [Baader et al., 2003; Horrocks et al., 2000]. SHIF is the theoretical basis of the Web Ontology Language OWL-Lite [Horrocks et al., 2003]. In what follows, we will freely use the terminology and notation from [Horrocks et al., 2000]. However for convenience of exposition, we assume role inclusion axioms (RIAs) to be part of the TBox instead of a separate role hierarchy.

We will use signatures often in our definitions. The full signature of SHIF consists of NC, NR, and NR+ ⊆ NR. Here NC and NR are countably infinite and mutually disjoint sets of concept names and role names, respectively; and NR+ is a countably infinite set of transitive role names. By a predicate, we mean an element of NC or NR. For all R ∈ NR, R- denotes its inverse. The set of roles is defined as NR ∪ {R- | R ∈ NR}. The function Inv over roles is defined as Inv(R) = R- if R ∈ NR, and Inv(R) = S if R = S- for an S ∈ NR. The boolean function Trans with domain roles is defined such that Trans(R) = 1 if and only if R ∈ NR+ or Inv(R) ∈ NR+.

In this paper, we will be considering several DLs that are fragments of SHIF. Following the standard naming scheme, letters in the name of a language indicate the constructors supported in that language. I stands for inverse roles and without its presence the set of roles is equal to the set of role names, i.e., NR. S stands for transitive role names and without its presence the set of transitive role names NR+ is assumed to be empty. F stands for allowing ≤ 1R in the concept language for every role R. H stands for RIAs and without its presence the TBoxes do not contain any RIAs. The 'vanilla' DL without any of these constructors is ALC. ALC with transitive role names is denoted as S but we will sometimes use ALCS for convenience. As usual transitive roles and roles with transitive sub-roles are not allowed in concepts of the form ≤ 1R in logics with S and F because of decidability concerns [Horrocks et al., 2000]. Finally, we use the symbol L as a placeholder for any of these DLs.

For an L-concept C0, the set sub(C0) consists of C0 and all its subconcepts. For a concept C0 and a TBox T , rol(C0, T ) denotes the set of roles occurring in C0 or T ; and sig(C0, T ) denotes the set of concept and role names occurring in C0 or T , i.e., the signature of C0 and T .

The Beth definability property, in the general sense, has been first shown to hold for first-order logic [Beth, 1953]. Beth definability comes in different flavors and the one we are interested in is related more to projective Beth definability. The projective version is known be stronger than Beth's original formulation [Hoogland, 2001]. Beth definability for first-order fragments used in database theory, e.g., conjunctive queries, can be used as a framework for query rewriting using exact views [Nash et al., 2010]. Besides the treatment of the topic in first-order logic, Lang and Marquis, also motivated from AI, study the propositional variant [Lang and Marquis, 2008]. Beth definability has been extensively studied for modal logics [Gabbay and Maksimova, 2005]. Because of the presence of TBoxes, the version of the Beth definability property we are interested in is for the global consequence relation in modal logics [Goranko and Otto, 2007].

Constructive methods to show Beth definability in DLs have been previously studied in [ten Cate et al., 2006; Seylan et al., 2009; 2010]. These papers also present some results on the size of explicit definitions that can be obtained for implicitly defined concepts. [ten Cate et al., 2006] establish a single exponential lower bound and a triple exponential upper bound for ALC. It is not hard to see that the lower bound proof of [ten Cate et al., 2006] carries to the Beth definability property we consider; and the matching single exponential upper bound on the size of explicit definitions was established in [Seylan et al., 2010]. Here the notion of the 'size' of a concept C is subtle and one can define it either as (i) the number of occurrences of symbols needed to write C, or as (ii) the cardinality of the set of C's subconcepts, i.e., sub(C). For example the algorithm of [Seylan et al., 2010] implies a double exponential upper bound when one uses (i) to measure the size of a concept instead of (ii). Therefore a matching lower bound on the size of explicit definitions was an open problem for the case of (i). Because of this subtlety, we fix what we mean by size for the rest of the paper.

Definition 2.1. The size of a L-concept C0, written |C0|, is the number of occurrences of symbols needed to write C0. The size of a L -TBox T , written |T |, is defined analogously.

In the rest of the section, we introduce notions that are related to Beth definability.

Definition 2.2 (Implicit definability). Let C be an Lconcept, T a L-TBox, and Σ ⊆ sig(C, T ). C is implicitly definable from Σ under T if and only if for any two models I and J of T , if

• ΔI =ΔJ and
• for all P ∈ Σ, P I = P J

then C

C

J .

In other words, given a TBox, a concept C is implicitly definable if the set of all its instances depends only on the extension of the predicates in Σ. Deciding implicit definability in L means, given an L-concept C, L-TBox T , and a set of predicates Σ ⊆ sig(C, T ), to check whether C is implicitly definable from Σ under T . For every predicate P ∈ sig(C, T ) \ Σ, introduce a new predicate P ′ which is not in sig(C, T ). Now let ˜ C ( ˜ T ) be the concept (TBox) obtained by replacing every occurrence of a predicate P ̸∈ Σ in C (T ) by P ′ . The following lemma provides an alternative, more syntactic definition of implicit definability. In particular, it reduces implicit definability in L to the entailment problem in L .

Lemma 2.3. Let C be a L-concept, T be a L-TBox, and Σ ⊆ sig(C, T ). Then C is implicitly definable from Σ under T if and only if T ∪ ˜ T |= C ≡ ˜ C.

It is also possible to reduce TBox-unsatisfiability to implicit definability.

Lemma 2.4. Let T be a L-TBox and let A0 be a concept name that does not appear in T . Then T is unsatisfiable if and only if A0 is implicitly definable from sig(T ) under T .

By Lemmas 2.3 and 2.4, the following theorem follows immediately, given that the concept satisfiability problem for each of these DLs is EXPTIME-complete.

Theorem 2.5. In ALC and any of its extensions with constructors from {S,H, I ,F}, implicit definability is EXPTIME-complete.

If a concept is implicitly definable from Σ, then it may be possible to find an expression using only predicates in Σ whose instances are the same as in the original concept: this would be its explicit definition.

Definition 2.6 (Explicit definability). Let C be a Lconcept, T a L-TBox, and Σ ⊆ sig(C, T ). C is explicitly definable from Σ under T if and only if there is some Lconcept D such that T |= C ≡ D and sig(D) ⊆ Σ. Such a D is called an explicit definition of C from Σ under T .

Proposition 2.7. Let C be a L-concept, T a L-TBox, and Σ ⊆ sig(C, T ). If C is explicitly definable from Σ under T then C is implicitly definable from Σ under T .

Definition 2.8 (Beth definability property). L has the Beth definability property (BP) if for all L-concepts C, all LTBoxes T , and all signatures Σ ⊆ sig(C, T ), if C is implicitly definable from Σ under T then C is explicitly definable from Σ under T .

I =

Clearly, we can restrict the role names that are allowed to appear in our explicit definitions by putting these role names into Σ. Let us call the version of BP that does not restrict role names but only concept names occurring in the explicit definitions the concept name BP (CBP). That is in CBP, we look for explicit definitions over subsets of Σ ∪ NR.

A logic may lack the finite model property (FMP) and in some cases it is more natural to consider only finite models. This is also the approach taken in DB theory. For example, in a DL KB with a DB instance, the purpose of the DB instance is to fix the extension of some predicates [Seylan et al., 2009]. Some DLs lack FMP and because of this the TBox may enforce the DB instance to be infinite, i.e., the DB instance can not be fixed.

Definition 2.9 (Finite model property). An interpretation is said to be finite if it has a finite domain. A DL L is said to have the finite model property (FMP) if for every L -concept C and every L -TBox T , if C is satisfiable w.r.t. T then there is some finite interpretation I such that I is a model of T and CI ̸= ∅.

A relevant question in this case is if the Beth definability property holds when one restricts attention to finite models. For example, Beth definability, when restricted to finite models, fails in first-order logic [Hoogland, 2001] although it holds in the unrestricted case. In this paper, we therefore also investigate BP restricted to finite interpretations. We call this version of the problem Beth definability property in the finite (BPF). Instead of redefining the relevant notions for BPF, we assume that all our definitions are the same except that we replace the word 'model' with 'finite model' and the symbol |= with |=f , where |=f considers only finite models. We call this version of implicit (explicit) definability f-implicit (resp. f-explicit) definability when we want to be precise.

If L has FMP then BP are BPF are equivalent because of Lemma 2.3 and the fact that |= coincides with |=f . Hence it only makes sense to consider BPF in logics without FMP.

3 Constructive Interpolation with Tableaux

This section provides a constructive proof of an interpolation property which will be the essential part of the proof of BP in Section 4. Resorting to interpolation to show the Beth definability property in a logic has been a standard technique since Craig's seminal paper [Craig, 1957]. We start by defining what we mean by an interpolant and then state the main result of this section.

Definition 3.1 (Interpolant). Let C,D be L-concepts and let T1, T2 be L -TBoxes such that T1 ∪ T2 |= C ⊑ D. An L - concept I is called an interpolant of C and D under 〈T1, T2〉 if the following conditions hold:

• sig(I) ⊆ sig(C, T1) ∩ sig(D, T2),
• T1 ∪ T2 |= C ⊑ I, and
• T1 ∪ T2 |= I ⊑ D.

Theorem 3.2. Let L be ALC or any of its extensions with constructors from {S, I , F}. For all L -concepts C1, C2 and all L-TBoxes T1, T2, if T1 ∪T2 |= C1 ⊑ C2 then there exists an interpolant of C1 and C2 under 〈T1, T2〉 that can be computed in time double exponential in |T1|+|T2|+|C1|+|C2|.

The proof of Theorem 3.2 consists of two stages. First Theorem 3.2 is shown to hold for ALC and ALCF directly using a worst-case optimal tableau algorithm in the style of Gor´e and Nyugen [Gor´e and Nguyen, 2007]. Then we show that Theorem 3.2 holds for extensions of ALC and ALCF via satisfiability and signature preserving reductions to ALC and ALCF .

It will be convenient for us to assume that concepts are in negation normal form (NNF) in the rest of the section. This is w.l.o.g. if we take e.g. ∀R.C not as an abbreviation of ¬∃R.¬C but as a primitive constructor of the language. The NNF of the complement of a concept C is written ˙¬C. Again w.l.o.g., we assume that a TBox consists only of axioms of the form ⊤ ⊑ C.

Definition 3.3. Let C0 be an ALCF-concept (ALCFIconcept) and let T be an ALCF-TBox (ALCFI-TBox). The concept closure cl(C0, T ) of C0 and T is the smallest set of concepts satisfying the following conditions:

• C0 ∈ cl(C0, T );
• if ⊤ ⊑ C ∈ T then C ∈ cl(C0, T );
• if C ∈ cl(C0, T ) and D ∈ sub(C) then D ∈ cl(C0, T );
• {≤ 1R, ∃R.C} ⊆ cl(C0, T ) then ∀R.C ∈ cl(C0, T ).

For the rest of this section, fix two ALCF-concepts C0 and D0, and three ALCF-TBoxes Tl, Tr, and T such that Tl ∪ Tr = T . l stand for left and r for right and it is a naming scheme adopted from [Fitting, 1996]. It will allows us to identify from which TBox (Tl or Tr) or concept (C0 or D0) an inference is made.

A biased concept is an expression of the form C λ , where C is an ALCF-concept and λ ∈ {l, r} is a bias. Two relevant biased concept closures cll and clr are defined as follows.

We use the Greek letters λ, κ to denote a bias.

Definition 3.4. Let Φ ⊆ cll ∪ clr. Then

• (C1 ⊓ C2)λ is an ⊓-burden of Φ iff (C1 ⊓ C2)λ ∈ Φ and {(C1)λ , (C2)λ } ̸⊆ Φ;
• (C1 ⊔ C2)λ is an ⊔-burden of Φ iff (C1 ⊔ C2)λ ∈ Φ and {(C1)λ , (C2)λ } ∩ Φ = ∅;
• (≤ 1R)λ is an ≤ 1-burden of Φ iff (≤ 1R)λ ∈ Φ and {(∀R.C)κ | (∃R.C)κ ∈ Φ} ̸⊆ Φ;
• (∃R.C)λ is an ∃-burden of Φ iff (∃R.C)λ is in Φ;
• (≥ 2R)λ is an ≥ 2-burden of Φ iff (≥ 2R)λ is in Φ.

A burden of Φ is any type of burden from above.

Definition 3.5. Let Φ ⊆ cll ∪ clr, C λ be a burden of Φ, and S = {Dl | ⊤ ⊑ D ∈ Tl} ∪ {Dr | ⊤ ⊑ D ∈ Tr}. Then Ψ ⊆ cll ∪ clr is called the Cλ -relief of Φ if

• C = (C1 ⊓ C2)λ and Ψ = {(C1)λ , (C2)λ } ∪ Φ;
• C = (C1 ⊔ C2)λ and either Ψ = Φ ∪ {(C1)λ } or Ψ = Φ ∪ {(C2)λ };
• C = (≤ 1R)λ and Ψ = Φ ∪ {(∀R.C)κ | (∃R.C)κ ∈ Φ};
• C = (∃R.C)λ and Ψ = {C λ }∪{Dκ | (∀R.D)κ ∈ Φ}∪S;
• C = (≥ 2R)λ and Ψ = {Dκ | (∀R.D)κ ∈ Φ} ∪ S.

For all Φ ⊆ cll ∪ clr, we define

Φ(λ) is a shorthand for Φ(l) ∪ Φ(r). In the following the signature of a set of ALCF-concepts S will be of concern. We define sig(S) = ⋃C∈S sig(C).

A biased 〈C0 ⊑ D0, T 〉-tableau (〈C0 ⊑ D0, T 〉-tableau for short) is a directed graph 〈V, E〉, where V is the set of nodes and E ⊆ V × V is the set of edges. We associate three different labels to nodes in V.

1. content : V → 2cll∪clr ,
2. type : V → {and-node, or-node},
3. status : V → {sat, unsat},
4. int : V →ALCF

The function of these labels are explained when they are used. We say that a node g in a tableau contains a clash if and only if either one of the following holds.

• ⊥λ ∈ g.content,
• {Aλ , (¬A)κ } ⊆ g.content,
• {(≤ 1R)λ , (≥ 2R)κ } ⊆ g.content.

The tableau expansion rules given in Figure 1 expand a tableau by making use of the semantics of concepts. A rule is said to be applicable to a node g if and only if its condition is satisfied in g, no rule was applied to g before, and g does not contain a clash. In order to guarantee a finite expansion, we use proxies in the following way. Whenever a rule creates a new node g′ from g, before attaching the edge 〈g, g′ 〉 to E, the tableau is searched for a node g′′ ∈ V such that g′ .content = g′′ .content. If such a g′′ is found then the edge 〈g, g′′ 〉 is added to E and g′ is discarded.

We are interested in deciding T |= C0 ⊑ D0. The tableau algorithm consists of two phases. The first phase starts with the initial 〈C0 ⊑ D0, T 〉-tableau T = 〈{g0}, ∅〉, where g0.content = {(C0)l , ( ˙¬D0)r }∪{El | ⊤ ⊑ E ∈ Tl}∪{Er | ⊤ ⊑ E ∈ Tr}. T is then expanded by repeatedly applying the tableau expansion rules in such a way that if more than one rule is applicable to a node at the same time then the first applicable rule in the list [R⊓, R⊔, R≤1, R∃] is chosen. If R⊔ has been applied to a node g then we set g.type ← or-node, and if some rule other than R⊔ has been applied to g we set g.type ← and-node. The first phase continues as long as some rule is applicable to T.

A 〈C0 ⊑ D0, T 〉-tableau is called complete if and only if it is the output of the first phase of the tableau algorithm.

Let T be a complete 〈C0 ⊑ D0, T 〉-tableau. The purpose of the second phase of the tableau algorithm, i.e., Algorithm 1, is to assign a status to every node in T and to calculate a concept int(g) for every g ∈ V with an unsatisfiable content. To this aim, it uses the interpolant calculation rules which are presented in Figure 2.

Algorithm 1 Second phase of the tableau algorithm

Propagate: Do

• done ← true.
• For every g ∈ V with g.status ̸= unsat:
• if g contains a clash then (i) g.status ← unsat, (ii) apply one of {Cl⊥, Cr⊥, Cll¬ , Crr ¬ , Clr ¬ , Crl ¬ }, one whose condition is satisfied, (iii) done ← false.
• if g.type = and-node and there is some direct successor g′ of g such that g′ .status = unsat then (i) g.status ← unsat, (ii) apply one of {C⊓, Cl̸R ≤1 , Cr̸R ≤1 , ClR ≤1 , CrR ≤1 , Cl̸R ∃ , Cr̸R ∃ , ClR ∃ , CrR ∃ }, one whose condition is satisfied, (iii) done ← false.
• if g.type = or-node and for all direct successors g′ of g we have g′ .status = unsat then (i) g.status ← unsat, (ii) apply one of {Cl⊔ , Cr⊔ }, one whose condition is satisfied, (iii) done ← false.

while done = false.

Assign:

For every g ∈ V with g.status ̸= unsat, g.status ← sat.

Let T = 〈V, E〉 be a complete 〈C0 ⊑ D0, T 〉-tableau which is an output of the second phase. T is said to be open if and only if g0.status = sat; and it is said to be closed if and only if g0.status = unsat. If T is determined to be open after the second phase, then the tableau algorithm returns "T ̸|= C0 ⊑D0", otherwise it returns "T |= C0 ⊑ D0".

The tableau algorithm is a decision procedure for concept subsumption (and satisfiability) in ALCF. Although a complete tableau can be constructed in EXPTIME, the interpolants calculated in the second phase may be double exponentially long. Hence the algorithm runs in 2-EXPTIME. If T |= C0 ⊑ D0 then one can show that int(g0) is the interpolant we are looking for and this is the idea behind the proof of the following theorem.

Theorem3.6. For all ALCF-concepts C,D and all ALCFTBoxes T1, T2 if T1 ∪ T2 |= C ⊑ D then there exists an interpolant of C and D under 〈T1, T2〉 that can be computed in time double exponential in |T1| + |T2| + |C| + |D|.

Now Theorem 3.2, which extends Theorem 3.6 to more logics, can be shown to hold as follows. For ALC, we have that the tableau algorithm for ALCF also decides concept satisfiability w.r.t. a TBox in ALC. Using the fact that in any execution of the algorithm for input in ALC, one can observe that R≤1 will never be applied and the interpolant calculation rules from Figure 2 will never produce concepts of the form ≤ 1R or ≥ 2R. Hence the output interpolant, if there is any, will be in ALC. For more expressive logics, the proof is more involved and requires the following reductions.

Definition 3.7. Let C0 be a SIF-concept and T be a SIFTBox. Then τS(C0, T ) is defined as the ALCFI-TBox T ∪ T ′ , where

[Tobies, 2001] shows that a SIF-concept C0 is satisfiable w.r.t. a SIF-TBox T if and only if C0 is satisfiable w.r.t. the ALCFI-TBox τS(C0, T ). Using this result, one can prove Lemma 3.8.

Lemma 3.8. Let T1, T2 be SIF-TBoxes and let C1,C2 be SIF-concepts. Then

We need a similar reduction to eliminate inverse roles. What is different from the previous reduction is that the signature of the original TBox is slightly modified in the resulting TBox. Let C0 be an ALCFI-concept and let T be an ALCFI-TBox. For each inverse role R- ∈ rol(C0, T ), introduce a new role name Rc which is not in rol(C0, T ). Now let ζ be the total function with domain cl(C0, T ) such that ζ(C) is obtained from C ∈ cl(C0, T ) by replacing every inverse role R- occurring in C by Rc . We extend ζ to T as follows.

Definition 3.9. Let C0 be an ALCFI-concept and let T be an ALCFI-TBox. Then τI(C0, T ) is defined as the ALCFTBox ζ(T )∪T ′ , where T ′ is equal to the union of the following:

• { ˙¬ζ(C) ⊑ ∀R.∃Rc . ˙¬ζ(C) | ∀R-.C ∈ cl(C0, T ), R ∈ NR},
• { ˙¬ζ(C) ⊑ ∀Rc .∃R. ˙¬ζ(C) | ∀R.C ∈ cl(C0, T ), R ∈ NR}.

[Calvanese et al., 2001] show that an ALCFI-concept C0 is satisfiable w.r.t. an ALCFI-TBox T if and only if the ALCF-concept ζ(C0) is satisfiable w.r.t. the ALCF-TBox τI(C0, T ). Using this result, one can prove Lemma 3.10.

Lemma 3.10. Let T1, T2 be ALCFI-TBoxes and let C1,C2 be ALCFI-concepts. Then T1 ∪ T2 |= C1 ⊑ C2 iff

Now the proof of Theorem 3.2 can be summarized as follows. Given L-TBoxes T1, T2 and L-concepts C1,C2, we reduce, by Lemma 3.8 and Lemma 3.10, T1 ∪T2 |= C1 ⊑ C2 to T ′ 1 ∪ T ′ 2 |= C ′1 ⊑ C ′2 , where T ′ 1 , T ′ 2 are ALC- (ALCF) TBoxes and C ′1 , C ′2 are ALC- (ALCF-) concepts. If T ′ 1 ∪ T ′ 2 |= C ′1 ⊑ C ′2 holds then we know by Theorem 3.6 that there is an interpolant I in ALC (ALCF). It is possible to show, by Lemma 3.8 and Lemma 3.10 again, that I yields an interpolant in L.

[Seylan et al., 2009] also present a procedure for computing interpolants in ALC in 2-EXPTIME. This procedure is based on a non-optimal tableau algorithm. An advantage of our algorithm is that it allows us to compute first-order interpolants in EXPTIME by using a succinct representation of concepts assigned to int(g). This is formalized in Theorem 3.11.

Theorem 3.11. Let L be ALC or any of its extensions with constructors from {S, I ,F}. For all L-concepts C, D and L-TBoxes T1, T2, if T1 ∪ T2 |= C ⊑ D then there exists a first-order formula ϕ(x) such that ϕ(x) is equivalent to an interpolant I of C and D under 〈T1, T2〉, sig(ϕ(x)) ⊆ sig(I), and ϕ(x) can be computed in time single exponential in |T1|+ |T2| + |C| + |D|.

The proof of Theorem 3.11 proceeds along the following lines. First we show that the double exponential size of the interpolants is only due to the repeated occurrence of subformulas and that our algorithm yields single exponential size interpolants using a succinct (DAG-shaped as opposed to tree-shaped) concept representation. Next we use a result of Avigad [Avigad, 2003] showing that succinctly represented first-order formulas can be transformed in polynomial time into equivalent ordinary tree-shaped first-order formulas over structures with at least two elements. This allows us to compute single exponential first-order interpolants over structures with at least two elements. After that, we show that single exponential interpolants over structures with one element can be constructed by a reduction to propositional logic. By combining the interpolants obtained via these two methods, we finally obtain the desired single exponential first-order interpolant over arbitrary structures.

4 Results on Beth Definability

In this section, we present the main technical contributions of the paper. We start by a positive result on BP which is a direct application of the interpolation theorem, i.e., Theorem 3.2.

Theorem 4.1 (BP). Let L be ALC or any of its extensions with constructors from {S, I ,F}. Then for all L-concepts C, all L-TBoxes T , and all signatures Σ ⊆ sig(C, T ), if C is implicitly definable from Σ under T then C is explicitly definable from Σ under T , and the explicit definition of C can be computed in time double exponential in |T | + |C|.

Proof. Let L be one of the DLs stated in the theorem, C be an L-concept, T be an L-TBox, and Σ ⊆ sig(C, T ) such that C is implicitly definable from Σ under T . We have that T ∪ ˜ T |= C ≡ ˜ C by Lemma 2.3. Now by Theorem 3.2, there is an interpolant I of C and ˜ C under 〈T , ˜ T 〉 that can be computed in time double exponential in |T |+| ˜ T |+|C|+| ˜ C|. Since it is an interpolant, sig(I) ⊆ sig(C, T ) ∩ sig( ˜ C, ˜ T ) = Σ, and both (a) T ∪ ˜ T |= C ⊑ I and (b) T ∪ ˜ T |= I ⊑ ˜ C. By (b) and T ∪ ˜ T |= ˜ C ⊑ C, we have T ∪ ˜ T |= I ⊑ C, from which T ∪ ˜ T |= C ≡ I follows by (a). From the structure of ˜ T , it now straightforwardly follows that T |= C ≡ I.

As for the time needed to compute I, observe that |T | + | ˜ T | + |C| + | ˜ C| = 2 · (|T | + |C|). Hence I can be computed in time double exponential in |T | + |C|.

The proof of Theorem 4.1 uses Theorem 3.2. Similarly, if we use Theorem 3.11 instead, we can show that first-order explicit definitions of implicitly defined concepts can be computed in EXPTIME. Note that Theorem 4.1 also establishes a double exponential upper bound on the size explicit definitions in the considered logics. This upper bound is optimal because explicit definitions in L can be inherently very big.

Theorem 4.2 (Explicit definition lower bound). For every n ∈ N, there is an ALC-concept Cn and an ALC-TBox Tn such that |Tn| and |Cn| are polynomial in n, Cn is implicitly definable from some Σ ⊆ sig(Cn, Tn) under Tn, and the smallest explicit definition of Cn is double exponentially long in n.

Proof. Let A1, . . . , An be concept names and let R, S be role names. For k ∈ {1, . . . , n},

• let Xk = ¬A1 ⊓ . . . ⊓ ¬Ak-1 ⊓ Ak and
• let Yk = A1 ⊓ . . . ⊓ Ak-1 ⊓ ¬Ak.

Note that Xk and Yk are just abbreviations, not concept names. Now define the ALC-TBox Tn as follows.

• ¬A1 ⊓ . . . ⊓ ¬An ⊑ ∀R.⊥ ⊓ ∀S.⊥
• A1 ⊔ . . . ⊔ An ⊑ ∃R.⊤ ⊔ ∃S.⊤

• For k = 1 . . . n and σ ∈ {R, S},

Note that |Tn| is polynomial in n and that Tn is satisfiable. If I is a model of Tn, we have for every s ∈ ΔI and every i ∈ {1, . . . , n}, either s ∈ AIi or s ∈ (¬Ai)I by the virtue of I being an interpretation. Therefore every s ∈ ΔI is assigned a unique number between 0, . . . , 2n - 1 that is expressed in terms of concept names A1, . . . ,An. For convenience, we will write e.g., 5 for A3 ⊓ ¬A2 ⊓ A1 when n = 3.

Now define concepts C0 . . . C2n-1 as follows.

Intuitively, Ci has the shape of a binary tree (due to role names R, S) and the height of the tree is exponential in i. This implies |C2n-1| is double exponential in n. Moreover, we have for every i ∈ {0, . . . , 2n - 1}, Tn |= i ≡ Ci. This means i is explicitly (and thus by Proposition 2.7 implicitly) definable from {R, S} under Tn. The rest of the proof goes on to show that there is no shorter concept than Ci that is an explicit definition of i from {R, S} under Tn. In order to show this, we use the path-set construction from [Lutz, 2006].

In conclusion, Tn |= 2n - 1 ≡ C2n-1, |C2n-1| is double exponential in n, and there is no shorter concept C than C2n-1 that is an explicit definition of 2n - 1 from {R, S} under Tn. Hence the lower bound follows.

Note that by the role disjunction constructor which is not present in ALC, one could get away with a single exponential explicit definition. Also note that the lower bound argument works for CBP as well. In fact, one just seeks an explicit definition over Σ = ∅ in this case.

Note that by Theorems 4.2 and 4.1, we have that implicit definitions using general TBoxes are double exponentially more succinct than acyclic concept definitions. This closes the open problem of [ten Cate et al., 2006] about the size of explicit definitions. Moreover, the same theorems also establish an exact bound on the size of equivalent rewritings of concept queries as considered in [Seylan et al., 2009].

By the following theorem, we have that BP fails in the considered logics having H. This shows that BP is indeed a stronger property than CBP because the same logics have CBP [ten Cate et al., 2006] (cf. Section 2). The theorem also implies that the claim in [Seylan et al., 2010] stating that ALCH and its extensions with S and/or I have BP is incorrect.

Theorem 4.3. Let L be ALCH or any of its extensions with constructors from {S, I , F}. Then L does not have BP.

Proof. Consider the ALCH-TBox T which consists of

It is easy to see that T is satisfiable. For an interpretation I, define XI = {s ∈ ΔI | ∃t ∈ ΔI .〈s, t〉 ∈ RI 1 ∩ RI 2 }. We have that for all models I of T , (∃S.⊤)I = XI. This implies that ∃S.⊤ is implicitly definable from Σ = {R1, R2} under T .

We now show that there is no ALCFI-concept C such that sig(C) ⊆ Σ and T |= ∃S.⊤ ≡ C. To this aim, let I = 〈ΔI , ·I 〉 be the interpretation where

• ΔI = {s, t},
• RI 1 = RI 2 = SI = {〈s, t〉};
• BI = ∅, for all B ∈ NC.

Let J = 〈ΔJ , ·J 〉 be the interpretation where

• ΔJ = {w, v, a, b},
• RJ 1 = {〈w, a〉, 〈v, b〉}, RJ 2 = {〈w, b〉, 〈v, a〉}, SJ = ∅;
• AJ = {a} and for all B ∈ (NC \ {A}), BJ = ∅.

I and J are models of T . Using a bisimulation argument, one can show that s and w satisfy the same ALCFIconcepts formulated over Σ. But clearly, s ∈ (∃S.⊤)I and w ̸∈ (∃S.⊤)J .

Now let L be as stated in the theorem, i.e., it is either ALCH or any of its extension with constructors from {S, I ,F}. Since the concept language of SHIF is same as the concept language of ALCFI and no transitive role occurs in T , we have that ∃S.⊤ is not explicitly definable from Σ under T in SHIF. But then there is no explicit definition in L . Hence L does not have BP.

As discussed in Section 2, it also makes sense to study BPF. However in the considered logics lacking FMP, BPF fails.

Theorem 4.4. Let L be ALCFI or any of its extensions with constructors from {S, H}. Then L does not have BPF.

Proof. Let A,B,X be concept names and let R be a role name. Consider the ALCFI-TBox T which consists of the following.

It is easy to see that the concept A ⊓ B is finitely satisfiable w.r.t. T , i.e., there is some finite model I of T such that (A ⊓ B)I ̸= ∅. In fact, we provide two such models In and Jn later on in the proof.

Now for all interpretations, define

where (RI )+ is the transitive closure of RI . We claim that for all finite models I of T , we have (A ⊓ B)I = YI. In particular, this implies A ⊓ B is f-implicitly definable from Σ = {R, A} under T .

For some n ∈ N, we will define in the following two interpretations In, Jn. Let s0, . . . , s2n+1 be all distinct elements and define In = 〈{s0, . . . , s2n+1}, ·In 〉 to be the interpretation which consists of the R-cycle 1 s0, s1, . . . , s2n+1, s0, where AIn = {s0}, XIn = {s0}, and BIn = ΔIn ; and define Jn = 〈{s0, . . . , s2n+1} \ {sn+1}, ·Jn 〉 to be the interpretation which consists of the R-path

where AJn = {s0}, XJn = {s0}, and BJn = ∅.

Observe that In and Jn are (finite) models of T , and Jn is the subinstance of In where the element sn+1 is removed.

Claim 4.5. For every ALCFI-concept C such that sig(C) ⊆ Σ = {R,A} and md(C) ≤ n, where md(C) is the modal depth of C, it holds that s0 ∈ C I iff s0 ∈ C J .

The claim follows from the fact that the subinstances of In and Jn containing all nodes at distance at most n from s0 are isomorphic. Now we have that s0 ∈ (A ⊓ B)I and s0 ̸∈ (A ⊓ B)J . But by the previous claim, s0 in I satisfies exactly the same concepts as s0 in J that are formulated over Σ and with modal depth ≤ n. Since we can come up with such witness models for every n, there exists no ALCFIconcept C such that sig(C) ⊆ Σ and T |=f A ⊓ B ≡ C. This means A ⊓ B is not f-explicitly definable from Σ under T . Hence ALCFI does not have BPF.

Let L be any proper extension of ALCFI with constructors from {S,H}. Since T and A ⊓ B are respectively an L-TBox and an L-concept, and the concept languages of ALCFI and L are the same, we have that L does not have BPF.

5 Discussion

Qualified number restrictions, denoted by Q in the language, is a generalization of F. Extending our upper bound results on the size of explicit definitions to ALCQ and ALCQI appears to be difficult. This is because of the unavailability of a natural and optimal tableau algorithm for these logics. We leave as another open problem the lower bound on the size of the first-order explicit definition given that a concept is implicitly defined under a TBox.