References & Citations
Computer Science > Mathematical Software
Title: A heuristic prover for real inequalities
(Submitted on 17 Apr 2014 (v1), last revised 4 Jan 2016 (this version, v2))
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.
Submission history
From: Jeremy Avigad [view email][v1] Thu, 17 Apr 2014 01:31:39 GMT (30kb,D)
[v2] Mon, 4 Jan 2016 19:09:17 GMT (35kb,D)
Link back to: arXiv, form interface, contact.