Abstract
The HOL system is afully expansive theorem prover: proofs generated in the system are composed of applications of the primitive inference rules of the underlying logic. One can have a high degree of confidence that such systems are sound, but they are far slower than theorem provers that exploit metatheoretic or derived properties.
This paper presents techniques for postponing part of the computation so that the user of a fully expansive theorem prover can be more productive. The notions oflazy theorem andlazy conversion are introduced. These not only allow part of the computation to be delayed, but also permit nonlocal optimizations that are only possible because the primitive inferences are not performed immediately. The approach also opens the way to proof procedures that exploit metatheoretic properties without sacrificing security; the primitive inferences still have to be performed in order to generate a theorem, but during the proof development the user is free of the overheads they entail.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
D.R. Musser. Report on the HOL (Higher Order Logic) proof checker. Computer Science Department, Rensselaer Polytechnic Institute, 1989.
M.J. Gordon, A.J. Milner, and C.P. Wadsworth.Edinburgh LCF: A Mechanised Logic of Computation, volume 78 ofLecture Notes in Computer Science, Springer-Verlag, 1979.
M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth. A metalanguage for interactive proof in LCF. InProceedings of the 5th ACM Conference on Principles of Programming Languages, Tuscon, Arizona, January, 1978, 119–130.
M.J.C. Gordon and T.F. Melham (eds.).Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
R.L. Constable, et al.Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.
L.C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge Computer Laboratory, January, 1993.
A. Chruch. A formulation of the simple theory of types.Journal of Symbolic Logic, 5:56–68, 1940.
S.L. Peyton Jones.The Implementation of Functional Programming Languages. International Series in Computer Science. Prentice-Hall, 1987.
L. Paulson. A higher-order implementation of rewriting.Science of Computer Programming, 3:119–149, 1983.
J. Camilleri. Symbolic compilation and execution of programs by proof: A case study in HOL. Technical Report 240, University of Cambridge Computer Laboratory, December, 1991.
R.S. Boyer and JS. Moore.A Computational Logic Handbook, Vol. 23 ofPerspectives in Computing, Academic Press, San Diego, 1988.
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.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Boulton, R.J. Lazy techniques for fully expansive theorem proving. Form Method Syst Des 3, 25–47 (1993). https://doi.org/10.1007/BF01383983
Issue Date:
DOI: https://doi.org/10.1007/BF01383983