2014/04/17 by Avigad, Jeremy, Lewis, Robert Y., Roux, Cody · 1 citation
#F.2.1 #FOS: Computer and information sciences #G.4 #I.1.2 #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS)
paper · doi:10.48550/arxiv.1404.4410
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.