In this paper, we develop uniform proofs à la Miller and Nadathur for coinductive predicates in 8 different logics that vary in expressive power. Such proofs allow algorithmic proof search, as the application of proof rules is deterministic for each connective. We show that these uniform proofs are sound relative to an intuitionistic first-order logic with recursion that was proposed here. Moreover, we show that both proof systems are sound with respect to complete Herbrand models. This proof is presented in a modern, coalgebraic style. Finally, we provide heuristics for the discovery of proof goals, which is necessary to answer certain queries that arise from Horn clause programming. Such a discovery is necessary, as the original query can often not be proven directly but needs to be strengthened first.