Clausal resolution for modal logics of confluence

DOI10.1007/978-3-319-08587-6_24zbMATH Open1425.03008OpenAlexW2095984791MaRDI QIDQ3192202FDOQ3192202

Authors Cláudia Nalon, João Marcos, Clare Dixon 

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.0293

zbMATH Keywords

normal modal logicsresolution methodcombined logics

Mathematics Subject Classification ID

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

Abstract: We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method.

Recommendations

• Clausal resolution for normal modal logics
• Resolution-based methods for modal logics
• Modal resolution in clausal form
• Modal Resolution
• scientific article; zbMATH DE number 3932427

Cited in

(5)

• Clausal presentation of theories in deduction modulo
• scientific article; zbMATH DE number 1418334 (Why is no real title available?)
• Clausal resolution for normal modal logics
• Resolution calculi for non-normal modal logics
• On the influence of confluence in modal logics

This page was built for publication: Clausal resolution for modal logics of confluence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192202)