Abstract
Proof management is an important issue for interactive theorem provers. We describe a simple proof manager that derives a large measure of its power from being parameterized by structures that separately manage 1) proof-specific information and 2) the relationships between proofs. Examples of its use include mixed forward and backward proof, automatic proof logging and replay, support for documenting a proof either before, during, or after the proof effort, and the management of proof dependencies.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andrew Appel and David MacQueen. Separate compilation for standard ML. Technical Report CS-TR-452-94, Princeton University, Princeton, New Jersey, 1994. To appear in PLDI'94.
Peter Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.
R. D. Arthan. A report on icl hol. In Phillip Windley, Myla Archer, Karl Levitt, and Jeffrey Joyce, editors, International Tutorial and Workshop on the HOL theorem proving system and it Applications, University of California at Davis, August 1991. ACM-SIGDA / IEEE Computer Society, IEEE Computer Society Press.
Yves Bertot. A canonical calculus of residuals. In G. Huet and G. Plotkin, editors, Logical Environments, pages 146–163. Cambridge Univeristy Press, 1993.
Robert Constable, S. Allen, H. Bromly, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith. Implementing Mathematics With the Nuprl Proof Development System. Prentice-Hall, New Jersey, 1986.
William Farmer. Theory interpretation in simple type theory. In Proceeding of the International Workshop on Higher-Order Algebra, Logic, and Term Rewriting (HOA '93), Amsterdam, The Netherlands, 1994. Springer-Verlag (LNCS).
George Fink, Myla Archer, and Lie Yang. Pm: A proof manager for HOL and other provers. In Phillip Windley, Myla Archer, Karl Levitt, and Jeffrey Joyce, editors, International Tutorial and Workshop on the HOL theorem proving system and it Applications, University of California at Davis, August 1991. ACM-SIGDA / IEEE Computer Society, IEEE Computer Society Press.
Mike Gordon and Tom Melham. Introduction to HOL, a theorem proving environment for higher order logic. Cambridge University Press, 1993.
Jim Grundy. Window inference in the HOL system. In Phillip Windley, Myla Archer, Karl Levitt, and Jeffrey Joyce, editors, International Tutorial and Workshop on the HOL theorem proving system and it Applications, University of California at Davis, August 1991. ACM-SIGDA / IEEE Computer Society, IEEE Computer Society Press.
M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In Mark Stickel, editor, Proceedings of the Tenth International Conference on Automated Deduction, LNAI 449, pages 1–15, Kaiserslautern, 1990.
Saraswati Kalvala, Myla Archer, and Karl Levitt. Implementation and use of annotations in HOL. In L. Claesen and M. Gordon, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, September 1992. IFIP TC10/WG10.2, Elsevier Science Publishers.
Leslie Lamport. How to write a proof. Technical Report 94, DEC Systems Research Center, Palo Alto, California, February 1993.
S. Owre, J. Rushby, N. Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: some lessons learned. In J. Woodcock and P. Larsen, editors, FME'93: Industrial Strength Formal Methods (LNCS 670), pages 482–500, Odense Denmark, 1993.
Lawrence Paulson. Logic and Computation: Interactive Proof With Cambridge LCF. Cambridge University Press, 1987.
Lawrence Paulson. ML for the working programmer. Cambridge University Press, 1991.
[TLP+93] Bent Thomsen, Lone Leth, Sanjiva Prasad, Tsung-Min Kuo, Andre Kramer, Fritz Knabe, and Alesasndro Giacalone. Facile Antigua release programming guide. Technical Report ECRC-93-20, European Computer-Industry Research Centre, Munich, Germany, December 1993.
L. Thery, Y.Bertot, and G. Kahn. Real theorem provers deserve real userinterfaces. In Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments (Software Engineering Notes), volume 17, pages 365–380, Tyson's Corner, Virginia USA, 1992. ACM Press.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Slind, K. (1994). A parameterized proof manager. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_57
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_57
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive