Advertisement

An interface between CLAM and HOL

  • Richard Boulton
  • Konrad Slind
  • Alan Bundy
  • Mike Gordon
Refereed Papers
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Theorem Prove Abstract Syntax Induction Scheme High Order Logic Concrete Syntax 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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.zbMATHMathSciNetCrossRefGoogle Scholar
  7. 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.zbMATHMathSciNetCrossRefGoogle Scholar
  8. 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. 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. 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. 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. 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. 13.
    L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  14. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Richard Boulton
    • 1
  • Konrad Slind
    • 2
  • Alan Bundy
    • 1
  • Mike Gordon
    • 2
  1. 1.Department of Artificial IntelligenceUniversity of EdinburghEdinburghScotland
  2. 2.University of Cambridge Computer LaboratoryCambridgeEngland

Personalised recommendations