Clausal resolution for modal logics of confluence

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

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

Publication date: 26 September 2014

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

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.

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

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

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)

Cited In (3)

• Title not available (Why is that?)
• Clausal presentation of theories in deduction modulo
• Resolution calculi for non-normal 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)