Uniform and Modular Sequent Systems for Description Logics
This work provides a modular approach for formal reasoning in description logics, which is incremental as it builds on existing ALC systems.
The authors tackled the problem of constructing sequent systems for expressive description logics extending ALC, resulting in a framework that covers a wide array of logics and extensions with role relational axioms, ensuring soundness, completeness, and favorable properties like height-preserving admissibility and invertibility.
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.