Abstract
We describe the key features of the proof description language of Declare, an experimental theorem prover for higher order logic. We take a somewhat radical approach to proof description: proofs are not described with tactics but by using just three expressive outlining constructs. The language is “declarative” because each step specifies its logical consequences, i.e. the constants and formulae that are introduced, independently of the justification of that step. Logical constants and facts are lexically scoped in a style reminiscent of structured programming. The style is also heavily “inferential”, because Declare relies on an automated prover to eliminate much of the detail normally made explicit in tactic proofs. Declare has been partly inspired by Mizar, but provides better automation. The proof language has been designed to take advantage of this, allowing proof steps to be both large and controlled. We assess the costs and benefots of this approach, and describe its impact on three areas of theorem prover design: specification, automated reasoning and interaction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, Baco Raton, Florida, 1995.
M.J.C Gordon and T.F Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
J. Harrison. A Mizar Mode for HOL. In J. Von Wright, J. Grundy, and J. Harrison, editors, Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL, volume 1125 of Lecture Notes in Computer Science, pages 203–220, Turku, Finland, August 1996. Springer Verlag.
Matt Kaufmann and J. Strother Moore. ACL2: An industrial strength version of Nqthm. COMPASS — Proceedings of the Annual Conference on Computer Assurance, pages 23–34, 1996. IEEE catalog number 96CH35960.
M.J.C. Gordon, R. Milner, and C.P. Wadsworth. A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1979.
Michael Norrish. C Formalized in HOL. PhD thesis, University of Cambridge, August 1998.
L.C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994.
R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1979.
P. Rudnicki. An overview of the MIZAR project, 1992. Unpublished; available by anonymous FTP from http://www.menaik.cs.ualberta.ca as http://www.pub/Mizar/Mizar_Over.tar.Z.
Don Syme. Interaction for Declarative Theorem Proving, December 1998. Available from http://research.microsoft.com/users/dsyme.
Don Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, Computer Laboratory, January 1999. Available from http://research.microsoft.com/users/dsyme.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Syme, D. (1999). Three Tactic Theorem Proving. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_14
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive