Efficient local reductions to basic modal logic

DOI10.1007/978-3-030-79876-5_5OpenAlexW3176063663MaRDI QIDQ2055845FDOQ2055845

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

Publication date: 1 December 2021

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

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
• Publication:4207883

Mathematics Subject Classification ID

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

Cites Work

• The higher-order prover Leo-III
• MleanCoP: a connection prover for first-order modal logic
• Clausal resolution for normal modal logics
• Combining superposition, sorts and splitting
• Multimodal and intuitionistic logics in simple type theory
• A guide to completeness and complexity for modal logics of knowledge and belief
• Prefixed tableaus and nested sequents
• BDD-based decision procedures for the modal logic K ★
• ExpTime tableau decision procedures for regular grammar logics with converse
• Encoding two-valued nonclassical logics in classical logic
• Decidability by resolution for propositional modal logics
• A benchmark method for the propositional modal logics K, KT, S4
• A Modal-Layered Resolution Calculus for K
• Modal Resolution
• Reducing Modal Consequence Relations
• First-order resolution methods for modal logics
• Decidability results in non-classical logics
• Labelled propositional modal logics: theory and practice
• \(\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
• The axiomatic translation principle for modal logic
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods

Cited In (6)

• Solving modal logic problems by translation to higher-order logic
• Local reductions for the modal cube
• 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)