Tableaux for Diagrammatic Reasoning

Diagrammatic notations, such as the Unified Modeling Language (UML), are in common use in software development. They allow many aspects of software systems to be described diagrammatically, but typically they rely on textual notations for logical constraints. In contrast, spider diagrams provide a visual notation for expressing a natural class of set- theoretic statements in a diagrammatic form. In this paper we present a tableau system for spider diagrams, and describe an implementation of the system. In a software development context, the system allows users to explore the implications of design choices, and thus to validate specifications; beyond this, the tableau algorithm and system are of general interest to visual reasoners.