A proof-theoretic approach to coinduction in Horn clause logic

Abstract

The thesis is on coinduction in Horn clauses. Specifically, it considers productive corecursion, and presents a framework called Coinductive Uniform Proof as a principled approach to coinduction in first-order Horn clause logic. It addresses the challenges of 1) discovering sufficient conditions for logic programs to be productive, 2) providing an explanation of why unification (without occur-check) between goals in a SLD derivation can be exploited to capture productive corecursion, and 3) identifying the principle that unifies the diverse approaches to Horn clause coinduction which are scattered across the literature. The thesis advances the state of the art by 1) providing a sufficient condition for productive corecursion which requires that a logic program does not admit perpetual term-rewriting steps nor existential variables, 2) showing that the goal-unification technique can be used to capture productive corecursion if a goal is no less general than some previous goal to which it unifies, and 3) defining a coinductively sound proof construction method for Horn clauses where a Horn clause to be proved is first asserted as an assumption and then used for its own proof.