Reseña: “Formalizing cut elimination of coalgebraic logics in Coq”
Se ha publicado un artículo de razonamiento formalizado en Coq sobre metalógica titulado Formalizing cut elimination of coalgebraic logics in Coq.
Su autor es Hendrik Tews (de la Dresden University of Technology) y se presentará en el Tableaux 2013 (Automated Reasoning with Analytic Tableaux and Related Methods).
Su resumen es
In their work on coalgebraic logics, Pattinson and Schröder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics. The present paper reports on a formalization of Pattinson’s and Schröder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.
El código de las correspondientes teorías en Coq se encuentra aquí.