“Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions” by Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, and Cesare Tinelli. In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026, (Kathrin Stark, Yannick Zakowski, Nikhil Swamy, and Nicolas Tabareau, eds.), Jan. 2026, pp. 216-230.
Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions is necessary in many applications, such as formally verifying dynamic systems. Doing this automatically generally requires costly and intricate methods, which limits their applicability. In the context of SMT solving, Incremental Linearization was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach. The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers MathSAT and cvc5. The cvc5 implementation is also proof-producing. This paper presents two 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 the proofs produced by cvc5 using this proof calculus. These contributions ensure the soundness of the proof calculus, making the underlying algorithm more trustworthy. Moreover, they allow users to check cvc5 results obtained via incremental linearization, as well as improve Lean's automation for problems in nonlinear arithmetic. We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them, as well as the issues in reconstructing proofs involving these rules in Lean, and how we solved them.
BibTeX entry:
@inproceedings{MKM+26,
author = {Tomaz Mascarenhas and Harun Khan and Abdalrhman Mohamed and
Andrew Reynolds and Haniel Barbosa and Clark W. Barrett and Cesare
Tinelli},
editor = {Kathrin Stark and Yannick Zakowski and Nikhil Swamy and
Nicolas Tabareau},
title = {Formalization of a Proof Calculus for Incremental
Linearization for Satisfiability Modulo Nonlinear Arithmetic and
Transcendental Functions},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} International
Conference on Certified Programs and Proofs, {CPP} 2026, Rennes,
France, January 12-13, 2026},
pages = {216--230},
publisher = {{ACM}},
month = jan,
year = {2026},
doi = {10.1145/3779031.3779111},
url = {https://doi.org/10.1145/3779031.3779111}
}
(This webpage was created with bibtex2web.)