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 implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R.J. Boulton, “On efficiency in theorem provers which fully expand proofs into primitive inferences,” Technical Report 248, University of Cambridge Computer Laboratory, 1992.
Robert S. Boyer and Gilles Dowek, “Towards checking proof checkers,” in Workshop on Types for Proofs and Programs (Type '93), 1993.
A. Cohn, “The notion of proof in hardware verification,” Journal of Automated Reasoning, Vol. 5,No. 2, pp. 127–139, June 1989.
Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1996.
James H. Fetzer, “Program verification: the very idea,” Communications of the ACM, Vol. 31,No. 9, pp. 1048–1063, Sept. 1988.
M.J.C. Gordon, “LCF_LSM, A system for specifying and verifying hardware,” Technical Report 41, University of Cambridge Computer Laboratory, 1983.
M.J.C. Gordon and T.F. Melham (Eds.), Introduction to HOL-A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science No. 78, Springer-Verlag, 1979.
Ministry of Defence, Requirements for the Procurement of Safety-Critical Software in Defence Equipment, Interim Standard 00–55, April 1991.
Shari L. Pfleeger and Les Hatton, “Investigating the influence of formal methods,” IEEE Computer, Vol. 30,No. 2, pp. 33–43, Feb. 1997.
D. Syme, “Reasoning with the formal definition of standard ML in HOL,” Higher Order Logic Theorem Proving and its Applications, Lecture Notes in Computer Science No. 780, Springer-Verlag, 1993, pp. 43–58.
M. VanInwegen and E. Gunter, “HOL-ML,” Higher Order Logic Theorem Proving and its Applications, Lecture Notes in Computer Science No. 780, Springer-Verlag, 1993, pp. 59–72.
J. von Wright, “Representing higher-order logic proofs in HOL,” Technical Report 323, University of Cambridge Computer Laboratory, Jan. 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, “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: A HOL system library manual, Computer Laboratory, University of Cambridge, 1994.
W. Wong, “A proof checker for HOL proofs,” Technical Report 389, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, 1995.
W. Wong and P. Curzon, “Towards an efficient proof recorder for HOL90,” in Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logic:TPHOL '97, 1997.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Wong, W. Validation of HOL Proofs by Proof Checking. Formal Methods in System Design 14, 193–212 (1999). https://doi.org/10.1023/A:1008643803725
Issue Date:
DOI: https://doi.org/10.1023/A:1008643803725