Proof methods for modal and intuitionistic logics
From MaRDI portal
Publication:1056744
Cited in
(only showing first 100 items - show all)- The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G.
- Reference and perspective in intuitionistic logics
- Metatheory of actions: beyond consistency
- Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
- Automated inferencing
- Synthesis of communicating process skeletons from temporal-spatial logic specifications
- TABLEAUX: A general theorem prover for modal logics
- Local model checking for infinite state spaces
- Representing scope in intuitionistic deductions
- A simple propositional \(\text{S}5\) tableau system
- Proof methods for reasoning about possibility and necessity
- A uniform tableau method for intuitionistic modal logics. I
- A tableau-like proof procedure for normal modal logics
- Accelerating tableaux proofs using compact representations
- Cut-free sequent and tableau systems for propositional Diodorean modal logics
- A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
- Completeness of a first-order temporal logic with time-gaps
- Tableau method for residuated logic
- Propositional lax logic
- Indexed systems of sequents and cut-elimination
- Definability and commonsense reasoning
- EXPtime tableaux for ALC
- Prehistoric graph in modal derivations and self-referentiality
- Sequent systems for negative modalities
- ``That will do: logics of deontic necessity and sufficiency
- On graphs for intuitionistic modal logics
- Multicomponent proof-theoretic method for proving interpolation properties
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- A uniform procedure for converting matrix proofs into sequent-style systems
- Effective completeness theorems for modal logic
- Tableaus for many-valued modal logic
- Positive modal logic
- Dynamic squares
- Natural deduction based upon strict implication for normal modal logics
- A set-theoretic translation method for polymodal logics
- A logical framework for evolving software systems
- A theoretical investigation into quantitative modal logic
- Introducing reactive modal tableaux
- Temporal alethic-deontic logic and semantic tableaux
- Formalizing a Seligman-style tableau system for hybrid logic (short paper)
- On Blass translation for Leśniewski's propositional ontology and modal logics
- On interactive proof-search for constructive modal necessity
- Nested sequents for intuitionistic modal logics via structural refinement
- Modal logic via global consequence
- Kneale's natural deductions as a notational variant of Beth's tableaus
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- A four-valued dynamic epistemic logic
- Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different
- Hypersequent and display calculi -- a unified perspective
- A loop-free decision procedure for modal propositional logics K4, S4 and S5
- Blocking and other enhancements for bottom-up model generation methods
- A tableaux calculus for default intuitionistic logic
- Labelled tableau systems for some subintuitionistic logics
- Rasiowa-Sikorski deduction systems with the rule of cut: a case study
- Nested sequents for intuitionistic logics
- Preservation of Craig interpolation by the product of matrix logics
- Approximations of modal logics: K and beyond
- Tableaux for constructive concurrent dynamic logic
- Connectionist computations of intuitionistic reasoning
- A general tableau method for propositional interval temporal logics: theory and implementation
- Axiomatizations of team logics
- Complexity of modal logics with Presburger constraints
- Inducing syntactic cut-elimination for indexed nested sequents
- A category-theoretic approach to social network analysis
- Higher-order syntax and saturation algorithms for hybrid logic
- Testing XML constraint satisfiability
- Decidability of a hybrid duration calculus
- A modal logic of knowledge, belief, and estimation
- Hypersequent calculi for S5: the methods of cut elimination
- Interpolation for first order S5
- Constructive interpolation in hybrid logic
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Coalition description logic with individuals
- A general approach for determining the validity of commonsense assertions using conditional logics
- Intuitionistic Decision Procedures Since Gentzen
- Through an inference rule, darkly
- On a multilattice analogue of a hypersequent S5 calculus
- Some Rough Consequence Logics and their Interrelations
- Tableaux and Hypersequents for Justification Logic
- A first step towards modeling semistructured data in hybrid multimodal logic
- Why does the proof-theory of hybrid logic work so well?
- Linear reasoning in modal logic
- Labeled sequent calculi for modal logics and implicit contractions
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
- Loop-free calculus for modal logic S4. I
- Contraction-free sequent calculi for intuitionistic logic
- Tableaux and hypersequents for justification logics
- Prefixed tableaus and nested sequents
- A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
- 1998 European Summer Meeting of the Association for Symbolic Logic
- A translation from the modal logic of provability into K4
- Modal sequents for normal modal logics
- A formalization of Sambins's normalization for GL
- A tableau-based decision procedure for CTL^*
- 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
- Barcan Both Ways
- Inducing syntactic cut-elimination for indexed nested sequents
- Tautology elimination, cut elimination, and S5
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)
