论一阶线性逻辑的证明搜索结构化
计算机科学中的逻辑
2022-07-01 v1
摘要
完整的一阶线性逻辑可以在 Miller 的 Forum 系统中表示为一种抽象逻辑编程语言，这在“证明搜索即计算”范式中产生了一种合理的操作解释。然而，Forum 仍然需要处理通常会被合理的操作语义所忽略的语法细节。在这方面，Forum 通过限制语言和推理规则的形式，改进了线性逻辑的 Gentzen 系统。我们通过限制允许的公式类，在一个我们称之为 G-Forum 的系统中进一步改进了 Forum，该系统仍等价于完整的一阶线性逻辑。G-Forum 中允许的唯一公式具有与 Forum 相继式相同的形状：这种限制并未削弱表达能力，并使 G-Forum 适用于证明论分析。G-Forum 由两个（大型）推理规则组成，我们为其展示了切消过程。这无需诉诸比 G-Forum 所提供的更细致的公式与相继式细节，从而成功检验了我们系统的内部对称性。
引用
@article{arxiv.cs/0312002,
title = {On Structuring Proof Search for First Order Linear Logic},
author = {Paola Bruscoli and Alessio Guglielmi},
journal= {arXiv preprint arXiv:cs/0312002},
year = {2022}
}
备注
Author website at http://alessio.guglielmi.name/res/