• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computational logic in multi-agent systems >Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic
【24h】

Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic

机译：将线性时间时序逻辑嵌入到无限逻辑中：在消除多主体无限性认知线性时间时序逻辑中的应用

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

摘要

Linear-time temporal logic (LTL) is known as one of the most useful logics for verifying concurrent systems, and infinitary logic (IL) is known as an important logic for formalizing common knowledge reasoning. The research fields of both LTL and IL have independently been developed each other, and the relationship between them has not yet been discussed before. In this paper, the relationship between LTL and IL is clarified by showing an embedding of LTL into IL. This embedding shows that globally and eventually operators in LTL can respectively be represented by infinitary conjunction and infinitary disjunction in IL. The embedding is investigated by two ways: one is a syntactical way, which is based on Gentzen-type sequent calculi, and the other is a semantical way, which is based on Kripke semantics. The cut-elimination theorems for (some sequent calculi for) LTL, an infinitary linear-time temporal logic ILT_ω (I.e., an integration of LTL and IL), a multi-agent infinitary epistemic linear-time temporal logic IELT_ω and a multi-agent epistemic bounded linear-time temporal logic ELT_ι are obtained as applications of the resulting embedding theorem and its extensions and modifications. In particular, the cut-elimination theorem for IELT-ω gives a new proof-theoretical basis for extremely expressive time-dependent multi-agent logical systems with common knowledge reasoning.
机译：线性时间时序逻辑（LTL）是验证并发系统的最有用的逻辑之一，而无限逻辑（IL）是形式化常识推理的重要逻辑。 LTL和IL的研究领域是相互独立发展的，它们之间的关系尚未讨论过。在本文中，LTL与IL之间的关系通过显示LTL嵌入IL得以阐明。此嵌入表明LTL的全局运算符和最终运算符可以分别用IL中的不定式合取和不定式分离来表示。嵌入的方法有两种：一种是基于Gentzen类型后续演算的句法方法，另一种是基于Kripke语义的语义方法。 LTL的割除定理，不定式线性时间时序逻辑ILT_ω（即LTL和IL的积分），多主体不定式认知线性时间时序逻辑IELT_ω和多主体作为结果的嵌入定理及其扩展和修改的应用，获得了有界的有界线性时间逻辑逻辑ELT_1。尤其是，IELT-ω的割除定理为具有常识推理的极具表现力的时间相关多主体逻辑系统提供了新的证明理论基础。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号