Formalizing cut elimination of coalgebraic logics in Coq

DOI10.1007/978-3-642-40537-2_22zbMATH Open1401.68280OpenAlexW294087978MaRDI QIDQ2851950FDOQ2851950

Authors: 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

Recommendations

• Cut elimination in coalgebraic logics
• Proof systems for Moss' coalgebraic logic
• Admissibility of cut in coalgebraic logics
• Interacting with Modal Logics in the Coq Proof Assistant
• scientific article; zbMATH DE number 5872402

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Categorical logic, topoi (03G30)

Cited In (13)

• Verification of dynamic bisimulation theorems in Coq
• \textsf{LOGIC}: a Coq library for logics
• Generic methods for formalising sequent calculi applied to provability logic
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Formalized meta-theory of sequent calculi for substructural logics
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• Formalized meta-theory of sequent calculi for linear logics
• LF+ in Coq for "fast and loose" reasoning
• A henkin-style completeness proof for the modal logic S5
• Mechanizing bisimulation theorems for relation-changing logics in Coq
• Cut elimination in coalgebraic logics
• Machine-checked proof-theory for propositional modal logics
• How to Kill Epsilons with a Dagger

Uses Software

• Coq
• PVS
• Proof General
• Nominal Isabelle

This page was built for publication: Formalizing cut elimination of coalgebraic logics in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851950)