Resolution-based methods for modal logics

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

zbMATH Keywords

surveytableauxguarded fragmentdescription logicinference methodsmodel generationdecision proceduresmulti-modal logicsresolution methodssolvable classesextended propositional modal logics

Mathematics Subject Classification ID

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 (19)

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

• OTTER
• SPASS
• Bliksem

This page was built for publication: Resolution-based methods for modal logics