A heuristic prover for real inequalities

Jeremy Avigad, Robert Y. Lewis, Cody Roux

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages61-76
Number of pages16
ISBN (Print)9783319089690
DOIs
Publication statusPublished - 1 Jan 2014
Externally publishedYes
Event5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: 14 Jul 201417 Jul 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8558 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period14/07/1417/07/14

Fingerprint Dive into the research topics of 'A heuristic prover for real inequalities'. Together they form a unique fingerprint.

  • Cite this

    Avigad, J., Lewis, R. Y., & Roux, C. (2014). A heuristic prover for real inequalities. In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 61-76). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8558 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_5