合流模态逻辑的子句归结
Clausal Resolution for Modal Logics of Confluence
摘要：
我们提出了一个子句解析为基础的方法，正常的多模态逻辑的融合，其Kripke语义的基础上，其特征在于适当的教会-罗瑟属性的实例框架。在这里，我们限制注意八个家庭这样的逻辑。我们展示了如何正常的逻辑汇流的推理规则，可以系统地获得从参数化公理，这些系统。我们讨论的方法的可靠性，完整性和终止。特别地，完备性可以通过显示每个新添加的推理规则的结论确保框架上的相应条件成立来模块化地证明。为了说明该方法的使用，给出了一些例子。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
