: A Resolution-Based Prover for Multimodal K

DOI10.1007/978-3-319-40229-1_28zbMath1475.68444OpenAlexW2494487003MaRDI QIDQ2817940

Clare Dixon, Cláudia Nalon, Ullrich Hustadt

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_28

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Theorem proving using clausal resolution: from past to present ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ Efficient local reductions to basic modal logic ⋮ Local is best: efficient reductions to modal logic \textsf{K}

Uses Software

• OTTER
• VAMPIRE
• FaCT++
• Spartacus
• InKreSAT
• BDDTab

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A benchmark method for the propositional modal logics K, KT, S4
• 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 ★
• Using the Universal Modality: Gains and Questions
• 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

This page was built for publication:

A Resolution-Based Prover for Multimodal K