Proof Generation from Delta-Decisions
Sicun Gao, Soonho Kong, Edmund Clarke

TL;DR
This paper introduces a method to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures, enhancing correctness verification and advancing automated theorem proving over real numbers.
Contribution
It presents a novel approach that transforms numerical constraint solving steps into formal logic proofs, enabling proof validation and application to complex mathematical conjectures.
Findings
Successfully generated proofs for nonlinear lemmas in Kepler Conjecture
Validated correctness of decision procedures through proof-checking
Bridged numerical algorithms with formal proof systems
Abstract
We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem is important for ensuring correctness of the decision procedures. At the same time, it is a new approach for automated theorem proving over real numbers. We design a first-order calculus, and transform the computational steps of constraint solving into logic proofs, which are then validated using proof-checking algorithms. As an application, we demonstrate how proofs generated from our solver can establish many nonlinear lemmas in the the formal proof of the Kepler Conjecture.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
