Tableau methods for modal and temporal logics
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 3937153
- Tableaus for many-valued modal logic
- TABLEAUX: A general theorem prover for modal logics
- Tableaux for relation-changing modal logics
- A general tableau method for propositional interval temporal logics
- Tableau methods for substructural logics
- Tableau metatheorem for modal logics
- A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
- A general tableau method for propositional interval temporal logics: theory and implementation
- Tableau method for residuated logic
Cited in
(95)- The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G.
- Proof theory for admissible rules
- Dual systems of tableaux and sequents for PLTL
- A new methodology for developing deduction methods
- Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom
- Hyperresolution for guarded formulae
- EXPtime tableaux for ALC
- Pure modal logic of names and tableau systems
- On refutation rules
- Constrained consequence
- Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
- Cut-elimination for weak Grzegorczyk logic Go
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Local is best: efficient reductions to modal logic \textsf{K}
- Local reductions for the modal cube
- A formally verified cut-elimination procedure for linear nested sequents for tense logic
- Tableaux for some modal-tense logics Graham Priest's fashion
- Uniform interpolation via nested sequents
- Proofs and countermodels in non-classical logics
- A loop-free decision procedure for modal propositional logics K4, S4 and S5
- Labelled tableau systems for some subintuitionistic logics
- In all but finitely many possible worlds: model-theoretic investigations on `\textit{overwhelming majority}' default conditionals
- The modal logic of copy and remove
- Tableaux for constructive concurrent dynamic logic
- Deciding regular grammar logics with converse through first-order logic
- Complexity of modal logics with Presburger constraints
- Modal logic S5 in answer set programming with lazy creation of worlds
- scientific article; zbMATH DE number 1612547 (Why is no real title available?)
- On the complexity of the equational theory of residuated Boolean algebras
- Tableau method and NEXPTIME-completeness of DEL-sequents
- Query answering with DBoxes is hard
- Testing XML constraint satisfiability
- Designing tableau-like axiomatization for propositional linear temporal logic at home of Arthur Prior
- Tableaux for Reasoning about Atomic Updates
- Tableau reductions: towards an optimal decision procedure for the modal necessity
- A history of until
- Coalition description logic with individuals
- Intuitionistic Decision Procedures Since Gentzen
- A new modal framework for epistemic logic
- Modal tableau systems with blocking and congruence closure
- Mīmāṃsā Deontic Logic: Proof Theory and Applications
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- On contraction and the modal fragment
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- Invariant-free clausal temporal resolution
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
- An efficient relational deductive system for propositional non-classical logics
- Labeled sequent calculi for modal logics and implicit contractions
- scientific article; zbMATH DE number 1189099 (Why is no real title available?)
- Tableaux and hypersequents for justification logics
- Prefixed tableaus and nested sequents
- A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
- Barcan Both Ways
- scientific article; zbMATH DE number 1775472 (Why is no real title available?)
- Definability in the class of all KD45-frames -- computability and complexity
- Free variable tableaux for propositional modal logics
- scientific article; zbMATH DE number 3997757 (Why is no real title available?)
- First-order resolution methods for modal logics
- Model Theoretic Syntax and Parsing
- Terminating Tableau Calculi for Hybrid Logics Extending K
- On logic of strictly-deontic modalities. A semantic and tableau approach
- Modal logic S5 satisfiability in answer set programming
- Extending fairness expressibility of ECTL^+: a tree-style one-pass tableau approach
- A note on the complexity of \textbf{S4.2}
- A Tableau Calculus for Regular Grammar Logics with Converse
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Tableau metatheorem for modal logics
- Automated Reasoning
- LINEAR TIME IN HYPERSEQUENT FRAMEWORK
- From KLM-style conditionals to defeasible modalities, and back
- Tableau Development for a Bi-intuitionistic Tense Logic
- Instantial neighbourhood logic
- Copy and remove as dynamic operators
- Verified Decision Procedures for Modal Logics.
- Shortcuts and dynamic marking in the tableau method for adaptive logics
- A tableau method for graded intersections of modalities: A case for concept languages
- First-order intensional logic
- One-pass Context-based Tableaux Systems for CTL and ECTL
- On the decidability of a fragment of preferential LTL
- Focus-style proofs for the two-way alternation-free \(\mu \)-calculus
- Cut elimination in coalgebraic logics
- Complexity of hybrid logics over transitive frames
- Parametrized modal logic. II: The unidimensional case
- Automated deduction
- Proof analysis in intermediate logics
- Refined tableau systems for some modal logics of confluence
- From modal sequent calculi to modal resolution
- Extending defeasibility for propositional standpoint logics
- Refutations and proofs in the paraconsistent modal logics: \textbf{KN4} and \textbf{KN4.D}
- A proof-theoretic approach to formal epistemology
- Nested sequents or tree-hypersequents -- a survey
- ExpTime tableau decision procedures for regular grammar logics with converse
- Symmetric blocking
- Cut-free sequent systems for temporal logic
This page was built for publication: Tableau methods for modal and temporal logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753601)
