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.

• Type: Journal
• Year: 2016
• Where: JAR
• Authors: Jeremy Avigad, Robert Y. Lewis, Cody Roux
• Keywords: Algorithms, JAR 2016