Checking Linear Integer Arithmetic Proofs in Lambdapi
Alessio Coltellacci, Stephan Merz · Lecture notes in computer science · 2025
Abstract Modern SMT solvers can generate proofs of unsatisfiability so that the result can be checked independently. A dependable approach to verify these proofs is to reconstruct them within a proof assistant. In previous work, the SMT checker Carcara was extended to reconstruct SMT proofs in Lambdapi—a proof assistant designed for interoperability, supporting the import and export of proofs for integration with other proof assistants such as Rocq, Lean, or HOL-Light. Whereas that work was limited to SMT theories without arithmetic, we here present an extension that enables the reconstruction of SMT proofs involving linear integer arithmetic.