# Uniform and Modular Sequent Systems for Description Logics

arXiv: https://arxiv.org/abs/2206.09020 · HTML: https://mlsanity.com/paper/2206.09020/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 30 references that are in the map.
- First posted on arXiv 17 Jun 2022.

## Builds on (most cited first, 3 of 3)

- [Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents](https://mlsanity.com/paper/1910.05215/) (2019)
- [Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics](https://mlsanity.com/paper/1908.11360/) (2019)
- [Refining Labelled Systems for Modal and Constructive Logics with Applications](https://mlsanity.com/paper/2107.14487/) (2021)

## Built on by (most cited first, 1 of 1)

- [Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules](https://mlsanity.com/paper/2306.02521/) (2023)

## Abstract (arXiv)

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.