\(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
From MaRDI portal
Publication:2303247
DOI10.1007/s10817-018-09503-xzbMath1468.68304OpenAlexW2945005331MaRDI QIDQ2303247
Ullrich Hustadt, Clare Dixon, Cláudia Nalon
Publication date: 3 March 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-09503-x
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (7)
CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT ⋮ Solving modal logic problems by translation to higher-order logic ⋮ On structures of regular standard contradictions in propositional logic ⋮ Theorem proving using clausal resolution: from past to present ⋮ Efficient local reductions to basic modal logic ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Prefixed tableaus and nested sequents
- A structure-preserving clause form translation
- Application of modal logic to programming
- Verifying concurrent processes using temporal logic
- A guide to completeness and complexity for modal logics of knowledge and belief
- An optimality result for clause form translation
- First-order modal logic
- A benchmark method for the propositional modal logics K, KT, S4
- : A Resolution-Based Prover for Multimodal K
- Implementing Tableau Calculi Using BDDs: BDDTab System Description
- A Modal-Layered Resolution Calculus for K
- Anti-prenexing and Prenexing for Modal Logics
- BDD-based decision procedures for the modal logic K ★
- Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
- Using the Universal Modality: Gains and Questions
- Labelled propositional modal logics: theory and practice
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- InKreSAT: Modal Reasoning via Incremental Reduction to SAT
- Clausal resolution for normal modal logics
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Clausal temporal resolution
This page was built for publication: \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
