Reasoning about the reals: the marriage of HOL and Maple

John Harrison and Laurent Théry.

Proceedings of the 4th international conference on Logic Programming and Automated Reasoning, Hotel Olgino, St. Petersburg. Springer LNCS 698, pp. 351-353, 1993.

NB! This paper was only a short `system description' and is superseded by a Journal version.

Abstract:

Modern computer algebra systems are extremely powerful and flexible, but often give results which require careful interpretation or are downright incorrect. By contrast, computer theorem provers are very reliable but lack the powerful specialized decision procedures and heuristics of computer algebra systems. In this paper we try to get the best of both worlds by careful exploitation of a link between the HOL theorem prover and the Maple computer algebra system.

PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-thery1,
        crossref        = "lpar93",
        author          = "John Harrison and Laurent Th{\'e}ry",
        title           = "Reasoning About the Reals:
                           the Marriage of {HOL}

@PROCEEDINGS{lpar93,
        editor          = "Andrei Voronkov",
        booktitle       = "Logic programming and automated reasoning:
                           proceedings of the 4th international conference,
                           {LPAR} '93",
        series          = "Lecture Notes in Computer Science",
        volume          = 698,
        address         = "Hotel Olgino, St. Petersburg, Russia",
        date            = "13--20 July 1993",
        year            = 1993,
        publisher       = "Springer-Verlag"}