We investigate the systematic development of refined tableau systems for a subset of the logics of confluence, which are modal logics comprising of instances of the Scott-Lemmon axioms. In particular, we look at rule refinements aiming to decrease branching, perform fewer inferences and reduce the application of rules which create new labels in the tableau. Propagation rules are common forms of refined rules, that construct smaller pre-models sufficient to determine satisfiability, without needing to construct full concrete models satisfying the correspondence properties which would require a lot more inference steps. These rules have already been developed for the confluence logics that are part of the modal logic cube, but are lacking for some instances outside the cube. Such instances can be awkward, as the nature of their correspondence properties makes the development of propagation rules particularly challenging. These are the logics KG0111, KG and KDe for which we propose refined tableau systems. We also present refined tableau systems for the combined logics Kalt1De, KBG0111 and KDDe. Soundness and completeness results for all the systems are established.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Refined Tableau Systems for Some Modal Logics of Confluence

  • Kiana Samadpour Motalebi,
  • Renate A. Schmidt,
  • Cláudia Nalon

摘要

We investigate the systematic development of refined tableau systems for a subset of the logics of confluence, which are modal logics comprising of instances of the Scott-Lemmon axioms. In particular, we look at rule refinements aiming to decrease branching, perform fewer inferences and reduce the application of rules which create new labels in the tableau. Propagation rules are common forms of refined rules, that construct smaller pre-models sufficient to determine satisfiability, without needing to construct full concrete models satisfying the correspondence properties which would require a lot more inference steps. These rules have already been developed for the confluence logics that are part of the modal logic cube, but are lacking for some instances outside the cube. Such instances can be awkward, as the nature of their correspondence properties makes the development of propagation rules particularly challenging. These are the logics KG0111, KG and KDe for which we propose refined tableau systems. We also present refined tableau systems for the combined logics Kalt1De, KBG0111 and KDDe. Soundness and completeness results for all the systems are established.