直觉主义逻辑中的聚焦与极性
计算机科学中的逻辑
2007-08-17 v1
摘要
聚焦证明系统为无切证明提供了一种范式，结构化地组织了可逆与不可逆推理规则的应用。Andreoli 针对线性逻辑提出的聚焦证明系统已被应用于计算的证明搜索和证明规范化方法。文献中的各种证明系统在不同程度上表现出聚焦特征。我们提出了一种新的直觉主义逻辑聚焦证明系统，称为 LJF，并展示了如何通过插入逻辑连接词来提前停止聚焦，从而将其他证明系统映射到新系统中。我们还利用 LJF 设计了一个经典逻辑的聚焦证明系统。我们对这些系统的设计与分析基于线性逻辑中聚焦的完备性，以及 Girard 的 LC 和 LU 证明系统中出现的极性概念。
引用
@article{arxiv.0708.2252,
title = {Focusing and Polarization in Intuitionistic Logic},
author = {Chuck Liang and Dale Miller},
journal= {arXiv preprint arXiv:0708.2252},
year = {2007}
}