Resolution calculi for non-normal modal logics
From MaRDI portal
Publication:6541160
DOI10.1007/978-3-031-43513-3_18MaRDI QIDQ6541160FDOQ6541160
Authors: Dirk Pattinson, N. Olivetti, Cláudia Nalon 
Publication date: 17 May 2024
Cites Work
- InKreSAT: modal reasoning via incremental reduction to SAT
- A structure-preserving clause form translation
- Title not available (Why is that?)
- Clausal resolution for normal modal logics
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Title not available (Why is that?)
- The intractability of resolution
- Neighborhood semantics for modal logic
- Title not available (Why is that?)
- Resolution-based methods for modal logics
- Modal resolution in clausal form
- SAT-based decision procedures for classical modal logics
- The recursive resolution method for modal logic
- Title not available (Why is that?)
- Destructive Modal Resolution
- Clausal resolution for modal logics of confluence
- Sequent calculi and decision procedures for weak modal systems
- Modular sequent calculi for classical modal logics
- Admissibility of cut in congruent modal logics
- Sequent calculi for monotonic modal logics
- Modularisation of sequent calculi for normal and non-normal modalities
- Modal Resolution
- Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi
- A simple deduction method for modal logic
- Linear strategy for propositional modal resolution
- Semantics-Based Translation Methods for Modal Logics
- Resolution for some first-order modal systems
- Proof analysis in deontic logics
- 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
- \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
- Local reductions for the modal cube
- CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
- Implementing Superposition in iProver (System Description)
- Implementing tableau calculi using BDDs: BDDTab system description
- Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
- Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity
- Title not available (Why is that?)
- Title not available (Why is that?)
This page was built for publication: Resolution calculi for non-normal modal logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6541160)
