Focusing and polarization in linear, intuitionistic, and classical logics
Focusing and polarization in linear, intuitionistic, and classical logics
复制标题
DOI：
10.1016/j.tcs.2009.07.041
复制
发表时间：
2009-11-01
影响因子：
1.1
通讯作者：
Miller, Dale
中科院分区：
文献类型：
--
作者：
Liang, Chuck;Miller, Dale
聚焦证明系统提供了一个范式，以削减自由证明，其中可逆和不可逆的推理规则的应用结构。在线性逻辑中，Andreoli的集中证明系统为无割证明提供了一个优雅而全面的范式。在直觉主义和经典逻辑中，文献中有各种不同的证明系统表现出聚焦行为。这些集中的证明系统已被应用于证明搜索和证明归一化方法的计算。我们提出了一个新的，集中的证明系统的直觉逻辑，称为LJF，并显示如何其他直觉证明系统可以映射到新的系统通过插入逻辑连接，过早地停止聚焦。我们还利用LJF设计了一个经典逻辑的集中证明系统LKF。我们的方法来设计和分析这些系统是基于完整性的重点在线性逻辑和极性的概念，出现在吉拉德的LC和LU证明系统。(C)2009爱思唯尔有限公司版权所有。
A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems. (C) 2009 Elsevier B.V. All rights reserved.