Skip to main content
SpringerLink
Log in

System description: An interface between CLAM and HOL

  • Conference paper
  • First Online:
Automated Deduction — CADE-15 (CADE 1998)

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

Included in the following conference series:

Abstract

The CLAM proof planner has been interfaced to the HOL interactive theorem prover to provide the power of proof planning to people using HOL for formal verification, etc. The interface sends HOL goals to CLAM for planning and translates plans back into HOL tactics that solve the initial goals. The project homepage can be found at http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/intro.html.

Research supported by the Engineering and Physical Sciences Research Council of Great Britain under grants GR/L03071 and GR/L14381.

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. J. Boulton. Combining decision procedures in the HOL system. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 971 of Lecture Notes in Computer Science. Springer, 1995.

    Google Scholar 

  2. R. Boulton, A. Bundy, K. Slind, and M. Gordon. A Prototype Interface between CLAM and HOL. Research Paper 854, Department of Artificial Intelligence, University of Edinburgh, June 1997.

    Google Scholar 

  3. A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7(3):303–324, 1991.

    Article  MathSciNet  Google Scholar 

  4. A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In Proceedings of the 14th International Conference on Automated Deduction (CADE-I4), volume 1249 of Lecture Notes in Artificial Intelligence. Springer, 1997.

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge, USA

    Konrad Slind & Mike Gordon

  2. Department of Artificial Intelligence, University of Edinburgh, USA

    Richard Boulton & Alan Bundy

Authors
  1. Konrad Slind
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mike Gordon
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Richard Boulton
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alan Bundy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Slind, K., Gordon, M., Boulton, R., Bundy, A. (1998). System description: An interface between CLAM and HOL. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054255

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation