结构归结的类型理论方法
A Type-Theoretic Approach to Structural Resolution
摘要：
结构解析（英语：Structural resolution）是一种新提出的SLD解析的替代方法，它允许系统地将派生分离为术语匹配和统一步骤。生产性逻辑程序是那些对任何查询的项匹配归约必须终止的程序。对于具有共归纳意义的生产性程序，有限项重写约简可以被看作是无限推导中的观测度量。以生产性方式处理上递归的能力是S-归结的一个有吸引力的计算特征。在本文中，我们的第一步，更好地理解的操作属性的S-分辨率相比，SLD分辨率。为此，我们提出了一个类型系统的SLD分辨率和S分辨率的分析。我们制定的S-分辨率和SLD-分辨率的减少系统，并显示其可靠性相对于类型系统。本文的核心方法之一是可实现性变换，它使逻辑程序具有生产性和非重叠性。我们表明，S-分辨率和SLD-分辨率是唯一等价的程序与这两个属性。
英文摘要：
Structural resolution (or S-resolution) is a newly proposed alternative to SLD-resolution that allows a systematic separation of derivations into term-matching and unification steps. Productive logic programs are those for which term-matching reduction on any query must terminate. For productive programs with coinductive meaning, finite term-rewriting reductions can be seen as measures of observation in an infinite derivation. Ability of handling corecursion in a productive way is an attractive computational feature of S-resolution. In this paper, we make first steps towards a better conceptual understanding of operational properties of S-resolution as compared to SLD-resolution. To this aim, we propose a type system for the analysis of both SLD-resolution and S-resolution. We formulate S-resolution and SLD-resolution as reduction systems, and show their soundness relative to the type system. One of the central methods of this paper is realizability transformation, which makes logic programs productive and non-overlapping. We show that S-resolution and SLD-resolution are only equivalent for programs with these two properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
