Sciweavers

Share
JAR
2016

A Heuristic Prover for Real Inequalities

4 years 3 months ago
A Heuristic Prover for Real Inequalities
Abstract We describe a general method for verifying inequalities between realvalued 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-Oppenstyle architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.
Jeremy Avigad, Robert Y. Lewis, Cody Roux
Added 06 Apr 2016
Updated 06 Apr 2016
Type Journal
Year 2016
Where JAR
Authors Jeremy Avigad, Robert Y. Lewis, Cody Roux
Comments (0)
books