SD2: A Sound and Complete Diagrammatic Reasoning System

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 to include lower and upper bounds for the cardinalities of the sets represented by regions of diagrams. This paper summarises their syntax and semantics and introduces 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 objectoriented modelling notations such as the Unified Modelling Language.

• Type: Conference
• Year: 2000
• Where: VL
• Authors: John Howse, Fernando Molina, John Taylor
• Keywords: Richer Spider Diagram, Venn-Peirce Diagrams, Venn-type Diagrams, Visual Languages, VL 2000