scientific article

From MaRDI portal

zbMath0972.03529MaRDI QIDQ2753601

Rajeev Goré

Publication date: 14 November 2001


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

Barcan Both Ways, A formally verified cut-elimination procedure for linear nested sequents for tense logic, Tableau reductions: towards an optimal decision procedure for the modal necessity, Modal Tableau Systems with Blocking and Congruence Closure, Mīmāṃsā Deontic Logic: Proof Theory and Applications, Complexity of modal logics with Presburger constraints, Uniform interpolation via nested sequents, A History of Until, Coalition Description Logic with Individuals, ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching, Invariant-free clausal temporal resolution, In all but finitely many possible worlds: model-theoretic investigations on `\textit{overwhelming majority}' default conditionals, The modal logic of copy and remove, First-order intensional logic, Labeled sequent calculi for modal logics and implicit contractions, Definability in the class of all -frames – computability and complexity, LINEAR TIME IN HYPERSEQUENT FRAMEWORK, Cut elimination in coalgebraic logics, Tableaux and hypersequents for justification logics, Prefixed tableaus and nested sequents, Focus-style proofs for the two-way alternation-free \(\mu \)-calculus, Symmetric blocking, On refutation rules, Constrained consequence, Hyperresolution for guarded formulae, Complexity of hybrid logics over transitive frames, Modal logic S5 in answer set programming with lazy creation of worlds, On contraction and the modal fragment, Free variable tableaux for propositional modal logics, Unnamed Item, Unnamed Item, From KLM-style conditionals to defeasible modalities, and back, Proof analysis in intermediate logics, Verified Decision Procedures for Modal Logics., Cut-free sequent systems for temporal logic, Intuitionistic Decision Procedures Since Gentzen, A note on the complexity of S4.2, Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\), One-pass Context-based Tableaux Systems for CTL and ECTL, First-Order Resolution Methods for Modal Logics, Proofs and countermodels in non-classical logics, INSTANTIAL NEIGHBOURHOOD LOGIC, Model Theoretic Syntax and Parsing, Cut-elimination for weak Grzegorczyk logic Go, A loop-free decision procedure for modal propositional logics K4, S4 and S5, A Tableau Calculus for Regular Grammar Logics with Converse, Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4F, S4R, S4M and G., Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach, On the Complexity of the Equational Theory of Residuated Boolean Algebras, Proof theory for admissible rules, Query Answering with DBoxes is Hard, Terminating Tableau Calculi for Hybrid Logics Extending K, ExpTime tableau decision procedures for regular grammar logics with converse, An efficient relational deductive system for propositional non-classical logics, 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, Deciding regular grammar logics with converse through first-order logic, Labelled tableau systems for some subintuitionistic logics, On Logic of Strictly-Deontic Modalities. A Semantic and Tableau Approach, EXPtime tableaux for ALC, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models, Tableau Metatheorem for Modal Logics, Copy and remove as dynamic operators, Local is best: efficient reductions to modal logic \textsf{K}, Local reductions for the modal cube, Testing XML constraint satisfiability, Modal Logic S5 Satisfiability in Answer Set Programming


Uses Software