Machine-checked proof-theory for propositional modal logics

DOI10.1007/978-3-319-29198-7_5MaRDI QIDQ3305555zbMATH OpenOpenAlexFDO

Authors Rajeev Goré, Jesse Wu, 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

zbMATH Keywords

backward proof searchexplicit structural rulesimplicit derivationsequent calculusSK rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05)

Recommendations

• scientific article; zbMATH DE number 970622
• Machine Checking Proof Theory: An Application of Logic to Logic
• Proof analysis in modal logic
• A tableau method for checking rule admissibility in S4
• A systematic proof theory for several modal logics

Cites work

• Cut-free hypersequent calculus for S4.3.
• Cut-free sequent and tableau systems for propositional Diodorean modal logics
• Display logic
• Formalizing cut elimination of coalgebraic logics in Coq
• Generic methods for formalising sequent calculi applied to provability logic
• scientific article; zbMATH DE number 3131074 (Why is no real title available?)
• scientific article; zbMATH DE number 120347 (Why is no real title available?)
• scientific article; zbMATH DE number 1989648 (Why is no real title available?)
• scientific article; zbMATH DE number 2064301 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Linear logic
• Machine Checking Proof Theory: An Application of Logic to Logic
• Proof analysis in modal logic
• Structural proof theory. With an appendix by Aarne Ranta
• Valentini's cut-elimination for provability logic resolved

Cited in

(7)

• The propositional formula checker HeerHugo
• Minimal Proof Search for Modal Logic K Model Checking
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• Machine Checking Proof Theory: An Application of Logic to Logic
• αCheck: A mechanized metatheory model checker
• scientific article; zbMATH DE number 1848381 (Why is no real title available?)
• scientific article; zbMATH DE number 7204319 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle
• ML
• HOL
• Pesca

This page was built for publication: Machine-checked proof-theory for propositional modal logics

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