摘要：解释计算是一种可应用于简单类型理论（也称为高阶逻辑）和集合论的一阶定理证明方法。当应用于某些类型理论的一阶表示时，它与高阶决议完全相同。本文比较了它在类型理论和集合论上的行为。
作者：Gilles Dowek
论文ID：2306.00498
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-02
PDF 下载： 英文版 中文版pdf翻译中