A Peirce-style calculus for ALC

Description logics (DLs) are a well-understood family of knowledge representation (KR) languages. The notation of DLs has the flavour of a variable-free first order predicate logic. In this paper, a diagrammatic representation of the DL ALC, based on Peirce’s existential graphs, is presented, and a set of transformation rules on these graphs is provided. It is proven that these rules form a sound and complete diagrammatic calculus for ALC.