A heuristic prover for real inequalities

Abstract. We describe a general method for verifying inequalities be-tween real-valued expressions, especially the kinds of straightforward in-ferences that arise in interactive theorem proving. In contrast to ap-proaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heteroge-neous 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.