δ-Complete decision procedures can solve SMT problems over the reals with a wide range of nonlinear functions, allowing "δ-bounded errors." The scalability of such procedures usually depends on efficient numerical procedures, whose implementation can be error-prone. It is important for δ-complete solvers to provide certificates to prove the correctness of their answers. We show how to do this for DPLLhICPi, a general solving framework based on Interval Constraint Propagation. We focus on the construction of proof trees for the "unsat" answers and the proof-checking of their correctness. Besides certifying solvers, we find our approach a promising one for automated theorem proving over the reals, exploiting the power of numerical algorithms in a formal way. One direct application is to establish many nonlinear lemmas in the Flyspeck project, for the formal proof of the Kepler Conjecture.

17 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu