Caught in the Spiders’ Diagrammatic Reasoning Web–The Euler/Spider Diagram Family of Formal Reasoning Systems–

Formal Diagrammatic Reasoning Systems are a class of formal systems whose syntax relies on diagrams and whose deduction rules can be expressed as diagram rewritings. A well known example is the family of Euler diagrams, which play a prominent role in information visualization but also have an underlying rigorous formal reasoning system expressed via diagram/graph rewritings. This course introduces Euler Diagrams and their offspring—particularly different variants of Spider Diagrams—from a rigorous formal logical point of view, especially highlighting their underlying diagrammatic deduction system that allows one to “draw” proofs. We show how to extend the diagrams’ expressive power in information visualisation with different variants of diagrammatic rule-based deduction systems, and provide a proper embedding into the categorical theory of graph transformation. State-of-the-art research insights into the design and implementation of (diagrammatic) reasoning systems are then applied in practice for providing a framework for policy-based reasoning on dynamic domain models.