Formalizing Cut Elimination of Coalgebraic Logics in Coq

DOI10.1007/978-3-642-40537-2_22zbMath1401.68280OpenAlexW294087978MaRDI QIDQ2851950

Hendrik Tews

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

Mathematics Subject Classification ID

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

• Coq
• PVS
• Proof General
• Nominal Isabelle

This page was built for publication: Formalizing Cut Elimination of Coalgebraic Logics in Coq