A HOL decision procedure for elementary real algebra

John Harrison.

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

NB! This paper is preliminary, and will be superseded by a chapter of the author's forthcoming PhD thesis.

Abstract:

The elementary theory of real algebra, including multiplication, is decidable. More precisely, there is an algorithm to eliminate quantifiers which does not introduce new free variables or new constants other than rational numbers. Therefore if a closed term of elementary real algebra involves no constants other than the rational numbers, its truth or falsity can be determined automatically. Quite a number of interesting algebraic and geometric problems can be expressed in this decidable subset. In this paper we describe a HOL implementation of a quantifier-elimination procedure and give some preliminary results.

DVI or PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-hol93,
        crossref        = "hol93",
        author          = "John Harrison",
        title           = "A {HOL} Decision Procedure for Elementary Real
                           Algebra",
        pages           = "426--436"}

@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"}