Resolution-based methods for modal logics
From MaRDI portal
Publication:4487263
DOI10.1093/jigpal/8.3.265zbMath0947.03014OpenAlexW2146427628MaRDI 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
surveytableauxguarded fragmentdescription logicinference methodsmodel generationdecision proceduresmulti-modal logicsresolution methodssolvable classesextended propositional modal logics
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
Simulation and Synthesis of Deduction Calculi, A description logic based situation calculus, Constrained consequence, Hyperresolution for guarded formulae, Resolution with order and selection for hybrid logics, Deciding expressive description logics in the framework of resolution, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), Using tableau to decide description logics with full role negation and identity, First-Order Resolution Methods for Modal Logics, Proof Complexity of Non-classical Logics, Blocking and other enhancements for bottom-up model generation methods, A Tableau Calculus for Minimal Modal Model Generation, A new methodology for developing deduction methods, Deciding regular grammar logics with converse through first-order logic, Rewriting Conjunctive Queries over Description Logic Knowledge Bases, Modal Satisfiability via SMT Solving, Local reductions for the modal cube, Clausal resolution in a logic of rational agency
Uses Software
