# Formalized Cut Elimination of Coalgebraic Logics: Source Code
and Documentation

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.

## Download and Check

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.

## Browse

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.

last modified on
23 Sep 2013
by Hendrik