Skip to main content
SpringerLink
Log in

Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers

  • Conference paper
Interactive Theorem Proving (ITP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6898))

Included in the following conference series:

Abstract

We present an interactive heterogeneous theorem proving framework, which performs formal reasoning by arbitrarily mixing diagrammatic and sentential proof steps.

We use Isabelle to enable formal reasoning with either traditional sentences or spider diagrams. We provide a mechanisation of the theory of abstract spider diagrams and establish a formal link between diagrammatic concepts and the existing theories in Isabelle/HOL.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barker-Plummer, D., Etchemendy, J., Liu, A., Murray, M., Swoboda, N.: Openproof - A Flexible Framework for Heterogeneous Reasoning. In: Stapleton, G., Howse, J., Lee, J. (eds.) Diagrams 2008. LNCS (LNAI), vol. 5223, pp. 347–349. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Barwise, J., Etchemendy, J.: A Computational Architecture for Heterogeneous Reasoning. In: TARK, pp. 1–11. Morgan Kaufmann, San Francisco (1998)

    Google Scholar 

  3. Gil, J., Howse, J., Kent, S.: Towards a Formalization of Constraint Diagrams. In: IEEE Symposia on Human-Centric Computing Languages and Environments, p. 72 (2001)

    Google Scholar 

  4. Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  5. Hammer, E.: Reasoning with Sentences and Diagrams. NDJFL 35(1), 73–87 (1994)

    MathSciNet  MATH  Google Scholar 

  6. Howse, J., Molina, F., Taylor, J., Kent, S., Gil, J.: Spider Diagrams: A Diagrammatic Reasoning System. JVLC 12(3), 299–324 (2001)

    Google Scholar 

  7. Howse, J., Stapleton, G., Taylor, J.: Spider Diagrams. LMS JCM 8, 145–194 (2005)

    MathSciNet  MATH  Google Scholar 

  8. Jamnik, M., Bundy, A., Green, I.: On Automating Diagrammatic Proofs of Arithmetic Arguments. JOLLI 8(3), 297–321 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  9. Shin, S.-J.: Heterogeneous Reasoning and its Logic. BSL 10(1), 86–106 (2004)

    MathSciNet  MATH  Google Scholar 

  10. Stapleton, G., Masthoff, J., Flower, J., Fish, A., Southern, J.: Automated Theorem Proving in Euler Diagram Systems. JAR 39(4), 431–470 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. Stapleton, G., Taylor, J., Thompson, S., Howse, J.: The expressiveness of spider diagrams augmented with constants. JVLC 20(1), 30 (2009)

    MATH  Google Scholar 

  12. Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Winterstein, D., Bundy, A., Gurr, C.: Dr.Doodle: A diagrammatic theorem prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 331–335. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Cambridge, UK

    Matej Urbas & Mateja Jamnik

Authors
  1. Matej Urbas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mateja Jamnik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculteit Informatica, Open Universiteit, Postbus 2960, Heerlen, 6401 DL, The Netherlands

    Marko van Eekelen

  2. FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Postbus 9010, 6500 GL, Nijmegen, The Netherlands

    Herman Geuvers  & Freek Wiedijk  & 

  3. Faculteit Informatica, Open Universiteit, Postbus 2960, 6401 DL, Heerlen, The Netherlands

    Julien Schmaltz

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Urbas, M., Jamnik, M. (2011). Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds) Interactive Theorem Proving. ITP 2011. Lecture Notes in Computer Science, vol 6898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22863-6_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22863-6_29

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22862-9

  • Online ISBN: 978-3-642-22863-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation