A Proof-Producing Decision Procedure for Real Arithmetic

Sean McLaughlin and John Harrison.

Proceedings of CADE-20: 20th International Conference on Automated Deduction. Springer LNCS 3632, pp. 295-314, 2005.

Abstract:

We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{mclaughlin-harrison,
        author          = "Sean McLaughlin and John Harrison",
        title           = "A Proof-Producing Decision Procedure for
                           Real Arithmetic",
        editor          = "Robert Nieuwenhuis",
        title           = "CADE-20: 20th International Conference on Automated
                           Deduction, proceedings",
        address         = "Tallinn, Estonia",
        date            = "July 2005",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 3632,
        year            = 2005,
        pages           = "295--314"}