Efficient local reductions to basic modal logic

DOI10.1007/978-3-030-79876-5_5MaRDI QIDQ2055845zbMATH OpenOpenAlexFDO

Authors Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Local is best: efficient reductions to modal logic \textsf{K}
• Improved decision procedures for the modal logics K, T and S4
• A benchmark method for the propositional modal logics K, KT, S4
• 3-SAT = SAT for a class of normal modal logics
• scientific article; zbMATH DE number 4128785

Cites work

• scientific article; zbMATH DE number 2196594 (Why is no real title available?)
• A Modal-Layered Resolution Calculus for K
• A benchmark method for the propositional modal logics K, KT, S4
• A guide to completeness and complexity for modal logics of knowledge and belief
• Automated Reasoning with Analytic Tableaux and Related Methods
• BDD-based decision procedures for the modal logic K ★
• Clausal resolution for normal modal logics
• Combining superposition, sorts and splitting
• Decidability by resolution for propositional modal logics
• Decidability results in non-classical logics
• Encoding two-valued nonclassical logics in classical logic
• ExpTime tableau decision procedures for regular grammar logics with converse
• First-order resolution methods for modal logics
• Labelled propositional modal logics: theory and practice
• MleanCoP: a connection prover for first-order modal logic
• Modal Resolution
• Multimodal and intuitionistic logics in simple type theory
• Prefixed tableaus and nested sequents
• Reducing Modal Consequence Relations
• The axiomatic translation principle for modal logic
• The higher-order prover Leo-III
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K

Cited in

(6)

• Local reductions for the modal cube
• Solving modal logic problems by translation to higher-order logic
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Local is best: efficient reductions to modal logic \textsf{K}
• Theorem proving using clausal resolution: from past to present
• Resolution calculi for non-normal modal logics

This page was built for publication: Efficient local reductions to basic modal logic

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