Proof analysis in modal logic

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

Sara Negri

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

decidabilityKripke semanticsKripke framenormal modal logicsGödel-Löb logicadmissibility of structural ruleslabelled sequent calculi

Mathematics Subject Classification ID

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

Related Items (only showing first 100 items - show all)

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 ⋮ Labelled calculi for the logics of rough concepts

Uses Software

• TABLEAUX
• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-theoretical analysis of order relations
• The modal logic of provability: cut-elimination
• Proof methods for modal and intuitionistic logics
• The modal logic of provability. The sequential approach
• TABLEAUX: A general theorem prover for modal logics
• The logic of information structures
• Indexed systems of sequents and cut-elimination
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Natural deduction for non-classical logics
• On the proof theory of the modal logic for arithmetic provability
• Cut Elimination in the Presence of Axioms
• Translation Methods for Non-Classical Logics: An Overview
• Representation, reasoning, and relational structures: a hybrid logic manifesto
• A cut-free Gentzen formulation of the modal logic S5
• A proof-theoretic study of the correspondence of classical logic and modal logic
• A Systematic Presentation of Quantified Modal Logics
• Proof systems for lattice theory

This page was built for publication: Proof analysis in modal logic