A Type-Theoretic Approach to Structural Resolution

Abstract. Structural resolution (or S-resolution) is a newly proposed al-ternative to SLD-resolution that allows a systematic separation of deriva-tions into term-matching and unification steps. Productive logic pro-grams 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 under-standing 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 rela-tive 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