Skip to main content
SpringerLink
Log in

On the Completeness of Spider Diagrams Augmented with Constants

  • Chapter
Visual Reasoning with Diagrams

Part of the book series: Studies in Universal Logic ((SUL))

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Since all constructs discussed here are abstract, we will use the terminology ‘zone’ rather than ‘abstract zone’ throughout.

  2. 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

  1. 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)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. Euler, L.: Lettres a une princesse d’Allemagne sur divers sujets de physique et de philosophie. Opera Omnia 2, 102–108 (1775)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Article  Google Scholar 

  12. Howse, J., Stapleton, G., Taylor, J.: Spider diagrams. LMS J. Comput. Math. 8, 145–194 (2005)

    MathSciNet  MATH  Google Scholar 

  13. Howse, J., Stapleton, G., Taylor, K., Chapman, P.: Visualizing ontologies: a case study. In: International Semantic Web Conference 2011. Springer, Bonn (2011)

    Google Scholar 

  14. Kent, S.: Constraint diagrams: visualizing invariants in object oriented modelling. In: Proceedings of OOPSLA97, pp. 327–341. ACM, New York (1997)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. Lovdahl, J.: Towards a visual editing environment for the languages of the semantic web. PhD thesis, Linkoping University (2002)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. Stapleton, G.: Spider diagrams augmented with constants: a complete system. In: Visual Languages and Computing, pp. 292–299 (2008)

    Google Scholar 

  22. Stapleton, G., Delaney, A.: Evaluating and generalizing constraint diagrams. J. Vis. Lang. Comput. 19(4), 499–521 (2008)

    Article  Google Scholar 

  23. Stapleton, G., Thompson, S., Howse, J., Taylor, J.: The expressiveness of spider diagrams. J. Log. Comput. 14(6), 857–880 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  24. Stapleton, G., Masthoff, J., Flower, J., Fish, A., Southern, J.: Automated theorem proving in Euler diagrams systems. J. Autom. Reason. 39, 431–470 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  25. 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)

    Article  Google Scholar 

  26. Stapleton, G., Rodgers, P., Howse, J., Zhang, L.: Inductively generating Euler diagrams. IEEE Trans. Vis. Comput. Graph. 17(1), 88–100 (2011)

    Article  Google Scholar 

  27. 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)

    Article  Google Scholar 

  28. 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)

    Google Scholar 

Download references

Acknowledgement

This work is supported by the UK EPSRC grant “Defining Regular Languages with Diagrams” [EP/H012311/1].

Author information

Authors and Affiliations

  1. Visual Modelling Group, University of Brighton, Brighton, UK

    Gem Stapleton, John Howse, John Taylor & Peter Chapman

  2. School of Computing, University of Kent, Canterbury, UK

    Simon Thompson

Authors
  1. Gem Stapleton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Howse
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Simon Thompson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. John Taylor
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Peter Chapman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gem Stapleton .

Editor information

Editors and Affiliations

  1. IRIST, Université de Strasbourg, Rue de l'Université 7, Strasbourg, 67000, France

    Amirouche Moktefi

  2. Department of Philosophy, Yale University, Hillhouse Avenue 38, New Haven, 06511, Connecticut, USA

    Sun-Joo Shin

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation