Resolution calculi for non-normal modal logics
type: Item
instance of: scholarly article
title: Resolution calculi for non-normal modal logics
DOI: 10.1007/978-3-031-43513-3_18
author: Dirk Pattinson
author: N. Olivetti
author: Cláudia Nalon
publication date: 2024-05-17T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7850752
zbMATH Keywords: modal logic
zbMATH Keywords: automated reasoning
zbMATH Keywords: resolution
MaRDI profile type: Publication
cites work: Q3030268
cites work: Q4263164
cites work: Linear strategy for propositional modal resolution
cites work: A simple deduction method for modal logic
cites work: The recursive resolution method for modal logic
cites work: Q3867808
cites work: Resolution for some first-order modal systems
cites work: Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity
cites work: Q5224565
cites work: Implementing Superposition in iProver (System Description)
cites work: Q4942680
cites work: Modal resolution in clausal form
cites work: Destructive Modal Resolution
cites work: Modular sequent calculi for classical modal logics
cites work: SAT-based decision procedures for classical modal logics
cites work: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
cites work: Implementing Tableau Calculi Using BDDs: BDDTab System Description
cites work: The intractability of resolution
cites work: Q3435245
cites work: Q3105688
cites work: InKreSAT: Modal Reasoning via Incremental Reduction to SAT
cites work: Sequent calculi and decision procedures for weak modal systems
cites work: Modularisation of Sequent Calculi for Normal and Non-normal Modalities
cites work: Q3972527
cites work: Clausal resolution for normal modal logics
cites work: Modal Resolution
cites work: : A Resolution-Based Prover for Multimodal K
cites work: \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
cites work: Local reductions for the modal cube
cites work: Clausal Resolution for Modal Logics of Confluence
cites work: Resolution-based methods for modal logics
cites work: Semantics-Based Translation Methods for Modal Logics
cites work: Q5688814
cites work: Proof Analysis in Deontic Logics
cites work: Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
cites work: Neighborhood semantics for modal logic
cites work: Efficient local reductions to basic modal logic
cites work: A structure-preserving clause form translation
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q3204443
description: scientific article; zbMATH DE number 7850752