• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Flat modal fixpoint logics with the converse modality
【24h】

Flat modal fixpoint logics with the converse modality

机译：具有逆模态的平面模态定点逻辑

获取原文
获取原文并翻译 | 示例
       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, with the restriction that the fixpoint connectives involved must be disjunctive formulas. This extends earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the free algebras of flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau-based reasoning for modal fixpoint logics, and the use of networks, which is a well-known tool for proving completeness of modal logics.
机译：我们证明了与双向mu-演算的扁平片段相对应的一类模态定点逻辑的一般完整性结果，但所涉及的定点连接词必须是析取公式的限制。这扩展了Santocanale和Venema的早期工作。我们观察到Santocanale和Venema的证明，即平面固定点逻辑的自由代数中的最小固定点是构造性的（使用最终伴随），当引入逆模态时不再起作用。相反，我们的完整性证明使用归纳规则以类似于命题动态逻辑的标准完整性证明的方式，直接为一致性公式构建模型。该方法与焦点概念（以前已在基于表格的模态定点逻辑推理中使用焦点）和网络的使用相结合，后者是证明模态逻辑完整性的众所周知的工具。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号