  We establish proof-theoretic, constructive and coalgebraic foundations for
proof search in coinductive Horn clause theories. Operational semantics of
coinductive Horn clause resolution is cast in terms of coinductive uniform
proofs; its constructive content is exposed via soundness relative to an
intuitionistic first-order logic with recursion controlled by the later
modality; and soundness of both proof systems is proven relative to a novel
coalgebraic description of complete Herbrand models.
