3 ms·
Automatically Translating Proof Systems for SMT Solvers to the λΠ-Calculus [pdf]
- finalcoalgebra 7mo agoEunoia 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.