  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.
