Machine-Checked Proof-Theory for Propositional Modal Logics
From MaRDI portal
Publication:3305555
DOI10.1007/978-3-319-29198-7_5zbMath1439.03035OpenAlexW2483720016MaRDI QIDQ3305555
Jesse Wu, Rajeev Goré, Jeremy E. Dawson
Publication date: 7 August 2020
Published in: Advances in Proof Theory (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-29198-7_5
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)
Uses Software
Cites Work
- Linear logic
- Proof analysis in modal logic
- Isabelle. A generic theorem prover
- Cut-free sequent and tableau systems for propositional Diodorean modal logics
- Display logic
- Formalizing Cut Elimination of Coalgebraic Logics in Coq
- Machine Checking Proof Theory: An Application of Logic to Logic
- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Machine-Checked Proof-Theory for Propositional Modal Logics