A compact representation of proofs
A compact representation of proofs
复制标题
证明的紧凑表示
DOI：
--
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
D. Miller
中科院分区：
文献类型：
--
作者：
D. Miller
通过包含替换项来推广公式的结构用于表示经典逻辑中的证明。这些结构称为展开树，可以很容易地理解为描述定理的重言式替换实例。它们还提供了一个计算上有用的代表性的经典证明作为一流的价值。作为价值观，它们是紧凑的，可以很容易地操纵和转换。例如，我们提出了一个显式的转换之间的扩展树证明和无割顺序证明。使用扩展树表示证明的定理证明器可以使用这种转换以更易于阅读的形式呈现其证明。另外，对扩展树的一个非常简单的计算可以将它们转换为Craig风格的线性推理，并在它们存在时转换为插值。我们选择了简单类型论的一个子逻辑作为我们的经典逻辑，因为它通过类型化λ-演算优雅地表示了所有有限类型的替换。由于所有的证明理论的结果，我们将研究在很大程度上依赖于性质的替代，使用这种逻辑使我们能够加强和扩展以前的结果：我们能够证明加强形式的一阶插值定理，以及提供正确的描述Skolem功能和Herbrand宇宙。后者不是它们的一阶定义的直接推广。
A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which represents proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed λ-calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions.