Coinduction is a powerful definition, programming and reasoning method that can be applied in a variety of situations, such as automata theory, reactive systems, modal logic, potentially infinite data, non-terminating computations etc. Typically, coinduction is understood as the fact that bisimilarity implies equality in the denotational semantics. However, coinduction can be extended to other predicates and relations on state-based systems, thereby providing for general coinductive programming and reasoning techniques.

I will present in this talk foundations for recursive proof search in coinductive Horn clause specifications, aka coinductive logic programs. Such specifications have a wide range of applications: coinductive programming, type class resolution, type checking and more. Because of applications like type class resolution, we will focus on constructive methods for proof search. In particular, we will discuss a first-order intuitionistic sequent calculus with recursion for coinductive predicates, a system of coinductive uniform proofs that will enable proof search, and we will study the relation of these proof system to each other and to complete Herbrand models.