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.
@cite_16 's (CoLP) extends SLD-resolution with a method to use atomic . That is, during the execution, if the current queries @math contain a query @math that unifies via @math with a @math in the earlier execution, then the next step of resolution will be given by @math . The coinductvie hyposesis mechanism in CoLP can be viewed as a form of loop detection. However, CoLP cannot detect hypotheses for more complex patterns of coinduction that produce coinductive subgoals that fail to unify. As discussed in introduction, it is not a suitable tool to analyze the productivity of infinite data structures in logic programming.
@cite_16
1963107927
Coinduction has recently been introduced as a powerful technique for reasoning about unfounded sets, unbounded structures, and interactive computations. Where induction corresponds to least fixed point semantics, coinduction corresponds to greatest fixed point semantics. In this paper we discuss the introduction of coinduction into logic programming. We discuss applications of coinductive logic programming to verification and model checking, lazy evaluation, concurrent logic programming and non-monotonic reasoning.