Carnegie Mellon University
Browse
file.pdf (322.87 kB)

A Heuristic Prover for Real Inequalities

Download (322.87 kB)
journal contribution
posted on 2014-06-01, 00:00 authored by Jeremy AvigadJeremy Avigad, Robert Y. Lewis, Cody Roux

We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen-style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method is promising, complementing techniques that are used by contemporary interactive provers.

History

Publisher Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08970-6_5

Date

2014-06-01

Usage metrics

    Categories

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC