This page provides additional material for my paper Formalizing Cut Elimination of Coalgebraic Logics in Coq, which was published in the proceedings of Tableaux 2013 (official LNAI DOI link to the paper). The paper is about my Coq formalization of Cut elimination in Coalgebraic Logics by Dirk Pattionson and Lutz Schröder. In their paper, Pattionson and Schröder develop a generic framework for propositional modal logics and prove soundness, completeness, cut elimination and Craig interpolation under certain assumptions on the rules and the semantics of the logic.
Here, you find the complete source code, you can browse the coqdoc generated documentation and there is a table below, linking the lemmas of Pattionson's and Schröder's paper with the formalization.
My formalization contains the results on soundness, completeness and cut elimination. Interpolation and the examples coalition logic and conditional logics are not (yet) covered. More details are contained in my paper.
The complete Coq sources of the formalization are available as free software under GLP version 3.
Download: [cut-eli.tgz]
To check the proofs you need Coq version 8.4 or 8.4pl2 (coqchk version 8.4pl1 fails on the Coq library). Download the formalization, untar it (tar -xf cut-eli.tgz) and run make check in the new subdirectory.
The check compiles the formalization and runs coqchk on it. Please be patient, the coqchk run takes about 15 minutes. At the end, coqchk prints the list of axioms that appear in the formalization. This list should be empty.
You can browse the coqdoc generated documentation of the formalization. There is also an Index of all definitions and theorems.
The following table relates the propositions of the paper with the formalization.