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

• scientific article; zbMATH DE number 1192312 (Why is no real title available?)
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 140411 (Why is no real title available?)
• A benchmark method for the propositional modal logics K, KT, S4
• A guide to completeness and complexity for modal logics of knowledge and belief
• A structure-preserving clause form translation
• An optimality result for clause form translation
• Automated Reasoning with Analytic Tableaux and Related Methods
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Clausal resolution for normal modal logics
• Combining superposition, sorts and splitting
• Deep sequent systems for modal logic
• Efficient local reductions to basic modal logic
• Encoding two-valued nonclassical logics in classical logic
• Extensional higher-order paramodulation in Leo-III
• Faster, higher, stronger: E 2.3
• First-order resolution methods for modal logics
• Handbook of modal logic
• Herbrand style proof procedures for modal logic
• Labelled modal tableaux
• Labelled propositional modal logics: theory and practice
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• MleanCoP: a connection prover for first-order modal logic
• Modal Resolution
• Prefixed tableaus and nested sequents
• Resolution in modal, description and hybrid logic
• Resolution-based methods for modal logics
• Sequent Calculi for Normal Modal Propositional Logics
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• TABLEAUX: A general theorem prover for modal logics
• Tableau methods for modal and temporal logics
• The QMLTP problem library for first-order modal logics
• The higher-order prover Leo-III
• Theorem provers for every normal modal logic
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments

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

Describes a project that uses

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)