Proof Generation from Delta-Decisions

Sicun Gao, Soonho Kong, Edmund Clarke

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…