A Proof-Producing Decision Procedure for Real Arithmetic

We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving. 1 Overview and related work Arguably the first automated theorem prover ever written was for a theory of linear arithmetic [8]. Nowadays many theorem proving systems, even those normally classified as `interactive' rather than `automatic', contain procedures to automate routine arithmetical reasoning over some of the supported number systems like N, Z, Q, R and C. Experience shows that such automated support is invaluable in relieving users of what would otherwise be tedious low-level proofs. We can identify several very common limitations of such procedures: ? Often they are restricted to proving purely universal formulas rather...

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Sean McLaughlin, John Harrison
• Keywords: Automated Reasoning, CADE 2005, Real Closed Fields, Standalone Decision Algorithms, Tedious Low-level Proofs