Local reductions for the modal cube

DOI10.1007/978-3-031-10769-6_29OpenAlexW4289104020MaRDI QIDQ2104538

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

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_29

Mathematics Subject Classification ID

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

Uses Software

• SPASS
• LoTREC
• QMLTP
• E Theorem Prover
• TABLEAUX
• Leo-III
• MleanCoP
• GitHub
• embed_modal
• MOIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Prefixed tableaus and nested sequents
• Deep sequent systems for modal logic
• A structure-preserving clause form translation
• TABLEAUX: A general theorem prover for modal logics
• A guide to completeness and complexity for modal logics of knowledge and belief
• An optimality result for clause form translation
• The higher-order prover Leo-III
• 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
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• \(\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
• Resolution in Modal, Description and Hybrid Logic
• The QMLTP Problem Library for First-Order Modal Logics
• MleanCoP: A Connection Prover for First-Order Modal Logic
• Herbrand style proof procedures for modal logic
• Sequent Calculi for Normal Modal Propositional Logics
• Labelled propositional modal logics: theory and practice
• Resolution-based methods for modal logics
• Theorem Provers For Every Normal Modal Logic
• First-Order Resolution Methods for Modal Logics
• Modal Resolution
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• Clausal resolution for normal modal logics
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Local reductions for the modal cube