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.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
R. S. Boyer and J. S. Moore. A Computational Logic Handbook, volume 23 of Perspectives in Computing. Academic Press, San Diego, 1988.
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.
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.
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.
A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In McCune [12], pages 351–365.
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.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
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.
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.
L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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