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.
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 [
Although work has been done on supplying sequent systems for DLs [
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 ℒ [
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 components 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 [
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 [
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(), if ℐ 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 ℐ |= ⊑ , if ℐ ⊆ ℐ .
1ℐ is transitive if 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 ∘ · · · ∘ ⊑ , if 1ℐ ∘ · · · ∘ • ℐ satisfies Refl(), written ℐ |= Refl(), if ℐ is reflexive; • ℐ satisfies Irr(), written ℐ |= Irr(), if ℐ is irreflexive; • ℐ satisfies Asy(), written ℐ |= Asy(), if ℐ is asymmetric; • ℐ satisfies Dis(, ), written ℐ |= Dis(, ), if ℐ 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(), if ℐ 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 inequality 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 ℐ |= ≈ , if ℐ = ℐ ; • ℐ satisfies ̸≈ , written ℐ |= ̸≈ , if ℐ ̸= ℐ ; • ℐ satisfies ¬(, ), written ℐ |= ¬(, ), if (, ) ̸∈ ℐ .
2We 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 [
3Each property is defined as follows: (i) ℐ is reflexive if for each ∈ Δℐ , (, ) ∈ ℐ , (ii) ℐ is irreflexive if for each ∈ Δℐ , (, ) ̸∈ ℐ , (iii) ℐ is asymmetric if for each , ∈ Δℐ , if (, ) ∈ ℐ , then (, ) ̸∈ ℐ , and (iv) ℐ and ℐ are disjoint if ℐ ∩ ℐ = ∅.
4ℐ is functional if for all , , ∈ Δℐ , if (, ), (, ) ∈ ℐ , then = .
5We use # for a set to denote the cardinality of the set.
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(), relfexivity 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.
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. [
6For a discussion of G3-style calculi, along with the G1 and G2 variants, see [19, Section 80].
R , Σ, : ⊢ : , Π, Q
R , Σ, ⊢ , Π, Q (C)
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) R , Σ, : ⊤ ⊢ Π, Q
R , Σ ⊢ Π, Q R , Σ, : ⊢ Π, Q R , Σ ⊢ : ¬, Π, Q (⊤) (¬) (⊔) (⊓)
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 suficient 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 ≤ ≤ }︁ R , Rel(1, . . . , ), , Σ ⊢ Π, Q
R , , Σ ⊢ Π, , Q
R , Σ ⊢ Π, Rel(1, . . . , ), Q
(Rel)†
(Rel)
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 [
R , Trans(), (, ), (, ), (, ), Σ ⊢ Π, Q
R , Trans(), (, ), (, ), Σ ⊢ Π, Q
(Trans()) R , (, ), (, ), Σ ⊢ Π, (, ), Q
R , Σ ⊢ Trans(), Π, Q (Trans())†
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 [
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 ℐ |= Λ, if if ℐ satisfies all formulae in R , Σ, then ℐ satisfies some formula in Q , Π. A sequent Λ is falsified in ℐ if ℐ ̸|= Λ, i.e. Λ is not satisfied in ℐ. A sequent Λ is valid, written |= Λ, if it is satisfiable in every interpretation, and is invalid otherwise.
We discuss extensions of G3ℒ⋆ with rules for deriving new concept assertions (e.g. unqualiifed 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 compositions. (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 descriptive 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
R , : {}, Σ ⊢ Π, Q
R , Σ ⊢ Π, Q ({}1) ({}2)
R , Σ ⊢ Π, : {}, ≈ , Q
R , Σ ⊢ Π, : {}, Q
({}1) R , Σ ⊢ Π, : {}, Q ({}2) ℐ 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.
ℱ Functionality axioms of the form Funct() can be defined by means of descriptive definitions; 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 , (, ), − (, ), Σ ⊢ Π, Q
R , (, ), Σ ⊢ Π, Q R , Σ ⊢ Π, (, ), − (, ), Q
R , Σ ⊢ Π, (, ), Q (()) (())
R , − (, ), (, ), Σ ⊢ Π, Q
R , − (, ), Σ ⊢ Π, Q R , Σ ⊢ Π, − (, ), (, ), Q
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)
R , (, 0), . . . , (, ), Σ, : (⩽ . ) ⊢ Π, Q R , (, 0), . . . , (, ), Σ, 0 : , . . . , : ⊢ Π, Q ′, Q
R , Σ ⊢ : (⩽ . ), Π, Q R , (, 1), . . . , (, ), Σ, 1 : , . . . , : ⊢ Π, Q ′, Q
R , Σ, : (⩾ . ) ⊢ Π, Q (⩽ .)†1 (⩾ .)†2 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 , Σ ⊢ Π, (, ), Q R , ¬(, ), Σ ⊢ Π, Q (¬R) R , ≈ , Σ, : , : ⊢ Π, Q
R , ≈ , Σ, : ⊢ Π, Q (Rep1(≈ ))
R , Σ ⊢ Π, (, ), Q R , Σ ⊢ : ∃.Self, Π, Q (Self) R , ≈ , , [/], Σ ⊢ Π, Q
R , ≈ , , Σ ⊢ Π, Q R , Σ ⊢ Π, ≈ , Q R , ̸≈ , Σ ⊢ Π, Q R , Σ ⊢ Π, U(, ), Q (≉ ) (U) (Rep2(≈ ))
R , ≈ , ≈ , ≈ , Σ ⊢ Π, Q (Euc(≈ ))
R , ≈ , ≈ , Σ ⊢ Π, Q R , (, ), Σ ⊢ Π, Q R , Σ ⊢ Π, ¬(, ), Q (¬R)
R , U(, ), Σ ⊢ Π, Q
R , Σ ⊢ Π, Q
R , (, ), Σ ⊢ Π, Q R , Σ, : ∃.Self ⊢ Π, Q (Self)
R , ≈ , Σ ⊢ Π, Q R , Σ ⊢ Π, ̸≈ , Q (U) (≉ )
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ℒ* if |= 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 if 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 if (^) is (height-presevering) admissible. That is, if there exists a derivation for
R , Σ ⊢ Π, Q R , R ′, Σ, Σ′ ⊢ Π, Q ()
R , Σ ⊢ Π, Q R , Σ ⊢ Π, Π′, Q , Q ′ ()
R , R ′, R ′, Σ, Σ′, Σ′ ⊢ Π, Q
R , R ′, Σ, Σ′ ⊢ Π, Q () R , Σ ⊢ Π′, Π′, Π, Q ′, Q ′, Q
R , Σ ⊢ Π′, Π, Q ′, Q ()
R , Σ ⊢ Π, Q
(R , Σ)[/] ⊢ (Π, Q )[/]
()
the conclusion, its premises can be derived as well [
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.
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 eficient 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. [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 decidability 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 biintuitionistic 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.