Uniform and Modular Sequent Systems for
Description Logics
Tim Lyon1 , Jonas Karge1
1
 Computational Logic Group, Institute of Artificial Intelligence, Technische Universität Dresden, 01062 Dresden,
Germany


                                         Abstract
                                         We introduce a framework that allows for the construction of sequent systems for expressive description
                                         logics extending 𝒜ℒ𝒞. Our framework not only covers a wide array of common description logics, but
                                         also allows for sequent systems to be obtained for extensions of description logics with special formulae
                                         that we call role relational axioms. All sequent systems are sound, complete, and possess favorable
                                         properties such as height-preserving admissibility of common structural rules and height-preserving
                                         invertibility of rules.

                                         Keywords
                                         Sequent Calculus, Description Logics, Proof theory




1. Introduction
Description logics (DLs) consist of an assortment of knowledge representation languages used
to structure and represent knowledge in an unequivocal and perspicuous manner. In DLs,
knowledge is represented by means of knowledge bases (KBs), i.e. collections of expressions
involving concepts and roles. KBs contain explicit knowledge of a particular domain of interest,
and by means of logical consequence, implicit knowledge may be derived, thus giving rise to a
need for logical tools to extract information. In addition, it is reasonable to request that such
tools be automatable, i.e. it is not only desirable to develop tools that have the potential of
deriving information, but which give definitive answers to a problem by means of an algorithm.
It is also worthwhile to possess tools that allow one to constructively prove (meta-)logical
properties of DLs (e.g. concept interpolation, or re-writings of concepts and TBoxes), and which
are applicable to a wide array of DLs, regardless of their idiosyncrasies.
   Such tools—meeting the above demands—are capable of being developed on the basis of proof
theory. Indeed, various DLs have been equipped with tableau-based proof-search algorithms [1,
2, 3, 4, 5, 6], resolution-based algorithms [7, 8, 9], or consequence-based algorithms [10, 11],
to solve certain reasoning tasks. These works highlight and demonstrate the success of proof-
theoretic methods in application to problems of description logics. Therefore, a proof-theoretic
formalism that yields proof systems for a significant number of DLs on demand is desirable.

  DL 2022: 35th International Workshop on Description Logics, August 7–10, 2022, Haifa, Israel
" timothy_stephen.lyon@tu-dresden.de (T. Lyon); jonas.karge@tu-dresden.de (J. Karge)
~ https://iccl.inf.tu-dresden.de/web/Tim_Lyon (T. Lyon); https://iccl.inf.tu-dresden.de/web/Jonas_Karge (J. Karge)
 0000-0003-3214-0828 (T. Lyon); 0000-0002-8296-1010 (J. Karge)
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
Hence, the intent of this paper is to propose a uniform and modular framework for generating
proof systems—namely, sequent systems—for a large class of DLs, in the style of [12]. That is, the
purpose of this paper is to provide a general recipe for constructing sequent systems for DLs.
   Although work has been done on supplying sequent systems for DLs [13, 14, 15, 16], the
systems have been constructed for a relatively narrow set. The distinguishing feature of the
present paper is that we provide a formalism for generating sound and complete sequent
systems for a sizable class of expressive DLs. Indeed, our work not only covers 𝒜ℒ𝒞 and its
prominent extensions (e.g. 𝒮ℋℐ𝒪𝒬 and the DL 𝒮ℛ𝒪ℐ𝒬 that underlies OWL 2 [17]), but
allows for extensions of expressive DLs with axioms we refer to as role relational axioms (RRAs).
Such axioms express properties of, and relationships between, roles. For instance, Trans(𝑟) and
Dis(𝑟, 𝑠), which express that the role 𝑟 is transitive and the roles 𝑟 and 𝑠 are disjoint, respectively,
are defined to be instances of role relational axioms. It will be seen that the sequent formalism
we provide is both uniform, covering many DLs, and modular, meaning that a sequent system
for one DL is straightforwardly transformable into a sequent system for another DL by the
addition or deletion of inference rules. Due to space constraints we leave the discussion of
complexity related issues as well as proof-search algorithms up to future work.
   The paper is organized as follows: In (Section 2), we introduce expressive DLs, including
their semantics and features of their knowledge bases. In (Section 3), we introduce a sequent
calculus for the attributive concept language with complements 𝒜ℒ𝒞 [6], and define extensions
for other expressive DLs along with the addition of rules for RRAs. We argue that all of our
sequent calculi are sound, complete, and possess standard properties (e.g. invertibility of rules
and admissibility of contraction).


2. Description Logics
In this section, we present the family of expressive description logics (DLs) (cf. [18]) that will
be considered in this paper. This class of logics is obtained by extending 𝒜ℒ𝒞. We first define
𝒜ℒ𝒞 and its associated semantics, and then discuss extensions thereof.

2.1. Preliminaries and 𝒜ℒ𝒞
𝒜ℒ𝒞, and DLs more generally, are defined relative to a vocabulary 𝒱 = (R, C, I) the compo-
nents of which are taken to be pairwise disjoint, countable sets. Each set contains primitive
symbols dedicated to a particular purpose: the set R contains role names used to denote binary
relations, the set C contains concept names used to denote classes of entities, and the set I
contains individuals used to denote particular entities. We use 𝑟, 𝑠, . . . (potentially annotated)
to denote role names, 𝐶, 𝐷, . . . (potentially annotated) to denote concept names, and 𝑎, 𝑏, . . .
(potentially annotated) to denote individuals. For 𝒜ℒ𝒞, complex concepts are built from role
and concept names as dictated by the following BNF grammar:

                      𝑃 ::= 𝐶 | ⊥ | ⊤ | ¬𝑃 | 𝑃 ⊔ 𝑃 | 𝑃 ⊓ 𝑃 | ∃𝑟.𝑃 | ∀𝑟.𝑃

where 𝐶 ∈ C and 𝑟 ∈ R. We use the symbols 𝑃 , 𝑄, . . . (potentially annotated) to denote
complex concepts. We interpret complex concepts and roles as follows:
Definition 1 (Interpretation [1]). An interpretation ℐ = (Δℐ , ·ℐ ) contains a non-empty set
Δℐ , called the domain, and a map ·ℐ such that for every 𝐶 ∈ C, 𝐶 ℐ ⊆ Δℐ ; for every 𝑟 ∈ R,
𝑟ℐ ⊆ Δℐ × Δℐ ; and for every 𝑎 ∈ I, 𝑎ℐ ∈ Δℐ . The map ·ℐ is extended to complex concept names
as follows:
  ⊤ℐ := Δℐ ; ⊥ℐ := ∅; 𝐶 ⊔ 𝐷ℐ := 𝐶 ℐ ∪ 𝐷ℐ ; 𝐶 ⊓ 𝐷ℐ := 𝐶 ℐ ∩ 𝐷ℐ ;
  ∃𝑟.𝐶 ℐ := {𝑎 ∈ Δℐ | there exists 𝑏 ∈ Δℐ s.t. (𝑎, 𝑏) ∈ 𝑟ℐ and 𝑏 ∈ 𝐶 ℐ .};
  ∀𝑟.𝐶 ℐ := {𝑎 ∈ Δℐ | for each 𝑏 ∈ Δℐ , if (𝑎, 𝑏) ∈ 𝑟ℐ , then 𝑏 ∈ 𝐶 ℐ .}.

   As is standard for DLs, we collect specific formulae into TBoxes to specify certain properties
of, and relationships between, concepts and roles. For 𝒜ℒ𝒞, a TBox is a finite set of general
concept inclusions (GCIs), which are formulae of the form 𝑃 ⊑ 𝑄, where 𝑃 and 𝑄 are complex
concepts. As explained in the following section (Section 2.2), we allow for a larger variety of
formulae in TBoxes for DLs more expressive than 𝒜ℒ𝒞.
   Typically, for DLs, assertional knowledge is represented by formulae that state whether or
not an individual or pair of individuals participate in a concept or role. Such formulae, which
are referred to as assertions, comprise the ABox. For 𝒜ℒ𝒞, the ABox contains a finite number of
concept assertions of the form 𝑎 : 𝑃 (with 𝑃 a complex concept and 𝑎 ∈ I) and a finite number
of role assertions of the form 𝑟(𝑎, 𝑏) (with 𝑟 ∈ R and 𝑎, 𝑏 ∈ I). A knowledge base (KB) 𝒦 is
defined to be a pair consisting of a TBox 𝒯 and an ABox 𝒜, i.e. 𝒦 = (𝒯 , 𝒜). Let us now define
how interpretations can be extended to the formulae of TBoxes, ABoxes, and therefore, to KBs.

Definition 2 (Model [1]). An interpretation ℐ = (Δℐ , ·ℐ ) satisfies a GCI 𝑃 ⊑ 𝑄, written
ℐ |= 𝑃 ⊑ 𝑄, iff 𝑃 ℐ ⊆ 𝑄ℐ ; a concept assertion 𝑎 : 𝑃 , written ℐ |= 𝑎 : 𝑃 , iff 𝑎ℐ ∈ 𝑃 ℐ ; and a role
assertion 𝑟(𝑎, 𝑏), written ℐ |= 𝑟(𝑎, 𝑏), iff (𝑎ℐ , 𝑏ℐ ) ∈ 𝑟ℐ . We say that an intepretation ℐ is a model
of a TBox 𝒯 (ABox 𝒜) iff it satisfies all formulae in 𝒯 (all formulae in 𝒜, resp.). An interpretation
ℐ is a model of a KB 𝒦 = (𝒯 , 𝒜) iff it is a model of 𝒯 and 𝒜.

2.2. Extensions of 𝒜ℒ𝒞
The sequent systems provided in the subsequent section allow for a sizable number of DLs to be
captured proof-theoretically. We focus our attention on presenting well-known extensions of
𝒜ℒ𝒞, making use of the well-established naming convention for DLs to do so. Also, we define
how new formulae within extensions are satisfied by a given interpretation ℐ = (Δℐ , ·ℐ ).
   𝒮 Prepending the name of a DL with 𝒮 (rather than 𝒜ℒ𝒞) indicates that a TBox is permitted
to include transitivity axioms of the form Trans(𝑟), or equivalently, axioms of the form 𝑟 ∘ 𝑟 ⊑ 𝑟,
where the composition operation ∘ is interpreted accordingly (with 𝑟, 𝑠 ∈ R): (𝑟 ∘ 𝑠)ℐ :=

           {(𝑎, 𝑏) ∈ Δℐ × Δℐ | there exists a 𝑐 ∈ Δℐ s.t. (𝑎, 𝑐) ∈ 𝑟ℐ and (𝑐, 𝑏) ∈ 𝑠ℐ .}

ℐ satisfies Trans(𝑟), written ℐ |= Trans(𝑟), iff 𝑟ℐ is transitive.1
  ℋ Including an ℋ in the name of a DL (e.g. 𝒜ℒ𝒞ℋ) indicates that simple role inclusions
axioms (RIAs) of the form 𝑟 ⊑ 𝑠 with 𝑟, 𝑠 ∈ R may be included in a TBox. ℐ satisfies 𝑟 ⊑ 𝑠,
written ℐ |= 𝑟 ⊑ 𝑠, iff 𝑟ℐ ⊆ 𝑠ℐ .
    1 ℐ
    𝑟 is transitive iff for all 𝑎, 𝑏, 𝑐 ∈ Δℐ , if (𝑎, 𝑏), (𝑏, 𝑐) ∈ 𝑟ℐ , then (𝑎, 𝑐) ∈ 𝑟ℐ .
   𝒮ℛ The most notable feature of DLs whose names are prepended with 𝒮ℛ is that such logics
allow for complex role inclusion axioms (CRIAs) of the form 𝑟1 ∘ · · · ∘ 𝑟𝑛 ⊑ 𝑟 to be included in a
TBox.2 Additionally, DLs from the 𝒮ℛ family may include reflexivity axioms of the form Refl(𝑟),
irreflexivity axioms of the form Irr(𝑟), asymmetry axioms of the form Asy(𝑟), or disjointness
axioms of the form Dis(𝑟, 𝑠).3

     • ℐ satisfies 𝑟1 ∘ · · · ∘ 𝑟𝑛 ⊑ 𝑟, written ℐ |= 𝑟1 ∘ · · · ∘ 𝑟𝑛 ⊑ 𝑟, iff 𝑟1 ℐ ∘ · · · ∘ 𝑟𝑛 ℐ ⊆ 𝑟ℐ ;
     • ℐ satisfies Refl(𝑟), written ℐ |= Refl(𝑟), iff 𝑟ℐ is reflexive;
     • ℐ satisfies Irr(𝑟), written ℐ |= Irr(𝑟), iff 𝑟ℐ is irreflexive;
     • ℐ satisfies Asy(𝑟), written ℐ |= Asy(𝑟), iff 𝑟ℐ is asymmetric;
     • ℐ satisfies Dis(𝑟, 𝑠), written ℐ |= Dis(𝑟, 𝑠), iff 𝑟ℐ and 𝑠ℐ are disjoint.

  𝒪 Including an 𝒪 in the name of a DL indicates that the set C of concept names includes
nominals of the form {𝑎}, for each 𝑎 ∈ I. We interpret nominals accordingly: {𝑎}ℐ := {𝑎ℐ }.
   ℐ Including an ℐ in the name of a DL indicates that the set R includes inverse roles of the
                                                                    ℐ
form 𝑟− , for each 𝑟 ∈ R. We interpret inverse roles accordingly: 𝑟− := {(𝑏, 𝑎) | (𝑎, 𝑏) ∈ 𝑟ℐ }.
  ℱ An ℱ in the name of a DL indicates that a TBox may include functionality axioms of the
form Funct(𝑟) for 𝑟 ∈ R. ℐ satisfies Funct(𝑟), written ℐ |= Funct(𝑟), iff 𝑟ℐ is functional.4
   𝒩 The symbol 𝒩 is included in the name of a DL when it includes unqualified number
restrictions of the form (⩽ 𝑛𝑟.⊤) or (⩾ 𝑛𝑟.⊤) with 𝑟 ∈ R among its concepts. We interpret
unqualified number restrictions as follows:5 (⩽ 𝑛𝑟.⊤)ℐ := {𝑎 ∈ Δℐ | #{𝑏 | (𝑎, 𝑏) ∈ 𝑟ℐ } ≤ 𝑛}
and (⩾ 𝑛𝑟.⊤)ℐ := {𝑎 ∈ Δℐ | #{𝑏 | (𝑎, 𝑏) ∈ 𝑟ℐ } ≥ 𝑛}.
  𝒬 We use 𝒬 to indicate that a DL includes qualified number restrictions of the form (⩽ 𝑛𝑟.𝑃 )
or (⩾ 𝑛𝑟.𝑃 ) with 𝑟 ∈ R among its concepts. We interpret qualified number restrictions
accordingly: (⩽ 𝑛𝑟.𝑃 )ℐ := {𝑎 ∈ Δℐ | #{𝑏 | (𝑎, 𝑏) ∈ 𝑟ℐ and 𝑏 : 𝑃 } ≤ 𝑛} and (⩾ 𝑛𝑟.𝑃 )ℐ :=
{𝑎 ∈ Δℐ | #{𝑏 | (𝑎, 𝑏) ∈ 𝑟ℐ and 𝑏 : 𝑃 } ≥ 𝑛}.
   Other Extensions We may also extend 𝒜ℒ𝒞 by permitting the inclusion of equality or in-
equality axioms of the form 𝑎 ≈ 𝑏 and 𝑎 ̸≈ 𝑏 (resp.) in a TBox, by permitting negated role
assertions of the form ¬𝑟(𝑎, 𝑏) in an ABox, by allowing for the universal role U to be included
in R (interpreted Uℐ := Δℐ × Δℐ ), or by allowing the complex concept ∃𝑟.Self for 𝑟 ∈ R
(interpreted (∃𝑟.Self)ℐ := {𝑎 | (𝑎, 𝑎) ∈ 𝑟ℐ }). The semantics of (in)equalities and negated role
assertions is as follows:
     • ℐ satisfies 𝑎 ≈ 𝑏, written ℐ |= 𝑎 ≈ 𝑏, iff 𝑎ℐ = 𝑏ℐ ;
     • ℐ satisfies 𝑎 ̸≈ 𝑏, written ℐ |= 𝑎 ̸≈ 𝑏, iff 𝑎ℐ ̸= 𝑏ℐ ;
     • ℐ satisfies ¬𝑟(𝑎, 𝑏), written ℐ |= ¬𝑟(𝑎, 𝑏), iff (𝑎, 𝑏) ̸∈ 𝑟ℐ .
    2
       We note that syntactic conditions are usually imposed on the form of CRIAs in order to ensure the decidability
of the resulting DL (e.g., see [1, 3]).
     3
       Each property is defined as follows: (i) 𝑟ℐ is reflexive iff for each 𝑎 ∈ Δℐ , (𝑎, 𝑎) ∈ 𝑟ℐ , (ii) 𝑟ℐ is irreflexive iff
for each 𝑎 ∈ Δℐ , (𝑎, 𝑎) ̸∈ 𝑟ℐ , (iii) 𝑟ℐ is asymmetric iff for each 𝑎, 𝑏 ∈ Δℐ , if (𝑎, 𝑏) ∈ 𝑟ℐ , then (𝑏, 𝑎) ̸∈ 𝑟ℐ , and (iv)
𝑟ℐ and 𝑠ℐ are disjoint iff 𝑟ℐ ∩ 𝑠ℐ = ∅.
     4 ℐ
       𝑟 is functional iff for all 𝑎, 𝑏, 𝑐 ∈ Δℐ , if (𝑎, 𝑏), (𝑎, 𝑐) ∈ 𝑟ℐ , then 𝑏 = 𝑐.
     5
       We use #𝑆 for a set 𝑆 to denote the cardinality of the set.
3. Sequent Systems
Our proof systems consist of inference rules that manipulate sequents of the form Λ := R , Σ ⊢
Π, Q , where R , Σ is referred to as the antecedent and Π, Q is referred to as the consequent. Note
that Σ, Π, R , and Q are taken to be (potentially empty) multisets of DL formulae. Σ and Π are
multisets of formulae of the form 𝑎 : 𝑃 , called internal formulae (IFs), where 𝑎 ranges over the
set of individuals I, and 𝑃 is a complex concept generated via the following grammar in BNF:

  𝑃 ::= 𝐶 | ⊥ | ⊤ | ¬𝑃 | 𝑃 ⊔ 𝑃 | 𝑃 ⊓ 𝑃 | ∃𝑟.𝑃 | ∀𝑟.𝑃 | {𝑎} | (⩽ 𝑛𝑟.𝑃 ) | (⩾ 𝑛𝑟.𝑃 ) | ∃𝑟.Self

with 𝐶 ∈ C, 𝑟 ∈ R (which is potentially an inverse role 𝑠− or the universal role U), 𝑎 ∈ I,
and 𝑛 ∈ N. R and Q consist of formulae generated via the following grammar in BNF, and are
referred to as external formulae (EFs).

         𝐹 ::= 𝑃 ⊑ 𝑄 | 𝑟(𝑎, 𝑏) | ¬𝑟(𝑎, 𝑏) | Rel(𝑟1 , . . . , 𝑟𝑛 ) | 𝑟1 ∘ · · · ∘ 𝑟𝑛 ⊑ 𝑟 | 𝑎 ≈ 𝑏 | 𝑎 ̸≈ 𝑏

where 𝑃 and 𝑄 are complex concepts, 𝑎, 𝑏 ∈ I, 𝑟1 , . . . , 𝑟𝑛 , 𝑟 ∈ R (and are potentially inverse
roles 𝑠− or the universal role U), and for each arity 𝑛 ∈ N, the relation name Rel ranges
over a countable set of 𝑛-ary relation names. We note that transitivity axioms Trans(𝑟), re-
flexivity axioms Refl(𝑟), irreflexivity axioms Irr(𝑟), asymmetry axioms Asy(𝑟), disjointness
axioms Dis(𝑟, 𝑠), and functionality axioms Funct(𝑟) are all instances of formulae of the form
Rel(𝑟1 , . . . , 𝑟𝑛 ), which we refer to as role relational axioms (RRAs). We use 𝐹 , 𝐺, . . . to denote
EFs defined by the grammar above. We distinguish EFs from IFs as EFs are those formulae
which govern reasoning with complex concepts, i.e. of reasoning with IFs.
   When supplying a calculus for a particular DL, we assume that the EFs and IFs occurring
within sequents are restricted to those formulae allowed by the DL language under consideration.
For example, for 𝒜ℒ𝒞, we omit the inclusion of nominals, (un)qualified number restrictions,
and ∃𝑟.Self from occurring in IFs since such concepts are not included in 𝒜ℒ𝒞’s language.

3.1. The System G3𝒜ℒ𝒞 and Descriptive Definitional Rules
We now present our calculus G3𝒜ℒ𝒞 for the DL 𝒜ℒ𝒞 as well as define extensions of the calculus
with descriptive definitional rules (DDRs).6 DDRs introduce RRAs into either the antecedent
or consequent of a sequent, and thus provide our calculus with the capacity to handle such
formulae. We discuss DDRs in detail below, and mention the DDRs that introduce widely-used
RRAs such as transitivity axioms and reflexivity axioms. The calculus G3𝒜ℒ𝒞 is obtained by
transforming the semantics of 𝒜ℒ𝒞 into inference rules (cf. [12, 20, 21]), and is displayed in
Figure 1. Note that in the (𝑖𝑑R ) rule we stipulate that 𝐹 must be of the form 𝑟(𝑎, 𝑏) or 𝑎 ≈ 𝑏.
We refer to the principal formulae of a rule as those formulae which are explicitly presented in
the conclusion (e.g. 𝑎 : 𝑃 ⊔ 𝑄 is the principal formula of (⊔𝑙 )), and to the multisets R , Σ, Π,
and Q as contexts. Furthermore, we note that proofs/derivations are constructed by successively
applying inference rules to initial rules/sequents, i.e. rules without premises (e.g. (𝑖𝑑C ), (𝑖𝑑R ),
(⊥𝑙 ), and (⊤𝑟 )), and the height of a proof is defined to be the longest sequence of sequents from
the conclusion of the proof to an initial rule (cf. [12]).
    6
        For a discussion of G3-style calculi, along with the G1 and G2 variants, see [19, Section 80].
                                                   (𝑖𝑑C )                         (𝑖𝑑R )
                     R , Σ, 𝑎 : 𝐶 ⊢ 𝑎 : 𝐶, Π, Q              R , Σ, 𝐹 ⊢ 𝐹, Π, Q

                                 (⊥𝑙 )    R , Σ ⊢ 𝑎 : ⊥, Π, Q             R , Σ, 𝑎 : ⊤ ⊢ Π, Q
          R , Σ, 𝑎 : ⊥ ⊢ Π, Q                                 (⊥𝑟 )                           (⊤𝑙 )
                                              R , Σ ⊢ Π, Q                    R , Σ ⊢ Π, Q

                                (⊤𝑟 )     R , Σ ⊢ 𝑎 : 𝑃, Π, Q             R , Σ, 𝑎 : 𝑃 ⊢ Π, Q
        R , Σ ⊢ 𝑎 : ⊤, Π, Q                                   (¬𝑙 )                            (¬𝑟 )
                                         R , Σ, 𝑎 : ¬𝑃 ⊢ Π, Q             R , Σ ⊢ 𝑎 : ¬𝑃, Π, Q

         R , Σ, 𝑎 : 𝑃 ⊢ Π, Q       R , Σ, 𝑎 : 𝑄 ⊢ Π, Q              R , Σ ⊢ 𝑎 : 𝑃, 𝑎 : 𝑄, Π, Q
                                                       (⊔𝑙 )                                   (⊔𝑟 )
                    R , Σ, 𝑎 : 𝑃 ⊔ 𝑄 ⊢ Π, Q                         R , Σ ⊢ 𝑎 : 𝑃 ⊔ 𝑄, Π, Q

         R , Σ, 𝑎 : 𝑃, 𝑎 : 𝑄 ⊢ Π, Q             R , Σ ⊢ 𝑎 : 𝑃, Π, Q      R , Σ ⊢ 𝑎 : 𝑄, Π, Q
                                    (⊓𝑙 )                                                    (⊓𝑟 )
         R , Σ, 𝑎 : 𝑃 ⊓ 𝑄 ⊢ Π, Q                          R , Σ ⊢ 𝑎 : 𝑃 ⊓ 𝑄, Π, Q

              R , 𝑃 ⊑ 𝑄, 𝑎 : 𝑃, 𝑎 : 𝑄, Σ ⊢ Π, Q               R , Σ, 𝑏 : 𝑃 ⊢ 𝑏 : 𝑄, Π, Q
                                                (⊑𝑙 )                                    (⊑𝑟 )†
                  R , 𝑃 ⊑ 𝑄, 𝑎 : 𝑃, Σ ⊢ Π, Q                    R , Σ ⊢ 𝑃 ⊑ 𝑄, Π, Q

             R , Σ, 𝑟(𝑎, 𝑏), 𝑏 : 𝑃 ⊢ Π, Q            R , Σ, 𝑟(𝑎, 𝑏) ⊢ 𝑎 : ∃𝑟.𝑃, 𝑏 : 𝑃, Π, Q
                                          (∃𝑙 )†                                            (∃𝑟 )
               R , Σ, 𝑎 : ∃𝑟.𝑃 ⊢ Π, Q                    R , Σ, 𝑟(𝑎, 𝑏) ⊢ 𝑎 : ∃𝑟.𝑃, Π, Q

             R , Σ, 𝑟(𝑎, 𝑏), 𝑎 : ∀𝑟.𝑃, 𝑏 : 𝑃 ⊢ Π, Q           R , Σ, 𝑟(𝑎, 𝑏) ⊢ 𝑏 : 𝑃, Π, Q
                                                    (∀𝑙 )                                  (∀𝑟 )†
                 R , Σ, 𝑟(𝑎, 𝑏), 𝑎 : ∀𝑟.𝑃 ⊢ Π, Q                R , Σ ⊢ 𝑎 : ∀𝑟.𝑃, Π, Q

Figure 1: G3𝒜ℒ𝒞. † stipulates that the rule can be applied only if 𝑏 is an eigenvariable, i.e. 𝑏 does not
occur in the conclusion of the rule.


  DDRs are rules which are equivalent to, and obtained from, descriptive definitions. Descriptive
definitions define properties of, and relationships between, roles; i.e. they define the necessary
and sufficient conditions for which an RRA obtains. For instance, the formula Trans(𝑟) ↔
∀𝑎∀𝑏∀𝑐(𝑟(𝑎, 𝑏) ∧ 𝑟(𝑏, 𝑐) → 𝑟(𝑎, 𝑐)) defines the RRA Trans(𝑟) for the role 𝑟.
Definition 3 (Descriptive Definition). A descriptive definition is a formula of the form:
                      Rel(𝑟1 , . . . , 𝑟𝑙 ) ↔ ∀𝑎
                                               ⃗ (𝐹1 ∧ · · · ∧ 𝐹𝑛 → 𝐺1 ∨ · · · ∨ 𝐺𝑘 )
such that each 𝐹𝑖 and 𝐺𝑗 is an EF of the form 𝑟(𝑎, 𝑏) or 𝑎 ≈ 𝑏, the individuals ⃗𝑎 := 𝑎1 , . . . , 𝑎𝑚
occur within 𝐹1 ∧ · · · ∧ 𝐹𝑛 (which is ⊤ if the conjunction is empty) and 𝐺1 ∨ · · · ∨ 𝐺𝑘 (which
is ⊥ if the disjunction is empty), and where the definiens (to the right of the bi-conditional) only
makes reference to the roles 𝑟1 , . . ., 𝑟𝑙 and/or equalities of the form 𝑎 ≈ 𝑏 (for 𝑎 and 𝑏 in ⃗𝑎).
   Each descriptive definition of the above form can be transformed into a pair of left and right
introduction rules (introducing the RRA Rel(𝑟1 , . . . , 𝑟𝑙 )) as shown below:
                   {︁                                                         }︁
                     R , Rel(𝑟1 , . . . , 𝑟𝑙 ), 𝐹 , 𝐺𝑗 , Σ ⊢ Π, Q | 1 ≤ 𝑗 ≤ 𝑘
                                                                                 (Rel𝑙 )
                              R , Rel(𝑟1 , . . . , 𝑟𝑙 ), 𝐹 , Σ ⊢ Π, Q

                                       R , 𝐹 , Σ ⊢ Π, 𝐺, Q
                                                                      (Rel𝑟 )†
                                  R , Σ ⊢ Π, Rel(𝑟1 , . . . , 𝑟𝑙 ), Q
We let 𝐹 := 𝐹1 , . . . , 𝐹𝑛 , 𝐺 := 𝐺1 , . . . , 𝐺𝑘 and the side condition † states that (Rel𝑟 ) is
applicable only if the individuals ⃗𝑎 (the collection of all individuals occurring within 𝐹 and 𝐺)
are eigenvariables. (NB. Eigenvariables are individuals that do not occur in the conclusion of
a rule, i.e. they are fresh in the premise(s), which ensures the soundness of rule applications;
for a discussion on eigenvariables, see [12].) We let G3𝒜ℒ𝒞 ⋆ denote G3𝒜ℒ𝒞 extended with
any finite number of DDR pairs {(Rel𝑙 ), (Rel𝑟 )}, and note that such extensions give calculi for
extensions of 𝒜ℒ𝒞. For example, if we aim to provide a calculus for the DL 𝒮, then our calculus
must be capable of reasoning with transitivity axioms i.e. formulae of the form Trans(𝑟) with
𝑟 ∈ R. Trans(𝑟) can be defined by means of a descriptive definition, implying that we can
obtain a calculus for the DL 𝒮 by extending G3𝒜ℒ𝒞 with the two rules shown below. (NB. The
side condition † states that 𝑎, 𝑏, and 𝑐 must be eigenvariables.)

                    R , Trans(𝑟), 𝑟(𝑎, 𝑏), 𝑟(𝑏, 𝑐), 𝑟(𝑎, 𝑐), Σ ⊢ Π, Q
                                                                      (Trans(𝑟)𝑙 )
                         R , Trans(𝑟), 𝑟(𝑎, 𝑏), 𝑟(𝑏, 𝑐), Σ ⊢ Π, Q

                         R , 𝑟(𝑎, 𝑏), 𝑟(𝑏, 𝑐), Σ ⊢ Π, 𝑟(𝑎, 𝑐), Q
                                                                 (Trans(𝑟)𝑟 )†
                                R , Σ ⊢ Trans(𝑟), Π, Q

  Some care must be taken when extending G3𝒜ℒ𝒞 with DDRs. It is possible that certain
properties of G3𝒜ℒ𝒞, such as contraction hp-admissibility (see Theorem 2), are not immediately
preserved in extensions of the calculus with DDRs. We apply a solution that is motivated by
the work of [12]; namely, we can avoid such undesirable circumstances by ensuring that any
extension of G3𝒜ℒ𝒞 with DDRs adheres to the closure condition. (NB. For the remainder of the
paper, we assume that every extension of G3𝒜ℒ𝒞 satisfies the closure condition.)
Definition 4 (Closure Condition [12]). A calculus with DDRs satisfies the closure condition
iff for any DDR in the calculus which has a substitution instance containing duplicate principal
formulae, the calculus also contains an instance of the rule with the duplicate formulae contracted.
  Since only a finite number of substitution instances produce duplicate principal formulae in
a DDR, the closure condition will only add a finite number of rules in any extension of G3𝒜ℒ𝒞.
  We now define a semantics for sequents as this will be used for soundness and completeness.
Definition 5 (Sequent Semantics). Let ℐ = (Δℐ , ·ℐ ) be an interpretation. A sequent Λ :=
R , Σ ⊢ Π, Q is satisfied in ℐ, written ℐ |= Λ, iff if ℐ satisfies all formulae in R , Σ, then ℐ satisfies
some formula in Q , Π. A sequent Λ is falsified in ℐ iff ℐ ̸|= Λ, i.e. Λ is not satisfied in ℐ. A sequent
Λ is valid, written |= Λ, iff it is satisfiable in every interpretation, and is invalid otherwise.

3.2. Rules for Extensions of 𝒜ℒ𝒞
We discuss extensions of G3𝒜ℒ𝒞 ⋆ with rules for deriving new concept assertions (e.g. unquali-
fied number restrictions and nominals) and EFs (e.g. equalities and RIAs). We introduce these
additional rules in the same manner as we introduced extensions of 𝒜ℒ𝒞 in Section 2.2.
   𝒮 If the language of our DL includes role compositions, then the rules (∘𝑙 ) and (∘𝑟 ) (shown
below) should be included in the corresponding calculus to allow reasoning with role compo-
sitions. (NB. 𝑠 is permitted to be a chain 𝑟1 ∘ · · · ∘ 𝑟𝑛 of role compositions.) Since we can use
axioms of the form 𝑟 ∘ 𝑟 ⊑ 𝑟 or Trans(𝑟) to indicate that a role 𝑟 is transitive, there are two
distinct sets of rules which can be included in a calculus to allow reasoning with transitive roles.
   First, if our DL allows for axioms of the form 𝑟 ∘ 𝑟 ⊑ 𝑟, then the composition rules, and
restricted versions of the (𝑐𝑟𝑖𝑎𝑙 ) and (𝑐𝑟𝑖𝑎𝑟 ) rules (introduced in the 𝒮ℛ subsection below) that
only allow principal formulae of the form 𝑟 ∘ 𝑟 ⊑ 𝑟, should be included in the corresponding
calculus. (NB. The side condition † on the (∘𝑙 ) rule stipulates that 𝑏 is an eigenvariable.)
                                R , 𝑟(𝑎, 𝑏), 𝑠(𝑏, 𝑐), Σ ⊢ Π, Q
                                                               (∘𝑙 )†
                                 R , (𝑟 ∘ 𝑠)(𝑎, 𝑐), Σ ⊢ Π, Q
         R , Σ ⊢ Π, (𝑟 ∘ 𝑠)(𝑎, 𝑐), 𝑟(𝑎, 𝑏), Q    R , Σ ⊢ Π, (𝑟 ∘ 𝑠)(𝑎, 𝑐), 𝑠(𝑏, 𝑐), Q
                                                                                      (∘𝑟 )
                                 R , Σ ⊢ Π, (𝑟 ∘ 𝑠)(𝑎, 𝑐), Q
  Second, if we make use of transitivity axioms of the form Trans(𝑟) in our DL, then the
DDRs (Trans(𝑟)𝑙 ) and (Trans(𝑟)𝑟 ), introduced in the previous section, should be included in
our calculus to ensure sound and complete reasoning with such formulae.
  ℋ If we wish to enable reasoning with RIAs of the form 𝑟 ⊑ 𝑠 (e.g. as in 𝒜ℒ𝒞ℋ), then one
should add restricted versions of the (𝑐𝑟𝑖𝑎𝑙 ) and (𝑐𝑟𝑖𝑎𝑟 ) rules (introduced in the 𝒮ℛ subsection
below) where 𝑛 = 1, to ensure sound and complete reasoning with RIAs.
   𝒮ℛ To enable reasoning with CRIAs, the composition rules (∘𝑙 ) and (∘𝑟 ) should be included
along with the following (𝑐𝑟𝑖𝑎𝑙 ) and (𝑐𝑟𝑖𝑎𝑟 ) rules. (NB. The side condition † on the (𝑐𝑟𝑖𝑎𝑟 )
rule states that 𝑎 and 𝑏 must be eigenvariables. For readability, let 𝐹 denote 𝑟1 ∘ · · · ∘ 𝑟𝑛 ⊑ 𝑟.)
            R , 𝐹, Σ ⊢ Π, (𝑟1 ∘ · · · ∘ 𝑟𝑛 )(𝑎, 𝑏), Q   R , 𝑟(𝑎, 𝑏), 𝐹, Σ ⊢ Π, Q
                                                                                 (𝑐𝑟𝑖𝑎𝑙 )
                                        R , 𝐹, Σ ⊢ Π, Q
                       R , (𝑟1 ∘ · · · ∘ 𝑟𝑛 )(𝑎, 𝑏), Σ ⊢ Π, 𝑟(𝑎, 𝑏), Q
                                                                       (𝑐𝑟𝑖𝑎𝑟 )†
                                        R , Σ ⊢ Π, 𝐹, Q
   The (ir)reflexivity, asymmetry, and disjointness axioms can all be defined by means of de-
scriptive definitions: Refl(𝑟) ↔ ∀𝑎(⊤ → 𝑟(𝑎, 𝑎)), Asy(𝑟) ↔ ∀𝑎∀𝑏(𝑟(𝑎, 𝑏) ∧ 𝑟(𝑏, 𝑎) → ⊥),
Irr(𝑟) ↔ ∀𝑎(𝑟(𝑎, 𝑎) → ⊥), and Dis(𝑟, 𝑠) ↔ ∀𝑎∀𝑏(𝑟(𝑎, 𝑏) ∧ 𝑠(𝑎, 𝑏) → ⊥). Thus, extending
G3𝒜ℒ𝒞 ⋆ with the corresponding DDRs provides our calculus with the capacity to reason with
such axioms. All such DDRs can be obtained from the (Rel𝑙 ) and (Rel𝑟 ) rule schemata.
  𝒪 To enable reasoning with nominals, one should include the following rules along with the
equality rules of the final subsection below.
           R , 𝑎 ≈ 𝑏, 𝑎 : {𝑏}, Σ ⊢ Π, Q              R , Σ ⊢ Π, 𝑎 : {𝑏}, 𝑎 ≈ 𝑏, Q
                                        ({𝑏}1𝑙 )                                  ({𝑏}1𝑟 )
               R , 𝑎 : {𝑏}, Σ ⊢ Π, Q                     R , Σ ⊢ Π, 𝑎 : {𝑏}, Q
                  R , 𝑏 : {𝑏}, Σ ⊢ Π, Q                                       ({𝑏}2𝑟 )
                                        ({𝑏}2𝑙 )     R , Σ ⊢ Π, 𝑏 : {𝑏}, Q
                       R , Σ ⊢ Π, Q

  ℐ To add support for reasoning with inverse roles, one should not only allow inverse roles to
appear in the relevant rules of the calculus (e.g. (𝑖𝑑R ), (∃𝑙 ), and (∀𝑟 )), but should also include
the following two rules that encode the fact that the roles 𝑟 and 𝑟− are inverses.
    R , 𝑟(𝑎, 𝑏), 𝑟− (𝑏, 𝑎), Σ ⊢ Π, Q                    R , 𝑟− (𝑎, 𝑏), 𝑟(𝑏, 𝑎), Σ ⊢ Π, Q
                                     (𝑖𝑛𝑣(𝑟)𝑙 )                                          (𝑖𝑛𝑣(𝑟− )𝑙 )
         R , 𝑟(𝑎, 𝑏), Σ ⊢ Π, Q                               R , 𝑟− (𝑎, 𝑏), Σ ⊢ Π, Q

    R , Σ ⊢ Π, 𝑟(𝑎, 𝑏), 𝑟− (𝑏, 𝑎), Q                    R , Σ ⊢ Π, 𝑟− (𝑎, 𝑏), 𝑟(𝑏, 𝑎), Q
                                     (𝑖𝑛𝑣(𝑟)𝑟 )                                          (𝑖𝑛𝑣(𝑟− )𝑟 )
         R , Σ ⊢ Π, 𝑟(𝑎, 𝑏), Q                              R , Σ ⊢ Π, 𝑟− (𝑎, 𝑏), Q

   ℱ Functionality axioms of the form Funct(𝑟) can be defined by means of descriptive defini-
tions; e.g. Funct(𝑟) ↔ ∀𝑎∀𝑏∀𝑐(𝑟(𝑎, 𝑏) ∧ 𝑟(𝑎, 𝑐) → 𝑏 ≈ 𝑐). We can make use of the (Rel𝑙 ) and
(Rel𝑟 ) rule schemata to define DDRs for Funct(𝑟). Hence, a calculus can be enabled to reason
about functionality axioms by including the equality rules (introduced in final subsection below)
along with the pair of DDRs obtained from the above descriptive defintion.
  𝒩 To allow reasoning with unqualified number restrictions, one makes use of versions of
the (⩽ 𝑛𝑟.𝑃𝑙 ), (⩽ 𝑛𝑟.𝑃𝑟 ), (⩾ 𝑛𝑟.𝑃𝑙 ), and (⩾ 𝑛𝑟.𝑃𝑟 ) rules (shown in the next subsection 𝒬)
where the first set of premises is omitted, and where the 𝑏𝑖 : 𝑃 formulae are omitted from
the remaining premises. We refer to each of these versions as (⩽ 𝑛𝑟𝑙 ), (⩽ 𝑛𝑟𝑟 ), (⩾ 𝑛𝑟𝑙 ), and
(⩾ 𝑛𝑟𝑟 ), respectively. Additionally, the equality rules of the final subsection below should be
included to ensure proper reasoning with equalities.
   𝒬 To enable a calculus to derive theorems concerning qualified number restrictions, we add
the following four rules along with the equality rules of the final subsection below. (NB. In
the (⩽ 𝑛𝑟.𝑃𝑟 ) rule, †1 states that 𝑏0 , . . . , 𝑏𝑛 must be eigenvariables and Q ′ := {𝑏𝑖 ≈ 𝑏𝑗 | 0 ≤
𝑖 < 𝑗 ≤ 𝑛}, and in the (⩾ 𝑛𝑟.𝑃𝑙 ) rule, †2 states that 𝑏1 , . . . , 𝑏𝑛 must be eigenvariables and
Q ′ := {𝑏𝑖 ≈ 𝑏𝑗 | 1 ≤ 𝑖 < 𝑗 ≤ 𝑛}.)
      {︁                                                                             }︁
        R , 𝑟(𝑎, 𝑏0 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ, 𝑎 : (⩽ 𝑛𝑟.𝑃 ) ⊢ 𝑏𝑖 : 𝑃, Π, Q | 0 ≤ 𝑖 ≤ 𝑛 ∪
   {︁                                                                                    }︁
     R , 𝑏𝑖 ≈ 𝑏𝑗 , 𝑟(𝑎, 𝑏0 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ, 𝑎 : (⩽ 𝑛𝑟.𝑃 ) ⊢ Π, Q | 0 ≤ 𝑖 < 𝑗 ≤ 𝑛
                                                                                                (⩽ 𝑛𝑟.𝑃𝑙 )
                   R , 𝑟(𝑎, 𝑏0 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ, 𝑎 : (⩽ 𝑛𝑟.𝑃 ) ⊢ Π, Q

             R , 𝑟(𝑎, 𝑏0 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ, 𝑏0 : 𝑃, . . . , 𝑏𝑛 : 𝑃 ⊢ Π, Q ′ , Q
                                                                                      (⩽ 𝑛𝑟.𝑃𝑟 )†1
                                  R , Σ ⊢ 𝑎 : (⩽ 𝑛𝑟.𝑃 ), Π, Q

              R , 𝑟(𝑎, 𝑏1 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ, 𝑏1 : 𝑃, . . . , 𝑏𝑛 : 𝑃 ⊢ Π, Q ′ , Q
                                                                                       (⩾ 𝑛𝑟.𝑃𝑙 )†2
                                   R , Σ, 𝑎 : (⩾ 𝑛𝑟.𝑃 ) ⊢ Π, Q
      {︁                                                                                  }︁
        R , 𝑟(𝑎, 𝑏1 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ ⊢ 𝑏𝑖 : 𝑃, 𝑎 : (⩾ 𝑛𝑟.𝑃 ), Π, Q | 1 ≤ 𝑖 ≤ 𝑛 ∪
   {︁                                                                                        }︁
     R , 𝑏𝑖 ≈ 𝑏𝑗 , 𝑟(𝑎, 𝑏1 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ ⊢ 𝑎 : (⩾ 𝑛𝑟.𝑃 ), Π, Q | 0 ≤ 𝑖 < 𝑗 ≤ 𝑛
                                                                                                  (⩾ 𝑛𝑟.𝑃𝑟 )
                    R , 𝑟(𝑎, 𝑏1 ), . . . , 𝑟(𝑎, 𝑏𝑛 ), Σ ⊢ 𝑎 : (⩾ 𝑛𝑟.𝑃 ), Π, Q

   Other Extensions To enable reasoning with equalities, we include (≈𝑙 ), (≈𝑟 ), (Rep1 (≈)),
(Rep2 (≈)) and (Euc(≈)); to enable reasoning with inequalities, we add the (̸≈𝑙 ) and (̸≈𝑟 ) rules
along with the previous five. To enable reasoning with negated role assertions we include (¬R𝑙 )
and (¬R𝑟 ) in our calculus; to ensure theorems can be derived concerning the universal role U,
we allow the role to be used in the relevant rules of our calculus (e.g. (𝑖𝑑R ), (∃𝑙 ), and (∀𝑟 )) and
also include the (U𝑙 ) and (U𝑟 ) rules shown below. Last, we include the (Self 𝑙 ) and (Self 𝑟 ) rules
if we want our calculus to support complex concepts of the form ∃𝑟.Self. (NB. In the (Rep1 (≈))
and (Rep2 (≈)) rules, [𝑎/𝑏] denotes a substitution of 𝑏 for 𝑎 in the relevant formula.)

   R , 𝑎 ≈ 𝑎, Σ ⊢ Π, Q                                     (≈𝑟 )     R , Σ ⊢ Π, 𝑟(𝑎, 𝑏), Q
                       (≈𝑙 )       R , Σ ⊢ Π, 𝑎 ≈ 𝑎, Q                                     (¬R𝑙 )
       R , Σ ⊢ Π, Q                                                 R , ¬𝑟(𝑎, 𝑏), Σ ⊢ Π, Q

        R , 𝑎 ≈ 𝑏, Σ, 𝑎 : 𝑃, 𝑏 : 𝑃 ⊢ Π, Q                     R , Σ ⊢ Π, 𝑟(𝑎, 𝑎), Q
                                          (Rep1 (≈))                                  (Self 𝑟 )
            R , 𝑎 ≈ 𝑏, Σ, 𝑎 : 𝑃 ⊢ Π, Q                      R , Σ ⊢ 𝑎 : ∃𝑟.Self, Π, Q

  R , 𝑎 ≈ 𝑏, 𝐹, 𝐹 [𝑎/𝑏], Σ ⊢ Π, Q                    R , 𝑎 ≈ 𝑏, 𝑎 ≈ 𝑐, 𝑏 ≈ 𝑐, Σ ⊢ Π, Q
                                  (Rep2 (≈))                                           (Euc(≈))
       R , 𝑎 ≈ 𝑏, 𝐹, Σ ⊢ Π, Q                            R , 𝑎 ≈ 𝑏, 𝑎 ≈ 𝑐, Σ ⊢ Π, Q

   R , Σ ⊢ Π, 𝑎 ≈ 𝑏, Q             R , 𝑟(𝑎, 𝑏), Σ ⊢ Π, Q                 R , U(𝑎, 𝑏), Σ ⊢ Π, Q
                        (̸≈𝑙 )                           (¬R𝑟 )                                (U𝑙 )
   R , 𝑎 ̸≈ 𝑏, Σ ⊢ Π, Q           R , Σ ⊢ Π, ¬𝑟(𝑎, 𝑏), Q                      R , Σ ⊢ Π, Q

                          (U𝑟 )      R , 𝑟(𝑎, 𝑎), Σ ⊢ Π, Q                  R , 𝑎 ≈ 𝑏, Σ ⊢ Π, Q
  R , Σ ⊢ Π, U(𝑎, 𝑏), Q                                      (Self 𝑙 )                           (̸≈𝑟 )
                                   R , Σ, 𝑎 : ∃𝑟.Self ⊢ Π, Q                R , Σ ⊢ Π, 𝑎 ̸≈ 𝑏, Q

  We use G3𝒜ℒ𝒞 * to denote an extension of a calculus G3𝒜ℒ𝒞 ⋆ with sets of the above rules.
We allow for extensions with the sets shown below, and note that the addition of one set of
rules may necessitate the addition of another set of rules, as explained above. Extensions with
rules for RRAs (such as Trans(𝑟) and Asy(𝑟)) are taken into account as extensions with DDRs:
  {(∘𝑙 ), (∘𝑟 )}; {(𝑐𝑟𝑖𝑎𝑙 ), (𝑐𝑟𝑖𝑎𝑟 )}; {(Self 𝑙 ), (Self 𝑟 )}; {(̸≈𝑙 ), (̸≈𝑟 )}; {(¬R𝑙 ), (¬R𝑟 )};
  {(U𝑙 ), (U𝑟 )}; {(𝑖𝑛𝑣(𝑟)𝑙 ), (𝑖𝑛𝑣(𝑟− )𝑙 ), (𝑖𝑛𝑣(𝑟)𝑟 ), (𝑖𝑛𝑣(𝑟− )𝑟 )};
  {({𝑏}1𝑙 ), ({𝑏}2𝑙 ), ({𝑏}1𝑟 ), ({𝑏}2𝑟 )}; {(⩽ 𝑛𝑟.𝑃𝑙 ), (⩽ 𝑛𝑟.𝑃𝑟 ), (⩾ 𝑛𝑟.𝑃𝑙 ), (⩾ 𝑛𝑟.𝑃𝑟 )};
  {(⩽ 𝑛𝑟𝑙 ), (⩽ 𝑛𝑟𝑟 ), (⩾ 𝑛𝑟𝑙 ), (⩾ 𝑛𝑟𝑟 )}; {(≈𝑙 ), (≈𝑟 ), (Euc(≈)), (Rep1 (≈)), (Rep2 (≈))}.

Theorem 1. R , Σ ⊢ Π, Q is derivable in G3𝒜ℒ𝒞 * iff |= R , Σ ⊢ Π, Q .

Proof. Soundness (the forward direction) is shown by induction on the height of the given
derivation. Completeness (the backward direction) is shown by a method due to Kripke [22].
We assume R , Σ ⊢ Π, Q is not derivable, and show that a counter-model can be extracted from
failed proof search; thus, if a sequent is not derivable, it is not valid, implying completeness.

   We additionally show that our calculi possess desirable proof-theoretic properties. Before
stating our theorem concerning which properties are possessed, we recall the definition of each
property for the reader. A rule is defined to be (height-preserving) admissible in a calculus iff
if the premise(s) of the rule is (are) derivable in the calculus (with a certain height), then the
conclusion is derivable in the calculus (with a height less than or equal to the height of the
premise(s)). Let us define the inverse of (𝑅), written (𝑅
                                                        ^ ), to be the rule obtained by switching the
conclusion and the premise(s) of (𝑅). A rule (𝑅) is defined to be (height-preserving) invertible
in a calculus iff (𝑅
                   ^ ) is (height-presevering) admissible. That is, if there exists a derivation for
       R , Σ ⊢ Π, Q                       R , Σ ⊢ Π, Q                  R , R ′ , R ′ , Σ, Σ′ , Σ′ ⊢ Π, Q
                          (𝑤𝑘𝑙 )                              (𝑤𝑘𝑟 )                                      (𝑐𝑡𝑟𝑙 )
   R , R ′ , Σ, Σ′ ⊢ Π, Q             R , Σ ⊢ Π, Π′ , Q , Q ′               R , R ′ , Σ, Σ′ ⊢ Π, Q

                R , Σ ⊢ Π′ , Π′ , Π, Q ′ , Q ′ , Q                  R , Σ ⊢ Π, Q
                                                   (𝑐𝑡𝑟𝑟 )                               (𝑠𝑢𝑏)
                    R , Σ ⊢ Π′ , Π, Q ′ , Q                  (R , Σ)[𝑏/𝑎] ⊢ (Π, Q )[𝑏/𝑎]

Figure 2: Admissible structural rules.


the conclusion, its premises can be derived as well [12]. As is common in the literature, we
usually write hp-admissible and hp-invertible instead of height-preserving admissible and height-
preserving invertible, and we remark that such properties are important as they can be leveraged
to prove decidability of logics [19], to permit automated counter-model extraction [23], or to
prove cut-elimination [12], among other applications. Note that in (𝑠𝑢𝑏), applying a substitution
[𝑏/𝑎] to a multiset is defined in the usual way as the replacement of all occurrences of 𝑎 by 𝑏 in
the multiset. Last, we note that special (hp-)admissible structural rules are shown in Figure 2.

Theorem 2. Each calculus G3𝒜ℒ𝒞 * possesses the following properties: (i) For all EFs and IFs 𝑋,
R , 𝑋, Σ ⊢ Π, 𝑋, Q is derivable in G3𝒜ℒ𝒞 * , (ii) All rules of G3𝒜ℒ𝒞 * are hp-invertible, (iii) The
(𝑠𝑢𝑏), (𝑤𝑘𝑙 ), (𝑤𝑘𝑟 ), (𝑐𝑡𝑟𝑙 ), and (𝑐𝑡𝑟𝑟 ) rules are hp-admissible in G3𝒜ℒ𝒞 * .

Proof. (i) is shown by induction on the structure of 𝑋, and (ii) and (iii) are shown by induction
on the height of the given derivation.


4. Conclusion and Future Work
This paper provides a uniform framework for generating sequent systems on demand for a
considerable number of expressive description logics including extensions with role relational
axioms. All calculi are sound, complete, and possess standard properties. In future work, we
aim to optimize our calculi by (i) simplifying the systems through confirming the admissibility
of rules (e.g. (⊥𝑟 ) and (⊤𝑙 )), (ii) applying a methodology called structural refinement [24],
which has been used to ready proof systems for use in automated reasoning tasks [25, 23],
and (iii) extending our formalism to a broader set of DLs (e.g. intuitionistic or constructive
DLs [26, 27, 28]) which can be defined proof-theoretically.
   We note that efficient reasoners, based on tableaux, for expressive DLs do already exist (e.g.
HermiT [29]). However, since the current paper merely provides a framework for constructing
sequent systems for expressive DLs, comparing decision algorithms based on our sequent
systems with those based on existing tableaux must be left to future work. Nevertheless,
sequent calculi have proven beneficial in establishing meta-logical properties, and thus, we aim
to adapt existing methods for sequent systems to obtain constructive proofs of (various forms
of) interpolation (as in [25, 30]), and to utilize our systems in computing re-writings of concepts
and TBoxes. Last, we conjecture that cut-elimination holds for G3𝒜ℒ𝒞 when we restrict cuts to
IFs, though we aim to investigate various forms of cut-elimination for all of our sequent calculi.
References
 [1] F. Baader, I. Horrocks, C. Lutz, U. Sattler, Introduction to Description Logic, Cambridge
     University Press, 2017.
 [2] F. M. Donini, M. Lenzerini, D. Nardi, W. Nutt, The complexity of concept languages,
     Information and Computation 134 (1997) 1–58. doi:10.1006/inco.1997.2625.
 [3] I. Horrocks, U. Sattler, Decidability of shiq with complex role inclusion axioms, Artificial
     Intelligence 160 (2004) 79–104.
 [4] M. Ortiz, D. Calvanese, T. Eiter, Characterizing data complexity for conjunctive query
     answering in expressive description logics, in: Proceedings of the 21st National Conference
     on Artificial Intelligence - Volume 1, AAAI’06, AAAI Press, 2006, p. 275–280.
 [5] M. Ortiz, D. Calvanese, T. Eiter, Data complexity of query answering in expressive
     description logics via tableaux, J. Autom. Reason. 41 (2008) 61–98. doi:10.1007/
     s10817-008-9102-9.
 [6] M. Schmidt-Schauß, G. Smolka, Attributive concept descriptions with complements,
     Artificial Intelligence 48 (1991) 1–26. doi:10.1016/0004-3702(91)90078-X.
 [7] Y. Kazakov, B. Motik, A resolution-based decision procedure for 𝒮ℋ𝒪ℐ𝒬, in: U. Furbach,
     N. Shankar (Eds.), Automated Reasoning, Springer Berlin Heidelberg, Berlin, Heidelberg,
     2006, pp. 662–677.
 [8] B. Motik, U. Sattler, A comparison of reasoning techniques for querying large description
     logic aboxes, in: M. Hermann, A. Voronkov (Eds.), Logic for Programming, Artificial
     Intelligence, and Reasoning, Springer Berlin Heidelberg, Berlin, Heidelberg, 2006, pp.
     227–241.
 [9] D. Trivela, G. Stoilos, A. Chortaras, G. Stamou, Optimising resolution-based rewriting
     algorithms for owl ontologies, Journal of Web Semantics 33 (2015) 30–49. doi:10.1016/j.
     websem.2015.02.001, ontology-based Data Access.
[10] F. Simancik, Y. Kazakov, I. Horrocks, Consequence-based reasoning beyond horn ontologies,
     in: IJCAI, 2011, pp. 1093–1099.
[11] Y. Kazakov, Consequence-driven reasoning for horn shiq ontologies, in: Proceedings of the
     21st International Jont Conference on Artifical Intelligence, IJCAI’09, Morgan Kaufmann
     Publishers Inc., San Francisco, CA, USA, 2009, p. 2040–2045.
[12] S. Negri, J. Von Plato, Proof analysis: a contribution to HIlbert’s last problem, Cambridge
     University Press, 2011.
[13] A. Borgida, E. Franconi, I. Horrocks, Explaining alc subsumption, in: Proceedings of the
     14th European Conference on Artificial Intelligence, ECAI’00, IOS Press, NLD, 2000, p.
     209–213.
[14] M. Hofmann, Proof-theoretic approach to description-logic, in: 20th Annual IEEE Sym-
     posium on Logic in Computer Science (LICS’ 05), 2005, pp. 229–237. doi:10.1109/LICS.
     2005.38.
[15] A. Rademaker, A Proof Theory for Description Logics, Springer Science & Business Media,
     2012.
[16] U. Straccia, A sequent calculus for reasoning in four-valued description logics, in:
     D. Galmiche (Ed.), Automated Reasoning with Analytic Tableaux and Related Methods,
     Springer Berlin Heidelberg, Berlin, Heidelberg, 1997, pp. 343–357.
[17] B. C. Grau, I. Horrocks, B. Motik, B. Parsia, P. Patel-Schneider, U. Sattler, Owl 2: The next
     step for owl, Journal of Web Semantics 6 (2008) 309–322. doi:10.1016/j.websem.2008.
     05.001, semantic Web Challenge 2006/2007.
[18] M. Ortiz, M. Šimkus, Reasoning and query answering in description logics, in: T. Eiter,
     T. Krennwallner (Eds.), Reasoning Web. Semantic Technologies for Advanced Query
     Answering: 8th International Summer School 2012, Vienna, Austria, September 3-8, 2012.
     Proceedings, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 1–53. doi:10.1007/
     978-3-642-33158-9\_1.
[19] S. C. Kleene, Introduction to Metamathematics, American Elsevier Publishing Company,
     INC. - New York, 1952.
[20] A. K. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, Ph.D. thesis,
     University of Edinburgh. College of Science and Engineering. School of Informatics, 1994.
[21] L. Viganò, Labelled Non-Classical Logics, Springer Science & Business Media, 2000.
[22] S. A. Kripke, A completeness theorem in modal logic, Journal of Symbolic Logic 24 (1959)
     1–14. doi:10.2307/2964568.
[23] T. Lyon, K. van Berkel, Automating agential reasoning: Proof-calculi and syntactic decid-
     ability for stit logics, in: M. Baldoni, M. Dastani, B. Liao, Y. Sakurai, R. Zalila Wenkstern
     (Eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems - 22nd International
     Conference, Proceedings, volume 11873 of Lecture Notes in Computer Science, Springer
     International Publishing, Cham, 2019, pp. 202–218.
[24] T. Lyon, Refining Labelled Systems for Modal and Constructive Logics with Applications,
     Ph.D. thesis, Technische Universität Wien, 2021.
[25] T. Lyon, A. Tiu, R. Goré, R. Clouston, Syntactic interpolation for tense logics and bi-
     intuitionistic logic via nested sequents, in: M. Fernández, A. Muscholl (Eds.), 28th EACSL
     Annual Conference on Computer Science Logic, CSL 2020, volume 152 of LIPIcs, Schloss
     Dagstuhl - Leibniz-Zentrum für Informatik, 2020, pp. 28:1–28:16. doi:10.4230/LIPIcs.
     CSL.2020.28.
[26] M. Ferrari, C. Fiorentini, G. Fiorino, ℬ𝒞𝒟ℒ: Basic constructive description logic, J. Autom.
     Reason. 44 (2010) 371–399. doi:10.1007/s10817-009-9160-7.
[27] V. de Paiva, Constructive description logics: What , why and how, 2006. Unpublished.
[28] S. Scheele, Model and Proof Theory of Constructive ALC, Constructive Description Logics,
     University of Bamberg Press, 2015.
[29] B. Glimm, I. Horrocks, B. Motik, G. Stoilos, Z. Wang, Hermit: an owl 2 reasoner, Journal
     of Automated Reasoning 53 (2014) 245–269.
[30] S. Maehara, On the interpolation theorem of craig, Sûgaku 12 (1960) 235–237.