通用判断和归纳逻辑的削减
摘要：逻辑$LG^omega$的消去证明 抽象判断的编码的一个证明系统扩展，逻辑$FOLDNb$，其中包含归纳原则。逻辑$LG^omega$和$FOLDNb$一样，扩展了一阶直觉逻辑，添加了不动点和“通用量词”$\nabla$来推理在逻辑中编码的对象系统中的绑定动态。之前试图以归纳原则扩展$FOLDNb$的尝试未能成功模拟归纳规范中的一些绑定行为。通过在$\nabla$上放松一些限制，特别是添加公理$B\equiv\nabla x.B$，其中$x$在$B$中不自由出现，我们解决了这个问题。我们展示了通过采用等变性原则，扩展逻辑的表达可以大大简化。本文包含了cite{tiu07entcs}中所述结果的技术证明；鼓励读者咨询cite{tiu07entcs}以了解$LG^omega$的动机和示例。
作者：Alwen Tiu
论文ID：0801.3065
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-01-22