Dennis, L. A., Bundy, A., & Green, I. (2000). The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction. Annals of Mathematics and Artificial Intelligence, 29(1-4),