Operational Semantics of Resolution and Productivity in Horn Clause Logic

TL;DR

This paper analyzes various resolution strategies in Horn clause logic using abstract reduction systems and type-theoretic semantics, providing a comparative framework and establishing their properties and equivalences.

Contribution

It introduces a uniform abstract reduction system framework for different resolution strategies and relates them to System H for a comprehensive semantic analysis.

Findings

Proves soundness of the reduction systems relative to System H.

Shows completeness of SLD-resolution and structural resolution.

Identifies conditions for operational equivalence between structural and SLD-resolution.

Abstract

This paper presents a study of operational and type-theoretic properties of different resolution strategies in Horn clause logic. We distinguish four different kinds of resolution: resolution by unification (SLD-resolution), resolution by term-matching, the recently introduced structural resolution, and partial (or lazy) resolution. We express them all uniformly as abstract reduction systems, which allows us to undertake a thorough comparative analysis of their properties. To match this small-step semantics, we propose to take Howard's System H as a type-theoretic semantic counterpart. Using System H, we interpret Horn formulas as types, and a derivation for a given formula as the proof term inhabiting the type given by the formula. We prove soundness of these abstract reduction systems relative to System H, and we show completeness of SLD-resolution and structural resolution relative to System H. We identify conditions under which structural resolution is operationally equivalent to SLD-resolution. We show correspondence between term-matching resolution for Horn clause programs without existential variables and term rewriting.