A diagrammatic reasoning system for the description logic ALC

Diagrammatic reasoning is a tradition of visual logic that allows sentences that are equivalent to first order logic to be written in a visual or structural form: usually for improved usability. A calculus for the diagram can then be defined that allows well-formed formulas to be derived. This calculus is intended in the analog of logical inference. Description logics (DLs) have become a popular knowledge representation and processing language. DLs correspond to decidable fragments of first order logic; their notation is in the style of symbolic, variable-free formulas. Moreover, DLs are equipped with table au theorem provers that are proven to be sound and complete. Although DLs have roots in diagrammatic languages (such as semantic networks), they are elaborated in a purely symbolic manner. This paper discusses how DLs can be equivalently represented in terms of a diagrammatic reasoning system. First, existing diagrammatic reasoning systems, namely spider- and constraint diagrams, as well as existential and conceptual graphs, are investigated to determine if they are compatible with DLs. It turns out that Peirce's existential graphs are better suited for this purpose than the alternatives we examine. The paper then redevelops the DL ALC, which is the smallest propositional DL, by means of labeled trees, and provides a diagrammatic representation for these trees in the style of Peircean graphs. We provide a calculus based on C.S. Peirce's calculus for existential graphs and prove the soundness and completeness of the calculus. The calculus acts on labeled trees, but can be best understood as a diagrammatic calculus whose rules modify the Peircean-style representation of ALC. © 2008 Elsevier Ltd. All rights reserved.