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)

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
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
Power and Limits of Structural Display Rules
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.
Efficient loop-check for backward proof search in some non-classical propositional logics
Belief, information acquisition, and trust in multi-agent systems -- a modal logic formulation
Prefixed tableaus and nested sequents
Tableaux and hypersequents for justification logics
Proof analysis in intermediate logics
A Tableau Calculus for Regular Grammar Logics with Converse
A first step towards modeling semistructured data in hybrid multimodal logic
A set-theoretic translation method for polymodal logics
Constructive modal logics. I
Cut-free sequent and tableau systems for propositional Diodorean modal logics
INSTANTIAL NEIGHBOURHOOD LOGIC
Possible worlds in use
Uniform Lyndon interpolation property in propositional modal logics
Modal sequents for normal modal logics
TABLEAUX: A general theorem prover for modal logics
ExpTime tableau decision procedures for regular grammar logics with converse
Tableaux and Hypersequents for Justification Logic
Constructive interpolation in hybrid logic
A simple propositional \(\text{S}5\) tableau system
Reference and perspective in intuitionistic logics
Automata can show PSpace results for description logics
Title not available (Why is that?)
Higher-order syntax and saturation algorithms for hybrid logic
Tableaus for many-valued modal logic
Strongly analytic tableaux for normal modal logics
Labeled sequent calculi for modal logics and implicit contractions
Labelled proofs for quantified modal logic
Finite and physical modalities
Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere
3-SAT = SAT for a class of normal modal logics
Blocking and other enhancements for bottom-up model generation methods
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
A Modal Logic of Knowledge, Belief, and Estimation
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
Inducing Syntactic Cut-Elimination for Indexed Nested Sequents
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
Interpolation Method for Multicomponent Sequent Calculi
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

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)