SD2: a sound and complete diagrammatic reasoning system

Abstract

SD2 is a system of Venn-type diagrams that can be used to reason diagrammatically about sets, their cardinalities and their relationships. They augment the systems of Venn-Peirce diagrams investigated by Shin (1994) to include lower and upper bounds for the cardinalities of the sets represented by regions of diagrams. We summarise their syntax and semantics and introduce inference rules for reasoning with the system. We discuss the soundness of the system and develop a proof strategy for completeness simpler than that adopted by Shin. We expect this strategy to extend to other, richer spider diagram systems and to constraint diagrams, the visual notation that has been used in conjunction with object-oriented modelling notations such as the Unified Modelling Language.