Comment by finalcoalgebra

Eunoia is an emerging logical framework for specifying the proofs and proof systems of SMT solvers, namely CVC5. We present a translation from Eunoia to the λΠ-calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool eo2lp, which we use for generating LambdaPi encodings of (a) a large fragment of CVC5’s Cooperating Proof Calculus (CPC), and (b) proofs produced by CVC5 on unsat problems from various fragments of SMT-LIB.