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.


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.

Prop 3.2.1 prop_3_2_1 Def 4.9 step_semantics
Def 3.3 one_step_rule Lem 4.10 semantics_step_semantics
Def 3.5 weaken_subst_rule Lem 4.11 unit_coalg_seq_cone_identity
Lem 3.7 stratified_one_step_rules Cor 4.12 step_semantics_validity
Lem 3.9 GR_n_provable_with_premises Prop 4.13 n_completeness
Lem 3.10 rank_proof_GR Prop 4.13 n_cut_free_completeness
Lem 3.11 weakening_admissible_GR_n Cor 4.14 completeness
Lem 3.12 inversion_depth_preserving_admissible_Gn_H   Cor 4.14 cut_free_completeness
Lem 3.13 inversion_admissible_GR_n Th 4.15 semantic_admissible_cut
Lem 3.14 GRC_n_substitution_lemma Th 4.15 semantic_admissible_contraction
Lem 3.15 rank_proof_GRC Def 5.1 absorbs_congruence
Def 4.1 one_step_sound Ex 5.2 k_absorbs_congruence
Def 4.1 one_step_complete Def 5.3 absorbs_contraction
Def 4.1 one_step_cut_free_complete Ex 5.4 k_absorbs_contraction
Lem 4.3 simple_one_step_cut_free_complete Def 5.5 absorbs_cut
Ex 4.6 k_rules_one_step_sound Prop 5.6 syntactic_GR_n_non_atomic_axioms  
Ex 4.6 k_rules_one_step_cut_free_complete Prop 5.6 syntactic_GR_n_cc
Th 4.7 sound_GRC Th 5.7 syntactic_admissible_cut
Th 4.7 sound_GR Th 5.7 syntactic_admissible_contraction

last modified on 23 Sep 2013 by Hendrik