Uniform and Modular Sequent Systems for Description Logics

TL;DR

This paper presents a unified framework for constructing sequent systems for expressive description logics, including extensions with role relational axioms, ensuring soundness, completeness, and desirable proof-theoretic properties.

Contribution

It introduces a general framework for sequent systems applicable to a wide range of description logics, including novel extensions with role relational axioms.

Findings

Sequent systems are sound and complete for the described logics.

Structural rules are height-preserving admissible.

Rules are height-preserving invertible.

Abstract

We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. 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.