Abstract
We describe the results of an experiment in which the Nuprl proof development system was used in conjunction with a collection of simple proof-assisting programs to constructively prove a substantial theorem of number theory. We believe that these results indicate the promise of an approach to reasoning about computationally meaningful mathematics by which both proof construction and the results of formal reasoning are mathematically comprehensible.
This work was supported, in part, by NSF grant no. MCS-81-04018
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E. Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967.
R. Boyer and J S. Moore. A Computational Logic. Academic Press, NY, 1979.
N. G. deBruijn. A Survey of the Project AUTOMATH. In Essays in Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley, eds., pages 589–606. Academic Press, 1980.
R. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System, Prentice Hall, 1986.
R. Constable, S. Johnson, and C. Eichenlaub. Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science, vol. 135, Springer-Verlag, Berlin, 1982.
R. Constable, T. Knoblock, and J. Bates. Writing Programs that Construct Proofs. Journal of Automated Reasoning v.1 n.3, (1985), pages 285–326.
T. Coquand & G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. EUROCAL 85, Linz, Austria, April 1985.
M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science, vol. 78, Springer-Verlag, Berlin, 1979.
D. Howe. Implementing Analysis. PhD Dissertation, Department of Computer Science, Cornell University, 1986 (expected).
D. Howe Reflected Term Rewriting In Type Theory. Technical Report, Department of Computer Science, Cornell University, 1986 (to appear).
T. Knoblock, R. Constable. Formalized Metareasoning in Type Theory. Technical Report TR 86-742, Department of Computer Science, Cornell University, 1986.
Z. Manna, R. Waldinger. A Deductive Approach to Program Synthesis. ACM Trans. on Prog. Lang. and Sys. v.2 n.1 (January 1980), pp 90–121.
Per Martin-Löf. Constructive Mathematics and Computer Programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, North Holland, Amsterdam, 1982, pages 153–175.
L. Paulson. A Higher-Order Implementation of Rewriting. Science of Computer Programming n. 3, 1983, pp 119–149.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Howe, D.J. (1986). Implementing number theory: An experiment with Nuprl. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_108
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_108
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive