Machine-Checked Proof-Theory for Propositional Modal Logics

Abstract

We describe how we machine-checked the admissibility of the standard structural rules of weakening, contraction and cut for multiset-based sequent calculi for the unimodal logics S4, S4.3 and D4De, as well as for the bimodal logic S4C recently investigated by Mints. Our proofs for both S4 and S4.3 appears to avoid the complications he encountered. the paper is intended to be an overview of how to machine-check proof theory for readers with a good understanding of proof theory. Show more