Local reductions for the modal cube

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

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

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)

Cites Work

• TABLEAUX: A general theorem prover for modal logics
• Faster, higher, stronger: E 2.3
• The higher-order prover Leo-III
• MleanCoP: A Connection Prover for First-Order Modal Logic
• A structure-preserving clause form translation
• Handbook of modal logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Clausal resolution for normal modal logics
• Combining superposition, sorts and splitting
• 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
• Deep sequent systems for modal logic
• An optimality result for clause form translation
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• Encoding two-valued nonclassical logics in classical logic
• Resolution-based methods for modal logics
• Sequent Calculi for Normal Modal Propositional Logics
• A benchmark method for the propositional modal logics K, KT, S4
• Resolution in modal, description and hybrid logic
• Modal Resolution
• Theorem Provers For Every Normal Modal Logic
• First-order resolution methods for modal logics
• The QMLTP problem library for first-order modal 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
• Automated Reasoning with Analytic Tableaux and Related Methods
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Extensional higher-order paramodulation in Leo-III
• Labelled modal tableaux
• Herbrand style proof procedures for modal logic
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

Cited In (3)

• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Non-classical logics in satisfiability modulo theories
• Resolution calculi for non-normal modal logics

Uses Software

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

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

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