Local is best: efficient reductions to modal logic \textsf{K}

DOI10.1007/S10817-022-09630-6MaRDI QIDQ2102930zbMATH OpenOpenAlexFDO

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

Publication date 12 December 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-022-09630-6

zbMATH Keywords

modal logicstheorem provingresolution method

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• 3-SAT = SAT for a class of normal modal logics
• Correction to: ``Local is best: efficient reductions to modal logic \textsf{K}
• InKreSAT: modal reasoning via incremental reduction to SAT
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• A benchmark method for the propositional modal logics K, KT, S4

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
• Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability
• 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
• Efficient local reductions to basic modal logic
• Encoding two-valued nonclassical logics in classical logic
• ExpTime tableau decision procedures for regular grammar logics with converse
• Extensional higher-order paramodulation in Leo-III
• Faster, higher, stronger: E 2.3
• First-order resolution methods for modal logics
• InKreSAT: modal reasoning via incremental reduction to SAT
• 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
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• Tableau methods for modal and temporal logics
• The axiomatic translation principle for modal logic
• Theorem provers for every normal modal logic
• \(\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

(4)

• Efficient local reductions to basic modal logic
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Not all Kripke models of \(\mathsf{HA}\) are locally \(\mathsf{PA}\)
• Correction to: ``Local is best: efficient reductions to modal logic \textsf{K}

Describes a project that uses

Uses Software

• SPASS
• LoTREC
• E Theorem Prover
• Leo-III
• MleanCoP
• InKreSAT
• embed_modal

This page was built for publication: Local is best: efficient reductions to modal logic \textsf{K}

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