Skip to main content
SpringerLink
Log in

A proof development system for the HOL theorem prover

  • Conference paper
  • First Online:
Higher Order Logic Theorem Proving and Its Applications (HUG 1993)

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

Included in the following conference series:

Abstract

In this paper, we present a system to improve the interaction between HOL and the user when doing proofs.

Supported by SERC grant GR/G 33837 and a grant from DSTO Australia

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. Y. Bertot, G. Kahn, L. Théry, “Proof by Pointing”, to be published.

    Google Scholar 

  2. R. J. Boulton, “The arithmetic decision procedure”, in the HOL system.

    Google Scholar 

  3. R. S. Boyer, J S. More, “A Computational Logic”, ACM Monograph Series, Academic Press, New York, 1979.

    Google Scholar 

  4. “The Centaur 1.3 Manual”, I. Jacobs, ed., available from INRIA-Sophia-Antipolis, January 1993.

    Google Scholar 

  5. E. Charniak, C. K. Riesbeck, D. V. McDermott, J. R. Meehan, “Artificial intelligence programming”, Lawrence Erlbaum Associates Publishers, New Jersey 1987.

    Google Scholar 

  6. T. W. Reps, T. Teitelbaum, “The Synthesizer generator: a system for constructing language-based editors”, Springer-Verlag, 1988.

    Google Scholar 

  7. B. T. Graham, “The SECD Microprocessor, A Verification Case Study”, Kluwer Academic Publishers, Boston, 1992.

    Google Scholar 

  8. S. Kalvala, “Developing an Interface for HOL”, in Proceedings of the '91 International Workshop on the HOL Theorem Proving System and its Applications, Davis, Cal., IEEE Computer Society Press, August 1991.

    Google Scholar 

  9. D. Shepherd, “The convert library”, in the HOL system.

    Google Scholar 

  10. L. Théry, Y. Bertot, G. Kahn, “Real Theorem Provers Deserve Real User-Interfaces”, in Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments, Tyson's Corner, Va, USA, Software Engineering Notes, Vol. 17, no. 5, ACM Press, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Cambridge Computer Laboratory, UK

    Laurent Théry

  2. INRIA, Sophia-Antipolis

    Laurent Théry

Authors
  1. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Théry, L. (1994). A proof development system for the HOL theorem prover. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_129

Download citation

  • DOI: https://doi.org/10.1007/3-540-57826-9_129

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57826-0

  • Online ISBN: 978-3-540-48346-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation