Clausal resolution for normal modal logics
From MaRDI portal
Publication:5429559
DOI10.1016/j.jalgor.2007.04.001zbMath1131.03007MaRDI QIDQ5429559
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
03B45: Modal logic (including the logic of norms)
03B35: Mechanization of proofs and logical operations
Related Items
Modal Logic S5 Satisfiability in Answer Set Programming, Towards resolution-based reasoning for connected logics, Proof complexity of modal resolution, Efficient local reductions to basic modal logic, Local is best: efficient reductions to modal logic \textsf{K}, Local reductions for the modal cube, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, Resolution with order and selection for hybrid logics, Theorem proving using clausal resolution: from past to present, : A Resolution-Based Prover for Multimodal K, Sub-propositional Fragments of the Interval Temporal Logic of Allen’s Relations, A Modal-Layered Resolution Calculus for K