Resolution-based methods for modal logics
From MaRDI portal
Publication:4487263
DOI10.1093/jigpal/8.3.265zbMath0947.03014MaRDI QIDQ4487263
Hans de Nivelle, Renate A. Schmidt, Ullrich Hustadt
Publication date: 7 November 2000
Published in: Logic Journal of IGPL (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/bfd93c6e5f2e51892715f54d87df751816e30ef5
survey; tableaux; guarded fragment; description logic; inference methods; model generation; decision procedures; multi-modal logics; resolution methods; solvable classes; extended propositional modal logics
03B45: Modal logic (including the logic of norms)
03B35: Mechanization of proofs and logical operations
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
First-Order Resolution Methods for Modal Logics, Modal Satisfiability via SMT Solving, Using tableau to decide description logics with full role negation and identity, Rewriting Conjunctive Queries over Description Logic Knowledge Bases, Proof Complexity of Non-classical Logics, A description logic based situation calculus, Deciding expressive description logics in the framework of resolution, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., A new methodology for developing deduction methods, Hyperresolution for guarded formulae, Clausal resolution in a logic of rational agency, Constrained consequence, Local reductions for the modal cube, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), Blocking and other enhancements for bottom-up model generation methods, Resolution with order and selection for hybrid logics, Deciding regular grammar logics with converse through first-order logic, A Tableau Calculus for Minimal Modal Model Generation, Simulation and Synthesis of Deduction Calculi
Uses Software
