Proof Theory of Circular Description Logics

Abstract

In [12], Hofmann introduces a sequent calculus for the description logic EL where the TBoxes allow for circular concept definitions. In this thesis, we apply this frame- work to a family of DLs which allow for circular TBoxes. We start off by adjusting the calculus for the class of frame-based DLs, with base logic FL0. We continue to the attribute languages AL and ALE. For these calculi, we prove soundness and completeness with respect to greatest fixpoint semantics for their fragments AL′ and ALE′, using Hofmann’s strategy. When applying the theory to a logic including disjunction, we require a different strategy and introduce the notion of pre-interpretation for the soundness and completeness proofs. Then, we acknowl- edge the drawbacks of considering only greatest fixpoint semantics when it comes to circular definitions, and propose a calculus that includes greatest- and least-fixpoint semantics in one. Finally, we discuss the drawbacks of Hofmann’s system for the classical logic ALC by discussing the consequences for the proofs when including the disjunction or negation, and give suggestions for future research.