Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions

Explore a conference presentation that formalizes a proof calculus for incremental linearization in satisfiability modulo nonlinear arithmetic and transcendental functions. Learn how researchers from Federal University of Minas Gerais, Stanford University, and University of Iowa address the challenge of determining satisfiability of formulas involving nonlinear real arithmetic and transcendental functions, which is crucial for formally verifying dynamic systems. Discover the incremental linearization approach that facilitates reasoning through abstraction-refinement via incremental axiomatization of nonlinear and transcendental operators, currently implemented in MathSAT and cvc5 SMT solvers. Examine two key contributions: a formalization in the Lean proof assistant of the proof calculus employed by cvc5, and an extension of the lean-smt plugin to reconstruct proofs produced by cvc5 using this calculus. Understand how these contributions ensure soundness of the proof calculus, making the underlying algorithm more trustworthy while allowing users to check cvc5 results and improve Lean's automation for nonlinear arithmetic problems. Gain insights into the modeling of rules in the proof assistant, challenges encountered during formalization, and solutions for reconstructing proofs involving these rules in Lean.