Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-24T12:14:47.374Z Has data issue: false hasContentIssue false
  • English
  • Français

Spider Diagrams

Published online by Cambridge University Press:  01 February 2010

John Howse ,
Gem Stapleton  and
John Taylor
John Howse
Affiliation:
School of Computing, Mathematical and Information Sciences, University of Brighton, Watts Building, Brighton BN2 4GJ, United Kingdom, [email protected], http://www.brighton.ac.uk/cmis/research/vmg/
Gem Stapleton
Affiliation:
School of Computing, Mathematical and Information Sciences, University of Brighton, Watts Building, Brighton BN2 4GJ, United Kingdom, [email protected], http://www.brighton.ac.uk/cmis/research/vmg/
John Taylor
Affiliation:
School of Computing, Mathematical and Information Sciences, University of Brighton, Watts Building, Brighton BN2 4GJ, United Kingdom, [email protected], http://www.brighton.ac.uk/cmis/research/vmg/

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The use of diagrams in mathematics has traditionally been restricted to guiding intuition and communication. With rare exceptions such as Peirce's alpha and beta systems, purely diagrammatic formal reasoning has not been in the mathematician's or logician's toolkit. This paper develops a purely diagrammatic reasoning system of “spider diagrams” that builds on Euler, Venn and Peirce diagrams. The system is known to be expressively equivalent to first-order monadic logic with equality. Two levels of diagrammatic syntax have been developed: an ‘abstract’ syntax that captures the structure of diagrams, and a ‘concrete’ syntax that captures topological properties of drawn diagrams. A number of simple diagrammatic transformation rules are given, and the resulting reasoning system is shown to be sound and complete.

Type
Research Article
Information
LMS Journal of Computation and Mathematics , Volume 8 , 2005 , pp. 145 - 194
Copyright
Copyright © London Mathematical Society 2005

References

reference

1Dreban, B.,and Goldfarb, D, The decision problem. Solvable classes of quantificational formulas (Addison Wesley, 1979).Google Scholar
2Euler, L., Lettres a une princesse d‘Allemagne sur divers sujets de physique et de philosophie, vol. 2 (1761) Letters 102–108.Google Scholar
3Fish, A. and Flower, J., ‘Investigating reasoning with constraint diagrams‘, Proc. Visual Languages and Formal Methods (2004), Electron. Notes Theor. Comput. Sci. 127 (Elsevier, 2005) 53–69.Google Scholar
4Fish, A. and Howse, J., ‘Computing reading trees for constraint diagrams’, Proc. AGTIVE (2003)(Applications of Graph Transformations with Industrial Relevance, Charlottesville, Virginia) (Springer, 2003) 260–274.Google Scholar
5Fish, A. and Howse, J., ‘Towards a default reading for constraint diagrams’, Proc. Diagrams (2004) (International Conference on the Theory and Application of Diagrams,Cambridge), Lecture Notes in Artificial Intelligence 2980 (Springer, 2004) 51–65.Google Scholar
6Fish, A., Flower, J. and Howse, J., ‘A reading algorithm for constraint diagrams’, Proc. IEEE Symposium on Human Centric Computing Languages and Environments (Auckland, New Zealand, October 2003) (IEEE Computer Society Press, 2003) 161–168.Google Scholar
7Fish, A., Flower, J. and HOWSE, J., ‘The semantics of augmented constraint diagrams’, J. of Visual Languages and Computing, to appear (2005).CrossRefGoogle Scholar
8Fitting, M., First order logic and automated theorem proving (Springer, 1996).CrossRefGoogle Scholar
9Flower, J. and Howse, J., ‘Generating Euler diagrams’, Proc. Diagrams (2002) (International Conference on the Theory and Application of Diagrams), Lecture Notes in Artificial Intelligence 2317 (Springer, 2002) 61–75.Google Scholar
10Flower, J. and Stapleton, G., ‘Automated theorem proving with spider diagrams’, Proc. CATS (2004) (Computing: The Australasian Theory Symposium, Dunedin, New Zealand), Electron. Notes Theor. Comput. Sci. 91 (Science Direct, (2004) 116–132.Google Scholar
11Flower, J., Howse, J. and Taylor, J., ‘Nesting in Euler Diagrams: syntax, semantics and construction’, J. Software and Systems Modeling 3 (2004) 55–67.CrossRefGoogle Scholar
12Flower, J., Howse, J., Taylor, J. and Kent, S., ‘A visual framework for modelling with heterogeneous notations’, Proc. HCC (2002) (IEEE Symposium on Human Centric Computing Languages and Environments, Arlington) (IEEE Computer Society Press, 2002)71–73.Google Scholar
13Flower, J., Masthoff, J. and Stapleton, G., ‘Generating readable proofs: a heuristic approach to theorem proving with spider diagrams’, Proc. Diagrams (2004) (International Conference on the Theory and Application of Diagrams, Cambridge), Lecture Notes in Artificial Intelligence 2980 (Springer, 2004) 166–181.Google Scholar
14Flower, J., Masthoff, J. and Stapleton, G., ‘Generating proofs with spider diagrams using heuristics’, Proc. VLC (2004)10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing, San Francisco) (Knowledge Systems Institute, 2004) 279–285.Google Scholar
15Flower, J., Rodgers, P. and Mutton, P., ‘Layout metrics for Euler diagrams’, Proc. iV (2003) (7th International Conference on Information Visualisation, London) (IEEE Computer Society Press, 2003) 272–280.Google Scholar
16Gil, J., Howse, J. and Kent, S., ‘Constraint diagrams: a step beyond UML’, Proc. TOOLS USA (1999) (Santa Barbara, California) (IEEE Computer Society Press, 1999) 453–463.Google Scholar
17Gil, J., Howse, J. and Kent, S., ‘Formalising spider diagrams’, Proc. VL (1999) (IEEE Symposium on Visual Languages) (IEEE Computer Society Press, 1999) 130–137.Google Scholar
18Gil, J., Howse, J. and Kent, S., ‘Towards a formalization of constraint diagrams’, Proc. HCC 2001 (IEEE Symposium on Human-Centric Computing, Stresa) (IEEE Computer Society Press, 2001) 72–79.Google Scholar
19Hammer, E., Logic and visual information (CSLI Publ., 1995).Google Scholar
20Harel, D., ‘On visual formalisms’, Diagrammatic reasoning (ed. Glasgow, J., Narayan, N. H. and Chandrasekaran, B., MIT Press, 1998) 235–271Google Scholar
21Howse, J., Molina, F., Shin, S.-J. and Taylor, J., ‘Type-syntax and token-syntax in diagrammatic systems’, Proc. FOIS 2001 (2nd International Conference on Formal Ontology in Information Systems, Maine, USA) (ACM Press, 2001) 174–185.Google Scholar
22Howse, J., Molina, F., Shin, S.-J. and Taylor, J., ‘On diagram tokens and types’, Proc. Diagrams (2002) (International Conference on the Theory and Application of Diagrams), Lecture Notes in Artificial Intelligence 2317 (Springer, 2002) 76–90.Google Scholar
23Howse, J., Molina, F. and Taylor, J., ‘SD2: a sound and complete diagrammatic reasoning system’, Proc. ASC 2000 (Artificial Intelligence and Soft Computing, Banff) (IASTED/ACTA Press, 2000) 402–408.Google Scholar
24Howse, J., Molina, F. and Taylor, J., ‘On the completeness and expressiveness of spider diagram systems’, Proc. Diagrams 2000 (International Conference on the Theory and Application of Diagrams), Lecture Notes in Artificial Intelligence 1889 (Springer, 2000)26–41.Google Scholar
25Howse, J., Molina, F. and Taylor, J., ‘A sound and complete diagrammatic reasoning system’, Proc. VL 2000 (IEEE Symposium on Visual Languages, Seattle) (IEEE Computer Society Press, 2000) 127–136.Google Scholar
26Howse, J., Molina, F., Taylor, J. and Kent, S., ‘Reasoning with spider diagrams’,Proc. VL 1999 (IEEE Symposium on Visual Languages, Tokyo, Sept. 1999) (IEEE Computer Society Press) 138Proc. VL 1999 (IEEE Symposium on Visual Languages, Tokyo, Sept. 1999) (IEEE socity press 138–147Google Scholar
27Howse, J., Molina, F., Taylor, J., Kent, S. and Gil, J., ‘Spider diagrams: a diagrammatic reasoning system’, J. Visual Languages and Computing 12 (2001) 299–324CrossRefGoogle Scholar
28Kent, S., ‘Constraint diagrams: visualising invariants in object oriented models’, Proc. OOPSLA91, ACM SIGPLAN Notices 32 (1997) 327–341.CrossRefGoogle Scholar
29LEMON, O., ‘Comparing the efficacy of visual languages’, Words, proofs and diagrams (ed. Barker-Plummer, D., Beaver, D. I., Benthem, J. van and Luzio, P. Scotto di, CSLI Publications, 2002) 47–69.Google Scholar
30Lull, R., Ars magma (Lyons, 1517).Google Scholar
31Molina, F., ‘Reasoning with extended Venn-Peirce diagrammatic systems’, PhD Thesis, University of Brighton, (2001).Google Scholar
32Mutton, P., Rodgers, P. and Flower, J., ‘Drawing graphs in Euler Diagrams’, Proc.Diagrams (2004) (International Conference on the Theory and Application of Diagrams, Cambridge, March (2004), Lecture Notes in Artificial Intelligence 2980 (ed.Blackwell, A. et al. , Springer, 2004) 66–81.Google Scholar
33OBJECT MANAGEMENT GROUP,‘Unified Modeling Language specification’, availableatwww.omg.org.Google Scholar
34Peirce, C., Collected papers, vol. 4 (Harvard Univ. Press, 1933).Google Scholar
35Rodgers, P., Mutton, P. and Flower, J., ‘Dynamic Euler diagram drawing’, Proc. VLHCC 2004 (Visual Languages and Human Centric Computing, Rome) (IEEE Computer Society Press, 2004) 147–156.Google Scholar
36Luzio, P. Scotto Di, ‘Patching up a logic of Venn diagrams’, Proc. 6th CSLI Workshop on Logic, Language and Computation (CSLI Publications, Stanford, 2000).Google Scholar
37Shin, S.-J., The logical status of diagrams (Cambridge Univ. Press, 1994).Google Scholar
38Stapleton, G., ‘Reasoning with constraint diagrams’, PhD Thesis, University of Brighton, August (2004).Google Scholar
39Stapleton, G., Howse, J. and TAYLOR, J., ‘A constraint diagram reasoning system’, Proc. VLC (2003) (Distributed Multimedia Systems, International Conference on Visual Languages and Computing, Florida International University, Miami) (Knowledge Systems Institute, 2003) 263–270.Google Scholar
40Stapleton, G., Howse, J. and Taylor, J., ‘A decidable constraint diagram reasoning system’, J. Logic Comput., to appear 2005.CrossRefGoogle Scholar
41Stapledon, G., Howse, J., Taylor, J. and Thompson, S., What can spider diagrams say?’ Proc. Diagrams (2004) (International Conference on the Theory and Application of Diagrams, Cambridge, March 2004), Lecture Notes in Artificial Intelligence 2980 (ed. Blackwell, A., et al., Springer, 2004) 112–127.Google Scholar
42Stapleton, G., Thompson, S., Howse, J. and Taylor, J., ‘The expressiveness of spider diagrams’, J. Logic Comput. 14 (2004) 857–880.CrossRefGoogle Scholar
43Venn, J., ‘On the diagrammatic and mechanical representation of propositions and reasonings’, The London, Edinburgh and Dublin Philosophical Magazine and Journal of Science 9 (1880) 1–18.CrossRefGoogle Scholar
44Verroust, A. and Viaud, M.-L., ‘Ensuring the drawability of extended Euler diagrams for up to 8 sets’, Proc. Diagrams (2004) (International Conference on the Theory and Application of Diagrams, Cambridge, March 2004), Lecture Notes in Artificial Intelligence 2980 (ed. Blackwell, A., et al., Springer, 2004) 128–141.Google Scholar
45Warmer, J. and Kleppe, A., The Object Constraint Language: precise modeling with UML (Addison-Wesley, 1998).Google Scholar