Formalizing Cut Elimination of Coalgebraic Logics in Coq
From MaRDI portal
Publication:2851950
DOI10.1007/978-3-642-40537-2_22zbMath1401.68280OpenAlexW294087978MaRDI QIDQ2851950
Publication date: 4 October 2013
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-40537-2_22
Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items (6)
A formally verified cut-elimination procedure for linear nested sequents for tense logic ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ A henkin-style completeness proof for the modal logic S5 ⋮ Machine-Checked Proof-Theory for Propositional Modal Logics ⋮ Formalized meta-theory of sequent calculi for substructural logics
Uses Software
This page was built for publication: Formalizing Cut Elimination of Coalgebraic Logics in Coq