Extending logic programming with coinduction

Traditional logic programming, with its minimal Herbrand model semantics, is useful for declaratively defining finite data structures and properties. A program in traditional logic programming defines a set of inference rules that can be used to automatically construct proofs of various logical statements. The fact that logic programming also has a goal directed, top-down operational semantics, means that these proofs can efficiently be constructed by executing the logical statement that is to be proved. However, since traditional logic programming's declarative semantics is given in terms of a least fixed-point, that is, since logic programming's semantics is inductive, it is impossible to directly reason about infinite objects and properties. In programming language terms, this means that the language cannot make use of infinite data structures and corecursion. The contribution of this dissertation is the extension of traditional logic programming with coinduction, by invoking the principle of duality on the declarative semantics of traditional logic programming and by developing an efficient top-down, goal-directed procedure based on the principle of coinduction, for deciding inclusion of a logical statement in the greatest fixed-point model. This gives rise to a new field of programming languages referred to by this author as co-logic programming.