直观逻辑中的聚焦与极化
摘要：一种聚焦证明系统为无剪裁证明提供了一个正常形式，以结构化可逆和非可逆推理规则的应用。Andreoli的线性逻辑的聚焦证明系统已应用于证明搜索和证明规范化方法的计算。文献中的各种证明系统都具有不同程度的聚焦特性。我们提出了一种新的、针对直觉主义逻辑的聚焦证明系统，称为LJF，并展示了如何通过插入过早停止聚焦的逻辑连接词将其他证明系统映射到新系统中。我们还使用LJF设计了一个用于经典逻辑的聚焦证明系统。我们设计和分析这些系统的方法基于线性逻辑的聚焦完备性和在Girard的LC和LU证明系统中出现的极性概念。
作者：Chuck Liang, Dale Miller (INRIA Futurs)
论文ID：0708.2252
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-08-17