Traditionally the dominant formalist school in mathematics has considered diagrams as merely heuristic tools. However, the last few years have seen a renewed interest in visualisation in mathematics and, in particular, in diagrammatic reasoning. This has resulteQ from the increasing capabilities of modern computers, the key role that design and modelling notations play in the development process of software systems, and the emergence of the first formal diagrammatic systems. Constraint diagrams are a diagrammatic notation for expressing constraints that can be used in conjunction with the Unified Modelling Language (UML) in object-oriented modelling. Recently, full formal semantics and sound and complete inference rules have been developed for Venn-Peirce diagrams and Euler circles. Spider diagrams emerged from work on constraint diagrams. They combine and extend Venn-Peirce diagrams and Euler circles to express constraints on sets and their relationships with other sets. The spider diagram system SDI developed in this thesis extends the second Venn-Peirce system that Shin investigated, Venn II, to give lower bounds for the cardinality of the sets represented by the diagrams. A sound and complete set of reasoning rules is given. The diagrammatic system SD2 extends SD 1 so that lower and upper bounds can be inferred for the cardinalities of the set represented by the diagrams. Soundness and completeness results are also given extending the proof strategies used in SD 1. The system SD2 is also shown to be syntactically rich enough to express the negation of any diagram. Finally, the ESD2 system incorporates syntactic elements from the spider diagram notation, so that information within a diagram can be expressed more compactly, and is proved equivalent to SD2. Two important innovations are introduced with respect to Venn I, Venn II, and Higraphs: two levels of syntax - abstract and concrete - and a proof of completeness that omits the use of maximal diagram used in these systems. This work will help to provide the necessary mathematical underpinning for the development of software tools to aid the reasoning process . and the development and formalisation of more expressive diagrammatic notations.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:366385 |
| Date | January 2001 |
| Creators | Molina, Fernando |
| Publisher | University of Brighton |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0023 seconds