A Modal-Layered Resolution Calculus for K

DOI10.1007/978-3-319-24312-2_13MaRDI QIDQ3455770zbMATH OpenOpenAlexFDO

Authors Cláudia Nalon, Ullrich Hustadt, 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

normal modal logicsresolution methodautomated reasoning

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)

Recommendations

• scientific article; zbMATH DE number 4055570
• scientific article; zbMATH DE number 4027426
• Resolution calculi for modal logics
• Modal Resolution
• Resolution-based calculi for modal and temporal logics
• scientific article; zbMATH DE number 1880278
• A note on Kripke semantics for residuated logic
• Resolution-based methods for modal logics
• Resolution theorem proving in reified modal logics
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K

Cites work

• scientific article; zbMATH DE number 67503 (Why is no real title available?)
• scientific article; zbMATH DE number 1341615 (Why is no real title available?)
• scientific article; zbMATH DE number 559756 (Why is no real title available?)
• scientific article; zbMATH DE number 2090297 (Why is no real title available?)
• scientific article; zbMATH DE number 757645 (Why is no real title available?)
• scientific article; zbMATH DE number 5043325 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3346109 (Why is no real title available?)
• A guide to completeness and complexity for modal logics of knowledge and belief
• A note on linear resolution strategies in consequence-finding
• A structure-preserving clause form translation
• Clausal resolution for normal modal logics
• Consequence-based and fixed-parameter tractable reasoning in description logics
• Modal logic
• Resolution with order and selection for hybrid logics
• Using the Universal Modality: Gains and Questions

Cited in

(10)

• Proof complexity of modal resolution
• Logic for Programming, Artificial Intelligence, and Reasoning
• Clausal resolution for normal modal logics
• Model construction for modal clauses
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
• Efficient local reductions to basic modal logic
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Local is best: efficient reductions to modal logic \textsf{K}
• Modal Resolution

Describes a project that uses

Uses Software

• HyLoRes
• TRP++
• E Theorem Prover

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3455770)