Abstract
This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Behrend, F.A.,A Contribution to the Theory of Magnitudes and the Foundations of Analysis, Mathematische Zeitschrift, vol. 63, pp. 345–362, 1956.
Bishop, E. and Bridges, D.,Constructive analysis, Springer-Verlag, 1985.
Bourbaki, N.,Elements of mathematics, vol. 3: General Topology, part 1, Hermann 1966.
de Bruijn, N.G.,Defining Reals Without the Use of Rationals, Indagationes Mathematicae, vol. 38, pp. 100–108, 1976.
Burkill, J.C.,A First Course in Mathematical Analysis, Cambridge 1962.
Burkill, J.C. and Burkill, H.,A Second Course in Mathematical Analysis, Cambridge 1970.
Burrill, C.W.,Foundations of Real Numbers, McGraw-Hill 1967.
Chirimar, J., Howe and D.J.,Implementing Constructive Real Analysis, preprint 1992.
Cohen, L.W., and Ehrlich, G.,Structure of the real number system, Van Nostrand 1963.
Conway, J.H.,On Numbers and Games, Academic Press 1976.
Faltin, F., Metropolis, N., Ross, B. and Rota, G.-C.,The Real Numbers as a Wreath Product Advances in Mathematics, vol. 16, pp. 278–304, 1975.
Golan, J.S.,The Theory of Semirings with Applications in Mathematics and Computer Science, Longman 1992.
Harrison, J.R. and Théry, L.,Reasoning About the Reals: The Marriage of HOL and Maple, Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR 93), Springer Lecture Notes in Artificial Intelligence vol. 698, pp. 351–353, 1993.
IEEE,Standard for Binary Floating Point Arithmetic, ANSI/IEEE Standard 754–1985.
Jones, C.,Completing the Rationals and Metric Spaces in LEGO, Proceedings of the 2nd Workshop on Logical Frameworks, Edinburgh 1991.
Jutting, L.S.,Checking Landau's “Grundlagen” in the Automath System, PhD thesis, Eindhoven University of Technology 1977.
Kelley, J.L.,General Topology, Van Nostrand 1955.
Kuhn, S.,The Derivative à la Carathéodory, American Mathematical Monthly, vol. 98, pp. 40–44, 1991.
Landau, E.,Foundations of analysis, Chelsea 1951.
Pnueli, A.,From Timed To Hybrid Systems, preprint 1992.
Stoll, R.R.,Set theory and logic, Dover 1979.
Thurston, H.A.,The number system, Blackie 1956.
Wallis, P.J.L.,Improving floating-point programming, Wiley 1990.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Harrison, J. Constructing the real numbers in HOL. Form Method Syst Des 5, 35–59 (1994). https://doi.org/10.1007/BF01384233
Issue Date:
DOI: https://doi.org/10.1007/BF01384233