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 -