Abstract
Following the success of the Mizar 15, 9 system in the mechanisation of mathematics, there is an increasing interest in the theorem proving community in developing similar declarative languages. In this paper we discuss the implementation of a simple declarative proof language (SPL) on top of the HOL system [3] where scripts in this language are used to generate HOL theorems, and HOL definitions, axioms, theorems and proof procedures can be used in SPL scripts. Unlike Mizar, the language is extensible, in the sense that the user can extend the syntax and semantics of the language during the mechanisation of a theory. A case study in the mechanisation of group theory illustrates how this extensibility can be used to reduce the difference between formal and informal proofs, and therefore increase the readability of formal proofs.
The work presented in this paper was done when the author was a student at the Computing Laboratory of the University of Kent at Canterbury.
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.
References
Bruno Barras et al. The Coq Proof Assistant Reference Manual. Projet Coq-INRIA-Rocquencourt, CNRS-ENS Lyons, November 1996. (Version 6.1).
Anatoli Degtyarev and Andrei Voronkov. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 20(1):47–80, 1998.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
Elsa Gunter. The implementation and use of abstract theories in HOL. In Proceedings of the Third HOL Users Meeting, Computer Science Department, Aarhus University, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark, October 1990. Technical Report DAIMI PB-340 (December 1990).
J. Harrison. A Mizar mode for HOL. In von Wright et al. J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996 [16], pages 203–220.
I.N. Herstein. Topics in Algebra. John Wiley & Sons, New York, 2nd edition, 1975.
L. Laibinis. Using lattice theory in higher order logic. In von Wright et al. J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996 [16], pages 315–330.
David A. Plaisted. Equational reasoning and term rewriting systems. In D. Gabbay, C. Hogger, J. A. Robinson, and J. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 5, pages 273–364. Oxford University Press, Oxford, 1993.
Piotr Rudnicki. An overview of the MIZAR project. Available by ftp from http://www.menaik.cs.ualberta.ca as http://www.pub/Mizar/Mizar_Over.tar.Z., June 1992.
Piotr Rudnicki and Andrzej Trybulec. On equivalents of well-foundedness. Available on the web at http://www.cs.ualberta.ca/~piotr/Mizar/Wfnd/, January 1997.
Konrad Slind. Object language embedding in Standard ML of New Jersey. In Proceedings of the Second ML Workshop held at Carnegie Mellon University, Pittsburgh, Pennsylvania, Septermber 26—27, 1991, CMU SCS Technical Report, November 1991.
Don Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997.
Don Syme. Proving Java type soundness. Technical Report 427, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997.
Donald Syme. Declarative Theorem Proving for Operating Semantics. PhDthesis, University of Cambridge, 1998. Submitted for Examination.
A. Trybulec. The Mizar-QC/6000 logic information language. Bulletin of the Association for Literary and Linguistic Computing, 6:136–140, 1978.
J. von Wright, J. Grundy, and J. Harrison, editors. Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’96), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer.
Vincent Zammit. On the Readability of Machine Checkable Formal Proofs. PhD thesis, University of Kent at Canterbury, October 1998. Submitted for Publication. (Currently available on the world wide web at the http://www.cs.ukc.ac.uk/people/rpg/vz1/thesis.ps.gz).
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
Zammit, V. (1999). On the Implementation of an Extensible Declarative Proof Language. 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_13
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_13
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