Efficient local reductions to basic modal logic

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

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

Publication date: 1 December 2021

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)

Related Items (4)

Solving modal logic problems by translation to higher-order logic ⋮ Theorem proving using clausal resolution: from past to present ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube

Cites Work

• 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
• The higher-order prover Leo-III
• A benchmark method for the propositional modal logics K, KT, S4
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• : 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 ★
• Decidability results in non-classical logics
• Labelled propositional modal logics: theory and practice
• Reducing Modal Consequence Relations
• First-Order Resolution Methods for Modal Logics
• 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: Efficient local reductions to basic modal logic