Abstract
Diagrammatic reasoning can be described formally by a number of diagrammatic logics; spider diagrams are one of these, and are used for expressing logical statements about set membership and containment. Here, existing work on spider diagrams is extended to include constant spiders that represent specific individuals. We give a formal syntax and semantics for the extended diagram language before introducing a collection of reasoning rules encapsulating logical equivalence and logical consequence. We prove that the resulting logic is sound, complete and decidable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Since all constructs discussed here are abstract, we will use the terminology ‘zone’ rather than ‘abstract zone’ throughout.
- 2.
However, for any diagram that incorporated such ties it is possible to define a semantically equivalent diagram that does not contain such ties. This is not the case for ties between constant spiders. It is straightforward to extend the work in this paper to the case where these additional types of tie are permitted.
References
Chow, S., Ruskey, F.: Drawing area-proportional Venn and Euler diagrams. In: Proceedings of Graph Drawing 2003, Perugia, Italy. LNCS, vol. 2912, pp. 466–477. Springer, Berlin (2003)
Clark, R.: Failure mode modular de-composition using spider diagrams. In: Proceedings of Euler Diagrams 2004. Electronic Notes in Theor. Comput. Sci., vol. 134, pp. 19–31 (2005)
De Chiara, R., Erra, U., Scarano, V.: VennFS: a Venn diagram file manager. In: Proceedings of Information Visualisation, pp. 120–126. IEEE Comput. Soc., Los Alamitos (2003)
Euler, L.: Lettres a une princesse d’Allemagne sur divers sujets de physique et de philosophie. Opera Omnia 2, 102–108 (1775)
Flower, J., Howse, J.: Generating Euler diagrams. In: Proceedings of 2nd International Conference on the Theory and Application of Diagrams, Georgia, USA, pp. 61–75. Springer, Callaway Gardens (2002)
Flower, J., Masthoff, J., Stapleton, G.: Generating proofs with spider diagrams using heuristics. In: Proceedings of Distributed Multimedia Systems, International Workshop on Visual Languages and Computing, pp. 279–285. Knowledge Systems Institute, San Francisco (2004)
Flower, J., Masthoff, J., Stapleton, G.: Generating readable proofs: a heuristic approach to theorem proving with spider diagrams. In: Proceedings of 3rd International Conference on the Theory and Application of Diagrams, Cambridge, UK. LNAI, vol. 2980, pp. 166–181. Springer, Berlin (2004)
Gurr, C.: Aligning syntax and semantics in formalisations of visual languages. In: Proceedings of IEEE Symposia on Human-Centric Computing Languages and Environments, pp. 60–61. IEEE Comput. Soc., Los Alamitos (2001)
Hayes, P., Eskridge, T., Saavedra, R., Reichherzer, T., Mehrotra, M., Bobrovnikoff, D.: Collaborative knowledge capture in ontologies. In: Proceedings of the 3rd International Conference on Knowledge Capture, pp. 99–106 (2005)
Howse, J., Molina, F., Shin, S.-J., Taylor, J.: Type-syntax and token-syntax in diagrammatic systems. In: Proceedings FOIS-2001: 2nd International Conference on Formal Ontology in Information Systems, Maine, USA, pp. 174–185. ACM, New York (2001)
Howse, J., Molina, F., Taylor, J., Kent, S., Gil, J.: Spider diagrams: a diagrammatic reasoning system. J. Vis. Lang. Comput. 12(3), 299–324 (2001)
Howse, J., Stapleton, G., Taylor, J.: Spider diagrams. LMS J. Comput. Math. 8, 145–194 (2005)
Howse, J., Stapleton, G., Taylor, K., Chapman, P.: Visualizing ontologies: a case study. In: International Semantic Web Conference 2011. Springer, Bonn (2011)
Kent, S.: Constraint diagrams: visualizing invariants in object oriented modelling. In: Proceedings of OOPSLA97, pp. 327–341. ACM, New York (1997)
Kestler, H., Muller, A., Kraus, J., Buchholz, M., Gress, T., Kane, D., Zeeberg, B., Weinstein, J.: VennMaster: area-proportional Euler diagrams for functional go analysis of microarrays. BMC Bioinformatics 9(67) (2008)
Lovdahl, J.: Towards a visual editing environment for the languages of the semantic web. PhD thesis, Linkoping University (2002)
Mutton, P., Rodgers, P., Flower, J.: Drawing graphs in Euler diagrams. In: Proceedings of 3rd International Conference on the Theory and Application of Diagrams, Cambridge, UK. LNAI, vol. 2980, pp. 66–81. Springer, Berlin (2004)
Oliver, I., Howse, J., Stapleton, G., Nuutila, E., Törmä, S.: Visualising and specifying ontologies using diagrammatic logics. In: 5th Australasian Ontologies Workshop. Conf. Res. Pract. Inf. Technol., vol. 112. CRPIT, Melbourne (2009)
Rodgers, P., Zhang, L., Fish, A.: General Euler diagram generation. In: International Conference on Theory and Applications of Diagrams, pp. 13–27. Springer, Herrsching (2008)
Shimojima, A.: Inferential and expressive capacities of graphical representations: survey and some generalizations. In: Proceedings of 3rd International Conference on the Theory and Application of Diagrams, Cambridge, UK. LNAI, vol. 2980, pp. 18–21. Springer, Berlin (2004)
Stapleton, G.: Spider diagrams augmented with constants: a complete system. In: Visual Languages and Computing, pp. 292–299 (2008)
Stapleton, G., Delaney, A.: Evaluating and generalizing constraint diagrams. J. Vis. Lang. Comput. 19(4), 499–521 (2008)
Stapleton, G., Thompson, S., Howse, J., Taylor, J.: The expressiveness of spider diagrams. J. Log. Comput. 14(6), 857–880 (2004)
Stapleton, G., Masthoff, J., Flower, J., Fish, A., Southern, J.: Automated theorem proving in Euler diagrams systems. J. Autom. Reason. 39, 431–470 (2007)
Stapleton, G., Taylor, J., Howse, J., Thompson, S.: The expressiveness of spider diagrams augmented with constants. J. Vis. Lang. Comput. 20(1), 30–49 (2009)
Stapleton, G., Rodgers, P., Howse, J., Zhang, L.: Inductively generating Euler diagrams. IEEE Trans. Vis. Comput. Graph. 17(1), 88–100 (2011)
Swoboda, N., Allwein, G.: Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference. J. Softw. Syst. Model. 3(2), 136–149 (2004)
Zhao, Y., Lövdahl, J.: A reuse based method of developing the ontology for e-procurement. In: Proceedings of the Nordic Conference on Web Services, pp. 101–112 (2003)
Acknowledgement
This work is supported by the UK EPSRC grant “Defining Regular Languages with Diagrams” [EP/H012311/1].
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer Basel
About this chapter
Cite this chapter
Stapleton, G., Howse, J., Thompson, S., Taylor, J., Chapman, P. (2013). On the Completeness of Spider Diagrams Augmented with Constants. In: Moktefi, A., Shin, SJ. (eds) Visual Reasoning with Diagrams. Studies in Universal Logic. Birkhäuser, Basel. https://doi.org/10.1007/978-3-0348-0600-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-0348-0600-8_7
Publisher Name: Birkhäuser, Basel
Print ISBN: 978-3-0348-0599-5
Online ISBN: 978-3-0348-0600-8
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)