Proof methods for modal and intuitionistic logics
From MaRDI portal
Publication:1056744
Cited in
(only showing first 100 items - show all)- A uniform tableau method for intuitionistic modal logics. I
- An empirical analysis of modal theorem provers
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- Decidability of a hybrid duration calculus
- Belief, information acquisition, and trust in multi-agent systems -- a modal logic formulation
- Tableaux for functional dependencies and independencies
- Normative reasoning and consequence
- Efficient loop-check for backward proof search in some non-classical propositional logics
- Prefixed tableaus and nested sequents
- Tableaux and hypersequents for justification logics
- Hintikka multiplicities in matrix decision methods for some propositional modal logics
- Introducing reactive modal tableaux
- The universe of discourse of modal logic
- Kneale's natural deductions as a notational variant of Beth's tableaus
- A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
- Multicomponent proof-theoretic method for proving interpolation properties
- Rasiowa-Sikorski deduction systems with the rule of cut: a case study
- Power and limits of structural display rules
- Preservation of Craig interpolation by the product of matrix logics
- Decision procedures for a deontic logic modeling temporal inheritance of obligations
- Proof analysis in intermediate logics
- Accelerating tableaux proofs using compact representations
- Cut Elimination for Extended Sequent Calculi
- Combining intuitionistic and classical propositional logic: Gentzenization and Craig interpolation
- Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
- Interpolation method for multicomponent sequent calculi
- A first step towards modeling semistructured data in hybrid multimodal logic
- A set-theoretic translation method for polymodal logics
- A Tableau Calculus for Regular Grammar Logics with Converse
- Sequent systems for negative modalities
- scientific article; zbMATH DE number 6987093 (Why is no real title available?)
- Constructive modal logics. I
- Cut-free sequent and tableau systems for propositional Diodorean modal logics
- Possible worlds in use
- Uniform Lyndon interpolation property in propositional modal logics
- Mechanising Gödel-Löb provability logic in HOL light
- TABLEAUX: A general theorem prover for modal logics
- ExpTime tableau decision procedures for regular grammar logics with converse
- Modal sequents for normal modal logics
- Tableaux and Hypersequents for Justification Logic
- Tableau for the logic ILP
- A simple propositional \(\text{S}5\) tableau system
- Reference and perspective in intuitionistic logics
- Automata can show PSpace results for description logics
- Constructive interpolation in hybrid logic
- A modal logic of knowledge, belief, and estimation
- Modal Tree‐Sequents
- A tableaux calculus for default intuitionistic logic
- Higher-order syntax and saturation algorithms for hybrid logic
- Tableaus for many-valued modal logic
- THE LOGIC OF SEQUENCE FRAMES
- A Note on the Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus
- Labeled sequent calculi for modal logics and implicit contractions
- Strongly analytic tableaux for normal modal logics
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Automated inferencing
- Testing XML constraint satisfiability
- ``That will do: logics of deontic necessity and sufficiency
- Converting non-classical matrix proofs into sequent-style systems
- Finite and physical modalities
- Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere
- Labelled proofs for quantified modal logic
- Formalizing a Seligman-style tableau system for hybrid logic (short paper)
- A general schema for bilateral proof rules
- Normal forms and syntactic completeness proofs for functional independencies
- 3-SAT = SAT for a class of normal modal logics
- Natural deduction based upon strict implication for normal modal logics
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
- Loop-free calculus for modal logic S4. I
- Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
- Almost duplication-free tableau calculi for propositional lax logics
- The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G.
- Instantial neighbourhood logic
- Through an inference rule, darkly
- Blocking and other enhancements for bottom-up model generation methods
- 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
- A four-valued dynamic epistemic logic
- Inducing syntactic cut-elimination for indexed nested sequents
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Tableaux and algorithms for Propositional Dynamic Logic with Converse
- Improved decision procedures for the modal logics K, T and S4
- On the modal logic K plus theories
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- Temporal alethic dyadic deontic logic and the contrary-to-duty obligation paradox
- An intriguing logic with two implicational connectives
- Why does the proof-theory of hybrid logic work so well?
- A general tableau method for propositional interval temporal logics: theory and implementation
- A uniform tableaux method for nonmonotonic modal logics
- Nested sequents for intuitionistic logics
- Tableau method for residuated logic
- Labelled tableau systems for some subintuitionistic logics
- Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition
- Linear reasoning in modal logic
- 1998 European Summer Meeting of the Association for Symbolic Logic
- Interpolation for first order S5
- On Blass translation for Leśniewski's propositional ontology and modal logics
- Some Rough Consequence Logics and their Interrelations
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)
