Proof methods for modal and intuitionistic logics

zbMATH Open0523.03013MaRDI QIDQ1056744FDOQ1056744

Publication date: 1983

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

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

Mathematics Subject Classification ID

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

Cited In (only showing first 100 items - show all)

Blocking and other enhancements for bottom-up model generation methods
Inducing syntactic cut-elimination for indexed nested sequents
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
Linear reasoning in modal logic
On Blass translation for Leśniewski's propositional ontology and modal logics
Approximations of modal logics: \(\mathbf K\) and beyond
A theoretical investigation into quantitative modal logic
From Schütte’s Formal Systems to Modern Automated Deduction
Synthesis of communicating process skeletons from temporal-spatial logic specifications
Representing scope in intuitionistic deductions
Proof methods for reasoning about possibility and necessity
Variants of multi-relational semantics for propositional non-normal modal logics
A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
Hypersequent calculi for S5: the methods of cut elimination
Tautology elimination, cut elimination, and S5
On interactive proof-search for constructive modal necessity
Definability and commonsense reasoning
Dynamic squares
Nested sequents for intuitionistic modal logics via structural refinement
A logical framework for evolving software systems
Complexity of modal logics with Presburger constraints
Modal logic via global consequence
Intuitionistic Decision Procedures Since Gentzen
On a multilattice analogue of a hypersequent S5 calculus
A tableau-like proof procedure for normal modal logics
Barcan Both Ways
Free variable tableaux for propositional modal logics
Completeness of a first-order temporal logic with time-gaps
A uniform tableau method for intuitionistic modal logics. I
Tableaux for functional dependencies and independencies
Hintikka multiplicities in matrix decision methods for some propositional modal logics
Introducing reactive modal tableaux
Kneale's natural deductions as a notational variant of Beth's tableaus
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
Rasiowa-Sikorski deduction systems with the rule of cut: a case study
Preservation of Craig interpolation by the product of matrix logics
Multicomponent proof-theoretic method for proving interpolation properties
Accelerating tableaux proofs using compact representations
Interpolation method for multicomponent sequent calculi
Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
Title not available (Why is that?)
Sequent systems for negative modalities
A modal logic of knowledge, belief, and estimation
Modal Tree‐Sequents
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
Automated inferencing
Converting non-classical matrix proofs into sequent-style systems
``That will do: logics of deontic necessity and sufficiency
Formalizing a Seligman-style tableau system for hybrid logic (short paper)
Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
Almost duplication-free tableau calculi for propositional lax logics
Natural deduction based upon strict implication for normal modal logics
Instantial neighbourhood logic
Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
Loop-free calculus for modal logic S4. I
The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G.
A four-valued dynamic epistemic logic
Propositional lax logic
A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics
Theory matrices (for modal logics) using alphabetical monotonicity
First-order intensional logic
Tableaux and algorithms for Propositional Dynamic Logic with Converse
A general tableau method for propositional interval temporal logics: theory and implementation
Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition
Nested sequents for intuitionistic logics
An intriguing logic with two implicational connectives
Tableau method for residuated logic
Interpolation for first order S5
Some Rough Consequence Logics and their Interrelations
Separation logics and modalities: a survey
Effective completeness theorems for modal logic
On multiple conclusion deductions in classical logic
Display calculi and other modal calculi: a comparison
Metatheory of actions: beyond consistency
Contraction-free sequent calculi for intuitionistic logic
On graph calculi for multi-modal logics
Prehistoric graph in modal derivations and self-referentiality
A multimodal logic for reasoning about complementarity
A tableau-based decision procedure for CTL\(^*\)
Temporal alethic-deontic logic and semantic tableaux
A loop-free decision procedure for modal propositional logics K4, S4 and S5
Indexed systems of sequents and cut-elimination
An epistemic model of logic programming
Connectionist modal logic: representing modalities in neural networks
Proof analysis in modal logic
EXPtime tableaux for ALC
A general approach for determining the validity of commonsense assertions using conditional logics
Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different
Uniform and non uniform strategies for tableaux calculi for modal logics
Axiomatizations of team logics
Positive modal logic
Tableaux for constructive concurrent dynamic logic
A category-theoretic approach to social network analysis
On graphs for intuitionistic modal logics
A uniform procedure for converting matrix proofs into sequent-style systems
Local model checking for infinite state spaces
An empirical analysis of modal theorem provers
Hypersequent and display calculi -- a unified perspective
Combining deduction and model checking into tableaux and algorithms for converse-PDL.

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

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