Skip to main content
SpringerLink
Log in

Modular Reasoning in Isabelle

  • Conference paper
Automated Deduction - CADE-17 (CADE 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1831))

Included in the following conference series:

Abstract

The concept of locales for Isabelle enables local definition and assumption for interactive mechanical proofs. Furthermore, dependent types are constructed in Isabelle/HOL for first class representation of structure. These two concepts are introduced briefly. Although each of them has proved useful in itself, their real power lies in combination. This paper illustrates by examples from abstract algebra how this combination works and argues that it enables modular reasoning.

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. Bailey, A.: The Machine-Checked Literate Formalisation of Algebra in Type Theory. PhD thesis. University of Manchester (1998)

    Google Scholar 

  2. Dowek, G. et al.: The Coq proof assistant user’s guide. Technical Report 154, INRIA-Rocquencourt (1993)

    Google Scholar 

  3. de Bruijn, N.G.: A Survey of the Project AUTOMATH. In: Seldin and Hindley [SH80], pp. 579–606

    Google Scholar 

  4. Dowek,G.: Naming and Scoping in a Mathematical Vernacular. Technical Report 1283, INRIA, Rocquencourt (1990)

    Google Scholar 

  5. Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning 11, 213–248 (1993)

    Article  MATH  Google Scholar 

  6. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  7. Gunter, E. L.: Doing Algebra in Simple Type Theory. Technical Report MS-CIS-89-38, Dep. of Computer and Information Science. University of Pennsylvania (1989)

    Google Scholar 

  8. Gunter, E.L.: The Implementation and Use of Abstract Theories in HOL. In: Third HOL Users Meeting. Aarhus University (1990)

    Google Scholar 

  9. Howard, W.A.: The formulae-as-types notion of construction. In: Seldin and Hindley [SH80], pp. 479–490

    Google Scholar 

  10. Jacobs, B., Melham, T.F.: Translating Dependent Type Theory into Higher Order Logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993)

    Google Scholar 

  11. Kammüller, F.: Modular Reasoning in Isabelle. PhD thesis. University of Cambridge, Technical Report 470 (1999)

    Google Scholar 

  12. Kammüller, F.: Modular Structures as Dependent Types in Isabelle. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, p. 121. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Kammüller, F., Paulson, L.C.: A Formal Proof of Sylow’s First Theorem – An Experiment in Abstract Algebra with Isabelle HOL. Journal of Automated Reasoning 23(3-4), 235–264 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  14. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales – a Sectioning Concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, p. 149. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  15. Luo, Z., Pollack, R.: Lego proof development system: User’s manual. Technical Report ECS-LFCS-92-211. University of Edinburgh (1992)

    Google Scholar 

  16. MacQueen, D.B.: Using Dependant Types to Express Modular Structures. In: Proc. 13th ACM Symp. Principles Programming Languages. ACM Press, New York (1986)

    Google Scholar 

  17. Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Part of the PVS Manual. Available on the Web as, http://www.csl.sri.com/pvsweb/manuals.html (September 1998)

  18. Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

  19. Seldin, J.P., Hindley, J.R. (eds.): To H. B. Curry: Essays on Combinatory Logic. Academic Press Limited, London (1980)

    MATH  Google Scholar 

  20. Trybulec, A.: Some Features of the Mizar Language (1993), Available from Mizar user’s group

    Google Scholar 

  21. Yu, Y.: Computer Proofs in Group Theory. Journal of Automated Reasoning 6, 251–286 (1990)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. GMD First, 12489, Berlin, Germany

    Florian Kammüller

Authors
  1. Florian Kammüller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

    David McAllester

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kammüller, F. (2000). Modular Reasoning in Isabelle. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_7

Download citation

  • DOI: https://doi.org/10.1007/10721959_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67664-5

  • Online ISBN: 978-3-540-45101-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation