Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 1998: Theorem Proving in Higher Order Logics pp 87–104Cite as

An interface between CLAM and HOL

  • Refereed Papers
  • Conference paper
  • First Online:

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

Abstract

This paper describes an interface between the CLAM proof planner and the HOL interactive theorem prover. The interface sends HOL goals to CLAM for planning, and translates plans back into HOL tactics that solve the initial goals. The combined system is able to automatically prove a number of theorems involving recursively defined functions.

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. ΩMega: Towards a mathematical assistant. In McCune [12]., pages 252–255.

    Google Scholar 

  2. 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, Aspen Grove, Utah, USA, September 1995. Springer-Verlag.

    Google Scholar 

  3. R. J. Boulton. Syn: A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty-printing. Technical Report 390, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, UK, March 1996.

    Google Scholar 

  4. R. S. Boyer and J. S. Moore. A Computational Logic Handbook, volume 23 of Perspectives in Computing. Academic Press, San Diego, 1988.

    Google Scholar 

  5. A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The OYSTER-CLAM system. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 647–648, Kaiserslautern, FRG, July 1990. Springer-Verlag.

    Google Scholar 

  6. A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185–253, 1993.

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  8. A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In McCune [12], pages 351–365.

    Google Scholar 

  9. F. Giunchiglia, P. Pecchiari, and C. Talcott. Reasoning theories — towards an architecture for open mechanized reasoning systems. In F. Baader and K. U. Schulz, editors, Proceedings of the First International Workshop on Frontiers of Combining Systems (FroCoS'96), volume 3 of Applied Logic Series, pages 157–174, Munich, Germany, March 1996. Kluwer Academic Publishers.

    Google Scholar 

  10. 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 

  11. M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    Google Scholar 

  12. W. McCune, editor. Proceedings of the 14th International Conference on Automated Deduction (CADE-14), volume 1249 of Lecture Notes in Artificial Intelligence, Townsville, North Queensland, Australia, July 1997. Springer.

    Google Scholar 

  13. L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  14. K. Slind. Function Definition in Higher Order Logic. In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer-Verlag.

    Google Scholar 

  15. K. Slind. Derivation and Use of Induction Schemes in Higher-Order Logic. In Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97), volume 1275 of Lecture Notes in Computer Science, Murray Hill, New Jersey, USA, August 1997. Springer-Verlag.

    Google Scholar 

  16. N. Shankar PVS: Combining Specification, Proof Checking, and Model Checking. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, USA, November 1996, pages 257–264. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Artificial Intelligence, University of Edinburgh, 80 South Bridge, EH1 1HN, Edinburgh, Scotland

    Richard Boulton & Alan Bundy

  2. University of Cambridge Computer Laboratory, New Museums Site, CB2 3QG, Cambridge, England

    Konrad Slind & Mike Gordon

Authors
  1. Richard Boulton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Konrad Slind
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alan Bundy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mike Gordon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boulton, R., Slind, K., Bundy, A., Gordon, M. (1998). An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055131

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation