• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >On the Specification of Sequent Systems
【24h】

On the Specification of Sequent Systems

机译：关于后续系统规范

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

摘要

Recently, linear Logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear logic can be used to draw conclusions about the specified sequent calculus. For example, derivability of one proof system from another can be decided by a simple procedure that is implemented via bounded logic programming-style search. Also, simple and decidable conditions on the linear logic presentation of inference rules, called homogeneous and coherence, can be used to infer that the initial rules can be restricted to atoms and that cuts can be eliminated. In the present paper we introduce Llinda, a logical framework based on linear logic augmented with inference rules for definition (fixed points) and induction. In this way, the above properties can be proved entirely inside the framework. To further illustrate the power of Llinda, we extend the definition of coherence and provide a new, semi-automated proof of cut-elimination for Girard's Logic of Unicity (LU).
机译：近来，线性逻辑已被用于指定后续演算证明系统，使得线性逻辑中的证明搜索可以在指定逻辑中产生证明搜索。此外，线性逻辑的元理论可用于得出有关指定顺序演算的结论。例如，一个证明系统与另一个证明系统的可导出性可以通过一个简单的过程来确定，该过程可以通过有界逻辑编程样式搜索来实现。同样，可以使用推断规则的线性逻辑表示的简单且可确定的条件（称为齐次和相干性）来推断初始规则可以限制在原子上，并且可以消除割伤。在本文中，我们介绍了Llinda，这是一个基于线性逻辑的逻辑框架，并添加了用于定义（定点）和归纳的推理规则。这样，可以完全在框架内部证明上述属性。为了进一步说明Llinda的功能，我们扩展了相干性的定义，并为吉拉德（Girard's Unicity）的逻辑（LU）提供了一种新的半自动化裁切证明。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号