Proof analysis in modal logic

DOI10.1007/s10992-005-2267-3zbMath1086.03045OpenAlexW1995718667MaRDI QIDQ812101

Publication date: 23 January 2006

Published in: Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10992-005-2267-3

zbMATH Keywords

decidability Kripke semantics Kripke frame normal modal logics Gödel-Löb logic admissibility of structural rules labelled sequent calculi

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items

Labelled calculi for the logics of rough concepts, FRACTIONAL-VALUED MODAL LOGIC, The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions, On a graph calculus for modalities, From axioms to synthetic inference rules via focusing, Power and Limits of Structural Display Rules, VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED, A more unified approach to free logics, Modal logics, justification logics, and realization, Deep sequent systems for modal logic, Analytic rules for mereology, Label-free natural deduction systems for intuitionistic and classical modal logics, Logicality, double-line rules, and modalities, A formally verified cut-elimination procedure for linear nested sequents for tense logic, Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq, Syntactic Completeness of Proper Display Calculi, Invited Talk: Coherentisation of First-Order Logic, A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics, Linear Nested Sequents, 2-Sequents and Hypersequents, SEMANTIC POLLUTION AND SYNTACTIC PURITY, Embedding Constructive K into Intuitionistic K, PRIORITY MERGE AND INTERSECTION MODALITIES, Labeled sequent calculus for justification logics, A deep inference system for the modal logic S5, Useful Four-Valued Extension of the Temporal Logic KtT4, CONDITIONAL BELIEFS: FROM NEIGHBOURHOOD SEMANTICS TO SEQUENT CALCULUS, Hypersequent rules with restricted contexts for propositional modal logics, Labeled sequent calculi for modal logics and implicit contractions, Does the deduction theorem fail for modal logic?, LINEAR TIME IN HYPERSEQUENT FRAMEWORK, Provability multilattice logic, Cut elimination in coalgebraic logics, Mechanising Gödel-Löb provability logic in HOL light, Rooted hypersequent calculus for modal logic \textsf{S5}, Metainferential reasoning on strong Kleene models, Metasequents and tetravaluations, Disentangling structural connectives or life without display property, Prefixed tableaus and nested sequents, Semantical analysis of the logic of bunched implications, A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic, Herzberger's limit rule with labelled sequent calculus, Proof systems for super-strict implication, Labelled calculi for lattice-based modal logics, The intensional side of algebraic-topological representation theorems, Neutral free logic: motivation, proof theory and models, Unnamed Item, Dualized Simple Type Theory, The Church-Fitch knowability paradox in the light of structural proof theory, Reasoning about collectively accepted group beliefs, Hypersequent Calculi for S5: The Methods of Cut Elimination, Simple cut elimination proof for hybrid logic, Proof analysis in intermediate logics, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Machine-Checked Proof-Theory for Propositional Modal Logics, Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic, Through an Inference Rule, Darkly, Implementing a relational theorem prover for modal logic, A Conditional Constructive Logic for Access Control and Its Sequent Calculus, Labelled sequent calculi for Lewis' non-normal propositional modal logics, Non-classical elegance for sequent calculus enthusiasts, Constructive Description Logics Hybrid-Style, Full classical S5 in natural deduction with weak normalization, On graph calculi for multi-modal logics, Proofs and countermodels in non-classical logics, A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5, Hypersequent and display calculi -- a unified perspective, HARMONIC INFERENTIALISM AND THE LOGIC OF IDENTITY, POSITIVE LOGIC WITH ADJOINT MODALITIES: PROOF THEORY, SEMANTICS, AND REASONING ABOUT INFORMATION, Recapturing dynamic logic of relation changers via bounded morphisms, A generalized proof-theoretic approach to logical argumentation based on hypersequents, Kripke semantics for intuitionistic Łukasiewicz logic, Unnamed Item, The Method of Tree-Hypersequents for Modal Propositional Logic, Machine Checking Proof Theory: An Application of Logic to Logic, Unnamed Item, Proof Theory for Distributed Knowledge, GEOMETRISATION OF FIRST-ORDER LOGIC, A Connection-Based Characterization of Bi-intuitionistic Validity, Multicomponent proof-theoretic method for proving interpolation properties, PROOF ANALYSIS FOR LEWIS COUNTERFACTUALS, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information, Meaning in Use, Revising a Labelled Sequent Calculus for Public Announcement Logic, Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics, Proof-theoretic analysis of the logics of agency: the deliberative STIT, Focused and Synthetic Nested Sequents, Validity, dialetheism and self-reference, Inducing Syntactic Cut-Elimination for Indexed Nested Sequents, On a multilattice analogue of a hypersequent S5 calculus, CUT AND GAMMA I: PROPOSITIONAL AND CONSTANT DOMAIN R, Expanding the Realm of Systematic Proof Theory, Sequent calculi and decidability for intuitionistic hybrid logic, A general proof certification framework for modal logic, Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate, Empirical Negation, Co-Negation and the Contraposition Rule II: Proof-Theoretical Investigations, A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY, Circular proofs for the Gödel-Löb provability logic, Paraconsistent Gödel modal logic, On the proof theory of infinitary modal logic, Geometric Rules in Infinitary Logic, Modular sequent calculi for classical modal logics, A connection-based characterization of bi-intuitionistic validity

Uses Software

Cites Work