A heuristic prover for real inequalities
Mathematical Software
2016-01-05 v2 Logic in Computer Science
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 works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.
Cite
@article{arxiv.1404.4410,
title = {A heuristic prover for real inequalities},
author = {Jeremy Avigad and Robert Y. Lewis and Cody Roux},
journal= {arXiv preprint arXiv:1404.4410},
year = {2016}
}