Modularisation of sequent calculi for normal and non-normal modalities

DOI10.1145/3288757MaRDI QIDQ4633639zbMATH OpenOpenAlexWikidataFDO

Authors Björn Lellmann, Elaine Pimentel

Publication date 3 May 2019

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.08193

zbMATH Keywords

labelled systemslinear nested sequentsmodal logicproof theory

Mathematics Subject Classification ID

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

Abstract: In this work we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules we obtain linear nested sequent calculi for a number of logics, including to our knowledge the first nested sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as bipole clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.

Recommendations

• Modular sequent systems for modal logic
• Proof search in nested sequent calculi
• Sequentialising nested systems
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Modular sequent calculi for classical modal logics

Cited in

(24)

• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• From input/output logics to conditional logics via sequents -- with provers
• Countermodel construction via optimal hypersequent calculi for non-normal modal logics
• Combining monotone and normal modal logic in nested sequents -- with countermodels
• A fresh view of linear logic as a logical framework
• Modular sequent calculi for classical modal logics
• Non-normal modal logics and conditional logics: semantic analysis and proof theory
• Structural Refinement for the Modal nu-Calculus
• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• Proof search in nested sequent calculi
• Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
• Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• A linear logic framework for multimodal logics
• Natural deduction calculi for classical and intuitionistic S5
• Cut Elimination for Extended Sequent Calculi
• CoNP complexity for combinations of non-normal modal logics
• Resolution calculi for non-normal modal logics
• On the finite model property of non-normal modal logics
• A natural deduction calculus for \textbf{S4.2}
• Minimal modal logics, constructive modal logics and their relations
• Nested sequents or tree-hypersequents -- a survey
• Sequent systems on undirected graphs
• Intuitionistic non-normal modal logics: a general framework

This page was built for publication: Modularisation of sequent calculi for normal and non-normal modalities

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