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

DOI10.1007/s10817-022-09630-6OpenAlexW4281289051MaRDI QIDQ2102930

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

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

zbMATH Keywords

theorem provingmodal logicsresolution method

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Prefixed tableaus and nested sequents
• ExpTime tableau decision procedures for regular grammar logics with converse
• A guide to completeness and complexity for modal logics of knowledge and belief
• Decidability by resolution for propositional modal logics
• A benchmark method for the propositional modal logics K, KT, S4
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• 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
• Faster, higher, stronger: E 2.3
• Extensional higher-order paramodulation in Leo-III
• : A Resolution-Based Prover for Multimodal K
• Multimodal and intuitionistic logics in simple type theory
• MleanCoP: A Connection Prover for First-Order Modal Logic
• A Modal-Layered Resolution Calculus for K
• BDD-based decision procedures for the modal logic K ★
• Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
• Decidability results in non-classical logics
• Labelled propositional modal logics: theory and practice
• Reducing Modal Consequence Relations
• Theorem Provers For Every Normal Modal Logic
• First-Order Resolution Methods for Modal Logics
• InKreSAT: Modal Reasoning via Incremental Reduction to SAT
• Modal Resolution
• The axiomatic translation principle for modal logic
• Clausal resolution for normal modal logics
• Automated Reasoning with Analytic Tableaux and Related Methods

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