Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Constructing the real numbers in HOL

Constructing the real numbers in HOL

John Harrison.

Formal Methods in System Design, vol. 5, pp. 35-59, 1994.

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.

PostScript

Bibtex entry:

@ARTICLE{harrison-fmsd94,
        author          = "John Harrison",
        title           = "Constructing the Real Numbers in {HOL}",
        journal         = "Formal Methods in System Design",
        year            = 1994,
        volume          = 5,
        pages           = "35--59"}