SD2: a sound and complete diagrammatic reasoning system

Author

Howse, John ; Molina, Fernando ; Taylor, John

Author_Institution

Sch. of Comput. & Math. Sci., Brighton Polytech., UK

fYear

2000

fDate

2000

Firstpage

127

Lastpage

134

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

Keywords

diagrams; object-oriented programming; set theory; spatial reasoning; visual programming; SD2; Unified Modelling Language; Venn diagrams; Venn-Peirce diagrams; completeness; constraint diagrams; diagrammatic reasoning system; inference rules; lower bounds; object-oriented modelling; proof strategy; semantics; set cardinalities; set theory; spider diagram systems; syntax; upper bounds; visual notation; Logic; Optimized production technology; Unified modeling language; Upper bound;

fLanguage

English

Publisher

ieee

Conference_Titel

Visual Languages, 2000. Proceedings. 2000 IEEE International Symposium on

Conference_Location

Seattle, WA

ISSN

1049-2615

Print_ISBN

0-7695-0840-5

Type

conf

DOI

10.1109/VL.2000.874376

Filename

874376