Local reductions for the modal cube
type: Item
instance of: scholarly article
title: Local reductions for the modal cube
DOI: 10.1007/978-3-031-10769-6_29
author: Cláudia Nalon
author: Ullrich Hustadt
author: Fabio Papacchini
author: Clare Dixon
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628205
describes a project that uses: TABLEAUX
describes a project that uses: Leo-III
describes a project that uses: QMLTP
describes a project that uses: SPASS
describes a project that uses: E Theorem Prover
describes a project that uses: MOIN
describes a project that uses: embed_modal
describes a project that uses: MleanCoP
describes a project that uses: LoTREC
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 29
OpenAlex ID: W4289104020
cites work: Resolution in modal, description and hybrid logic
cites work: A benchmark method for the propositional modal logics K, KT, S4
cites work: Labelled propositional modal logics: theory and practice
cites work: Q3408862
cites work: Deep sequent systems for modal logic
cites work: TABLEAUX: A general theorem prover for modal logics
cites work: Q3867808
cites work: Prefixed tableaus and nested sequents
cites work: Automated Reasoning with Analytic Tableaux and Related Methods
cites work: MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
cites work: Theorem Provers For Every Normal Modal Logic
cites work: Tableau methods for modal and temporal logics
cites work: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
cites work: Q3086941
cites work: A guide to completeness and complexity for modal logics of knowledge and belief
cites work: Resolution-based methods for modal logics
cites work: Q3842793
cites work: Single step tableaux for modal logics. Computational properties, complexity and methodology
cites work: Herbrand style proof procedures for modal logic
cites work: Clausal resolution for normal modal logics
cites work: Modal Resolution
cites work: \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
cites work: Encoding two-valued nonclassical logics in classical logic
cites work: MleanCoP: A Connection Prover for First-Order Modal Logic
cites work: Efficient local reductions to basic modal logic
cites work: A structure-preserving clause form translation
cites work: Q4028821
cites work: The QMLTP Problem Library for First-Order Modal Logics
cites work: First-Order Resolution Methods for Modal Logics
cites work: Faster, higher, stronger: E 2.3
cites work: The higher-order prover Leo-III
cites work: Extensional higher-order paramodulation in Leo-III
cites work: An optimality result for clause form translation
cites work: Sequent Calculi for Normal Modal Propositional Logics
cites work: Combining superposition, sorts and splitting
description: scientific article; zbMATH DE number 7628205