Clausal resolution for normal modal logics

DOI10.1016/j.jalgor.2007.04.001zbMath1131.03007OpenAlexW2016570675MaRDI QIDQ5429559

Clare Dixon, Cláudia Nalon

Publication date: 30 November 2007

Published in: Journal of Algorithms (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jalgor.2007.04.001

zbMATH Keywords

resolutionautomated deductionnormal modal logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items (12)

Towards resolution-based reasoning for connected logics ⋮ Proof complexity of modal resolution ⋮ A Modal-Layered Resolution Calculus for K ⋮ Sub-propositional Fragments of the Interval Temporal Logic of Allen’s Relations ⋮ Resolution with order and selection for hybrid logics ⋮ 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 ⋮ : A Resolution-Based Prover for Multimodal K ⋮ Efficient local reductions to basic modal logic ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube ⋮ Modal Logic S5 Satisfiability in Answer Set Programming

This page was built for publication: Clausal resolution for normal modal logics