Checking Linear Integer Arithmetic Proofs in Lambdapi.

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.