# A heuristic prover for real inequalities

arXiv: https://arxiv.org/abs/1404.4410 · HTML: https://mlsanity.com/paper/1404.4410/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Apr 2014.

## Built on by (most cited first, 1 of 1)

- [Contradictions](https://mlsanity.com/paper/2509.07026/) (2025)

## Abstract (arXiv)

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.