Sequent Calculi for Normal Modal Propositional Logics

DOI10.1093/logcom/4.2.125zbMath0799.03014MaRDI QIDQ4291036

Heinrich Wansing

Publication date: 24 November 1994

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/4.2.125

zbMATH Keywords

Kripke semantics; Kripke model; cut-elimination; display logic; sequents

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03F05: Cut-elimination and normal-form theorems

Related Items

POSITIVE LOGIC WITH ADJOINT MODALITIES: PROOF THEORY, SEMANTICS, AND REASONING ABOUT INFORMATION, Displaying the modal logic of consistency, Brodskio kodavimo metodas teiginių logikai;Brodsky’s coding method for propositional logic, A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY, Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere, Proof complexity of modal resolution, Self-referential justifications in epistemic logic, Display calculi and other modal calculi: a comparison, Indexed systems of sequents and cut-elimination, A proof-theoretic investigation of a logic of positions, On constructing a logic for the notion of complete and immediate formal grounding, A set-theoretic translation method for polymodal logics, Local reductions for the modal cube, Hypersequent and display calculi -- a unified perspective, From single agent to multi-agent via hypersequents, Disentangling structural connectives or life without display property, Full classical S5 in natural deduction with weak normalization, Logicality, double-line rules, and modalities, Linear Nested Sequents, 2-Sequents and Hypersequents, Self-referentiality of Justified Knowledge, A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5, The Method of Tree-Hypersequents for Modal Propositional Logic, Why does the proof-theory of hybrid logic work so well?