Skip to main content
SpringerLink
Log in

Recording HOL proofs in a structured browsable format

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1349))

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Back, J. Grundy, and J. von Wright. Structured calculational proof. Joint Computer Science Technical Report TR-CS-96-09, The Australian National University, Department of Computer Science, Canberra ACT 0200, Australia, 1996.

    Google Scholar 

  2. R.-J. R. Back. On correct refinement of programs. J. Comput. Syst. Sci., 23(1):49–68, 1981.

    Google Scholar 

  3. M. Butler, J. Grundy, T. Långbacka, R. Rukšėnas, and J. von Wright. The refinement calculator: Proof support for program refinement. In Groves and Reeves, editors, Formal Methods Pacific'97: Proceedings of FMP'97, Discrete Mathematics and Theoretical Computer Science, pages 40–61, Wellington, New Zealand, 1997. Springer-Verlag.

    Google Scholar 

  4. M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge, England, 1993.

    Google Scholar 

  5. D. Gries and F. B. Schneider. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag, New York, 1993.

    Google Scholar 

  6. J. Grundy. A browsable format for proof presentation. Mathesis Universalis, 1(2), 1996.

    Google Scholar 

  7. J. Grundy. Transformational hierarchical reasoning. Comput. J., 39(4):291–302, 1996.

    Google Scholar 

  8. T. Långbacka, R. Rukšėnas, and J. von Wright. TkWinHOL: A tool for doing window inference in HOL. In Schubert, Windley, and Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, volume 971 of LNCS, pages 245–260, Aspen Grove, Utah, 1995. Springer-Verlag.

    Google Scholar 

  9. P. J. Robinson and J. Staples. Formalizing a hierarchical structure of practical mathematical reasoning. J. Logic Comput., 3(1):47–61, 1993.

    Google Scholar 

  10. A. Trybulec and H. A. Blair. Computer aided reasoning. In Parikh, editor, Logic of Programs, volume 193 of LNCS, pages 406–412, New York, 1985. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Australian National University, Australia

    Jim Grundy

  2. Department of Computer Science, University of Helsinki, Finland

    Thomas Långbacka

  3. Turku Centre for Computer Science-TUCS, Finland

    Thomas Långbacka

Authors
  1. Jim Grundy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Långbacka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Johnson

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grundy, J., Långbacka, T. (1997). Recording HOL proofs in a structured browsable format. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000500

Download citation

  • DOI: https://doi.org/10.1007/BFb0000500

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63888-9

  • Online ISBN: 978-3-540-69661-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation