Computer Science Department
School of Computer Science, Carnegie Mellon University
Extracting Proofs from Branch-and-Prune
Sicun Gao, Soonho Kong, Michael Wang, Edmund M. Clarke
δ-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.