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

DOI10.1007/S10817-022-09630-6OpenAlexW4281289051MaRDI QIDQ2102930FDOQ2102930

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)

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

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

zbMATH Keywords

modal logicstheorem provingresolution method

Mathematics Subject Classification ID

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

Cites Work

• Faster, higher, stronger: E 2.3
• MleanCoP: a connection prover for first-order modal logic
• InKreSAT: modal reasoning via incremental reduction to SAT
• 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
• Tableau methods for modal and temporal logics
• Prefixed tableaus and nested sequents
• BDD-based decision procedures for the modal logic K ★
• ExpTime tableau decision procedures for regular grammar logics with converse
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• 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
• Theorem provers for every normal modal logic
• First-order resolution methods for modal logics
• Decidability results in non-classical logics
• Labelled propositional modal logics: theory and practice
• 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
• \({\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
• Extensional higher-order paramodulation in Leo-III
• Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability

Cited In (3)

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

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)