A heuristic prover for real inequalities

Jeremy Avigad; Robert Y. Lewis; Cody Roux

doi:10.1007/978-3-319-08970-6_5

A heuristic prover for real inequalities

Jeremy Avigad, Robert Y. Lewis, Cody Roux

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer Verlag
Pages	61-76
Number of pages	16
ISBN (Print)	9783319089690
DOIs	https://doi.org/10.1007/978-3-319-08970-6_5
Publication status	Published - 1 Jan 2014
Externally published	Yes
Event	5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 14 Jul 2014 → 17 Jul 2014

Publication series

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

Conference

Conference	5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Country	Austria
City	Vienna
Period	14/07/14 → 17/07/14

Access to Document

10.1007/978-3-319-08970-6_5

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

Avigad, Jeremy ; Lewis, Robert Y. ; Roux, Cody. / A heuristic prover for real inequalities. Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 61-76 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d8b8f03aa3b346cda496b575b6ad617b,

title = "A heuristic prover for real inequalities",

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.",

author = "Jeremy Avigad and Lewis, {Robert Y.} and Cody Roux",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-08970-6_5",

language = "English",

isbn = "9783319089690",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "61--76",

booktitle = "Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

address = "Germany",

note = "5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",

}

Avigad, J, Lewis, RY & 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8558 LNCS, Springer Verlag, pp. 61-76, 5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 14/07/14. https://doi.org/10.1007/978-3-319-08970-6_5

A heuristic prover for real inequalities. / Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody.

Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 61-76 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8558 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A heuristic prover for real inequalities

AU - Avigad, Jeremy

AU - Lewis, Robert Y.

AU - Roux, Cody

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84904811070&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904811070&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08970-6_5

DO - 10.1007/978-3-319-08970-6_5

M3 - Conference contribution

AN - SCOPUS:84904811070

SN - 9783319089690

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 61

EP - 76

BT - Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

T2 - 5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014

Y2 - 14 July 2014 through 17 July 2014

ER -

Avigad J, Lewis RY, Roux C. 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. Springer Verlag. 2014. p. 61-76. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-08970-6_5

A heuristic prover for real inequalities

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this