• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Cyclic Involutive Distributive Full Lambek Calculus is Decidable
【24h】

Cyclic Involutive Distributive Full Lambek Calculus is Decidable

机译：循环渐开分布Lambek微积分是可决定的

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

摘要

We prove the decidability of the extension CylnDFL of DFL (Distributive Full Lambek Calculus), in which the involutive law is derivable under the assumption of cyclicity. So far, the decidability of this logic has been an open problem (Galatos et al.. 2007, Residuated Lattices: An Algebraic Glimpse at Subslructural Logics, Elsevier). We present a Gentzen-slyle consecution calculus which is complete with respect to the class of cyclic involutive distributive full Lambek algebras (CylnDFL). It is an extension of the system DFL introduced by the author (2009, Stud. Log., 91, 201-216). We prove the cut elimination theorem for this system, and give a procedure of building a finite proof-search tree for any consecution.
机译：我们证明了DFL（分布式完全Lambek演算）的扩展CylnDFL的可判定性，其中对合定律是在周期性假设下可导出的。到目前为止，这种逻辑的可判定性一直是一个悬而未决的问题（Galatos等人，2007年，《剩余格：残基逻辑中的代数瞥见》，爱思唯尔）。我们提出了关于循环渐开分布全兰贝克代数（CylnDFL）的类的Gentzen-slyle连续演算。它是作者介绍的系统DFL的扩展（2009，Stud。Log。，91，201-216）。我们证明了该系统的割消除定理，并给出了用于构建任何证明的有限证明搜索树的过程。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号