Abstract
Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an efficient proof checker which is able to check a practical proof consisting of thousands of inference steps.
The work described in this paper was carried out by the author while he was in the University of Cambridge Computer Laboratory supported by a grant from SERC (No. GR/G223654)
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Robert S. Boyer and Gilles Dowek. Towards checking proof checkers. In Workshop on types for proofs and programs (Type '93). 1993.
R. J. Boulton. On efficiency in theorem provers which fully expand proofs into primitive inferences. Technical Report 248, University of Cambridge Computer Laboratory, 1992.
Constable et al. Implementing Mathematics with the Nuprl proof development system. Prentice-Hall, 1996.
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. C. Gordon. LCF_LSM, A system for specifying and verifying hardware. Technical Report 41, University of Cambridge Computer Laborartory, 1983.
Ministry of Defence. Requirements for the procurement of safety-critical software in defence equipment. Interim Standard 00–55, April 1991.
D. Syme. Reasoning with the formal definition of standard ML in HOL. In Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science No. 780, pages 43–58. Springer-Verlag, 1993.
M. VanInwegen and E. Gunter. HOL-ML, In Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science No. 780, pages 59–72. Springer-Verlag, 1993.
J. von Wright. Representing higher order logic proofs in HOL. In Thomas F. Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, volume 859 of Lecture Notes in Computer Science, pages 456–470. Springer-Verlag, September 1994.
J. von Wright. Program refinement by theorem prover. In Proceedings of the 6th Refinement workshop, Lecture Notes in Computer Science. Springer-Verlag, 1995.
W. Wong. Formal verification of VIPER's ALU. Technical Report 300, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, ENGLAND, May 1993.
W. Wong. Recording HOL proofs. Technical Report 306, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, ENGLAND, July 1993.
W. Wong. The HOL record_proof Library. Computer Laboratory, University of Cambridge, 1994.
W. Wong. A proof checker for HOL proofs. Technical report, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, ENGLAND, 1995. to be published as technical report.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wong, W. (1995). Recording and checking HOL proofs. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_76
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_76
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive