Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals

John Harrison and Laurent Théry.

Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, Vancouver. Springer LNCS 780, pp. 174-184.

NB! This paper is superseded by a recent Journal version

Abstract:

In this paper we describe an environment for reasoning about the reals which combines the rigour of a theorem prover with the power of a computer algebra system.

PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-thery2,
        crossref        = "hol93",
        author          = "John Harrison and Laurent Th{\'e}ry",
        title           = "Extending the {HOL} Theorem Prover
                           with a Computer Algebra System
                           to Reason about the Reals",
        pages           = "174--184"}

@PROCEEDINGS{hol93,
        editor          = "Jeffrey J. Joyce and Carl Seger",
        booktitle       = "Proceedings of the 1993 International Workshop on
                           the {HOL} theorem proving system and its
                           applications",
        series          = "Lecture Notes in Computer Science",
        volume          = 780,
        address         = "UBC, Vancouver, Canada",
        date            = "August 1993",
        year            = 1993,
        publisher       = "Springer-Verlag"}