Proof methods for modal and intuitionistic logics

Publication date: 1983

Published in: Synthese Library (Search for Journal in Brave)

interpolation modal logic cut elimination proof theory intuitionistic logic completeness proofs semantic tableaux Gentzen calculi natural deduction rules

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Categoricity and completeness of theories (03C35)

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

Power and Limits of Structural Display Rules ⋮ 1998 European Summer Meeting of the Association for Symbolic Logic ⋮ Interpolation Method for Multicomponent Sequent Calculi ⋮ Barcan Both Ways ⋮ Tableau for the logic ILP ⋮ Linear reasoning in modal logic ⋮ THE LOGIC OF SEQUENCE FRAMES ⋮ Tautology Elimination, Cut Elimination, and S5 ⋮ A translation from the modal logic of provability into K4 ⋮ Uniform and non uniform strategies for tableaux calculi for modal logics ⋮ Modal sequents for normal modal logics ⋮ A formalization of Sambins's normalization for GL ⋮ Variants of multi-relational semantics for propositional non-normal modal logics ⋮ Separation logics and modalities: a survey ⋮ A Sound Interpretation of Leśniewski's Epsilon in Modal Logic KTB ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ Unnamed Item ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ Cut Elimination for Extended Sequent Calculi ⋮ Free variable tableaux for propositional modal logics ⋮ Hintikka multiplicities in matrix decision methods for some propositional modal logics ⋮ Tableaux methods for access control in distributed systems ⋮ Tableaux for functional dependencies and independencies ⋮ Stanisław Jaśkowski and Natural Deduction Systems ⋮ Modal Tree‐Sequents ⋮ The universe of discourse of modal logic ⋮ A Note on the Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus ⋮ Labelling ideality and subideality ⋮ Through an Inference Rule, Darkly ⋮ Fibred tableaux for multi-implication logics ⋮ Almost duplication-free tableau calculi for prepositional lax logics ⋮ A simple tableau system for the logic of elsewhere ⋮ Efficient loop-check for backward proof search in some non-classical propositional logics ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ Tableaux and algorithms for Propositional Dynamic Logic with Converse ⋮ Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition ⋮ INSTANTIAL NEIGHBOURHOOD LOGIC ⋮ Unnamed Item ⋮ A Tableau Calculus for Regular Grammar Logics with Converse ⋮ Some Rough Consequence Logics and their Interrelations ⋮ Temporal Alethic Dyadic Deontic Logic and the Contrary-to-Duty Obligation Paradox ⋮ Tableaux and Hypersequents for Justification Logic ⋮ Normal forms and syntactic completeness proofs for functional independencies ⋮ Unnamed Item ⋮ Strongly analytic tableaux for normal modal logics ⋮ A multimodal logic for reasoning about complementarity ⋮ SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation ⋮ An empirical analysis of modal theorem provers ⋮ On a multilattice analogue of a hypersequent S5 calculus ⋮ Decision Procedures for a Deontic Logic Modeling Temporal Inheritance of Obligations ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ A first step towardsmodeling semistructured data in hybrid multimodal logic ⋮ Why does the proof-theory of hybrid logic work so well? ⋮ Labelled proofs for quantified modal logic ⋮ A uniform tableaux method for nonmonotonic modal logics ⋮ Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief ⋮ A tableau-like proof procedure for normal modal logics ⋮ Effective completeness theorems for modal logic ⋮ Constructive interpolation in hybrid logic ⋮ Accelerating tableaux proofs using compact representations ⋮ Cut-free sequent and tableau systems for propositional Diodorean modal logics ⋮ On interactive proof-search for constructive modal necessity ⋮ A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics ⋮ Nested sequents for intuitionistic modal logics via structural refinement ⋮ Completeness of a first-order temporal logic with time-gaps ⋮ Axiomatizations of team logics ⋮ Tableaus for many-valued modal logic ⋮ Complexity of modal logics with Presburger constraints ⋮ Modal logic via global consequence ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ Tableau method for residuated logic ⋮ Coalition Description Logic with Individuals ⋮ Positive modal logic ⋮ Dynamic squares ⋮ Natural deduction based upon strict implication for normal modal logics ⋮ A set-theoretic translation method for polymodal logics ⋮ Propositional lax logic ⋮ A logical framework for evolving software systems ⋮ Synthesis of communicating process skeletons from temporal-spatial logic specifications ⋮ A general approach for determining the validity of commonsense assertions using conditional logics ⋮ Indexed systems of sequents and cut-elimination ⋮ Connectionist modal logic: representing modalities in neural networks ⋮ Kneale's natural deductions as a notational variant of Beth's tableaus ⋮ First-order intensional logic ⋮ A theoretical investigation into quantitative modal logic ⋮ A Modal Logic of Knowledge, Belief, and Estimation ⋮ Labeled sequent calculi for modal logics and implicit contractions ⋮ Prehistoric graph in modal derivations and self-referentiality ⋮ Self-referentiality of Brouwer-Heyting-Kolmogorov semantics ⋮ Sequent systems for negative modalities ⋮ Loop-free calculus for modal logic S4. I ⋮ Introducing reactive modal tableaux ⋮ Rasiowa-Sikorski deduction systems with the rule of cut: a case study ⋮ Tableaux and hypersequents for justification logics ⋮ Prefixed tableaus and nested sequents ⋮ Definability and commonsense reasoning ⋮ A tableau-based decision procedure for CTL\(^*\)

This page was built for publication: Proof methods for modal and intuitionistic logics