A Modal-Layered Resolution Calculus for K

DOI10.1007/978-3-319-24312-2_13zbMath1471.03017OpenAlexW2240236149MaRDI QIDQ3455770

Ullrich Hustadt, Cláudia Nalon, Clare Dixon

Publication date: 11 December 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_13

zbMATH Keywords

automated reasoningnormal modal logicsresolution method

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Proof complexity of modal resolution ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ : A Resolution-Based Prover for Multimodal K ⋮ Efficient local reductions to basic modal logic ⋮ Local is best: efficient reductions to modal logic \textsf{K}

Uses Software

• E Theorem Prover
• TRP++
• HyLoRes

Cites Work

• Consequence-based and fixed-parameter tractable reasoning in description logics
• A structure-preserving clause form translation
• A guide to completeness and complexity for modal logics of knowledge and belief
• Resolution with order and selection for hybrid logics
• A note on linear resolution strategies in consequence-finding
• Using the Universal Modality: Gains and Questions
• Clausal resolution for normal modal logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Modal-Layered Resolution Calculus for K