{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:10:07Z","timestamp":1747548607363,"version":"3.40.5"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1023\/a:1018940332714","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"99-138","source":"Crossref","is-referenced-by-count":4,"title":["Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts"],"prefix":"10.1007","volume":"29","author":[{"given":"L.A.","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I.","family":"Green","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"317325_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and A.D. Gordon, A calculus for cryptographic protocols: The Spi Calculus, in: Fourth ACM Conference on Computer and Communications Security (ACM Press, 1997) pp. 36\u201347. Full version available as Technical Report 414, University of Cambridge Computer Laboratory, January 1997.","DOI":"10.1145\/266420.266432"},{"key":"317325_CR2","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"S. Abramsky","year":"1990","unstructured":"S. Abramsky, The lazy lambda calculus, in: Research Topics in Functional Programming, ed. D. Turner (Addison-Wesley, Reading, MA, 1990) pp. 65\u2013117."},{"key":"317325_CR3","first-page":"295","volume-title":"11th Conference on Automated Deduction","author":"D. Basin","year":"1992","unstructured":"D. Basin and T.Walsh, Difference matching, in: 11th Conference on Automated Deduction, ed. D. Kapur, Lecture Notes in Artificial Intelligence, Vol. 607(Springer, Berlin, 1992) pp. 295\u2013309."},{"issue":"1\u20132","key":"317325_CR4","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"D. Basin and T. Walsh, A calculus for and termination of rippling, J. Autom. Reason. 16(1\u20132) (1996) pp. 147\u2013180.","journal-title":"J. Autom. Reason."},{"key":"317325_CR5","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"14th Conference on Automated Deduction","author":"C. Benzm\u00fcller","year":"1997","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, A.Meier, E. Melis, W. Schaarschmidt, J. Siekmann and V. Sorge, \u03a9mega, Towards a mathematical assistant, in: 14th Conference on Automated Deduction, ed. W. McCune, Lecture Notes in Artificial Intelligence, Vol. 1249(Springer, Berlin, 1997) pp. 252\u2013255."},{"key":"317325_CR6","doi-asserted-by":"crossref","unstructured":"R. Boulton, K. Slind, A. Bundy and M. Gordon, An interface between CLAM and HOL, in: Proceedingsof the 11th International Conference on Theorem Proving in Higher Order Logics, eds. J. Grundy and M. Newey, Lecture Notes in Computer Science, Vol. 1479(Springer, Berlin) pp. 87\u2013104.","DOI":"10.1007\/BFb0055131"},{"key":"317325_CR7","doi-asserted-by":"crossref","unstructured":"A. Bundy, The use of explicit plans to guide inductive proofs, in: 9th Conference on Automated Deduction, eds. R. Lusk and R. Overbeek (1988) pp. 111\u2013120. Longer version available from Edinburgh as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"317325_CR8","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland and A. Smaill, Rippling: A heuristic for guiding inductive proofs, Artif. Intell. 62(1993) 185\u2013253. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artif. Intell."},{"key":"317325_CR9","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"A. Bundy, F. van Harmelen, C. Horn and A. Smaill, The Oyster-Clam system, in: 10th International Conference on Automated Deduction, ed. M.E. Stickel, Lecture Notes in Artificial Intelligence, Vol. 449(Springer, Berlin, 1990) pp. 647\u2013648. Also available from Edinburgh as DAI Research Paper 507."},{"key":"317325_CR10","unstructured":"A. Bundy, A. Smaill and J. Hesketh, Turning eureka steps into calculations in automatic program synthesis, in: Proceedings of UK IT 90, ed. S.L.H. Clarke (1990) pp. 221\u2013226. Also available from Edinburgh as DAI Research Paper 448."},{"key":"317325_CR11","first-page":"100","volume-title":"Proceedings of the 2nd International Workshop of Conditional and Typed Rewriting Systems","author":"H. Chen","year":"1990","unstructured":"H. Chen, J. Hsiang and H.-C. Kong, On finite representations of infinite sequences of terms, in: Proceedings of the 2nd International Workshop of Conditional and Typed Rewriting Systems, ed. M. Okada, Lecture Notes in Computer Science, Vol. 516(Springer, Berlin, 1990) pp. 100\u2013114."},{"key":"317325_CR12","volume-title":"Proceedings of the Workshop on Automated Verification Methods for Finite-State Systems","author":"R. Cleaveland","year":"1989","unstructured":"R. Cleaveland, J. Parrow and B. Steffen, The ConcurrencyWorkbench: A semantics-based verification tool for finite-state systems, in: Proceedings of the Workshop on Automated Verification Methods for Finite-State Systems, Lecture Notes in Computer Science, Vol. 407(Springer, Berlin, 1989). Also available from Edinburgh, as ECS-LFCS-89-83."},{"key":"317325_CR13","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BFb0105400","volume-title":"9th International Conference of Theorem Proving in Higher Order Logics","author":"G. Collins","year":"1996","unstructured":"G. Collins, A proof tool for reasoning about functional programs. in: 9th International Conference of Theorem Proving in Higher Order Logics, eds. J. von Wright, J. Grundy and J. Harrison, Lecture Notes in Computer Science, Vol. 1125(Springer, Berlin, 1996) pp. 109\u2013124."},{"key":"317325_CR14","first-page":"276","volume-title":"14th Conference on Automated Deduction","author":"L. Dennis","year":"1996","unstructured":"L. Dennis, A. Bundy and I. Green, Using a generalisation critic to find bisimulations for coinductive proofs, in: 14th Conference on Automated Deduction, ed.W. McCune, Lecture Notes in Artificial Intelligence, Vol. 1249(Springer, Berlin, 1996) pp. 276\u2013290."},{"key":"317325_CR15","unstructured":"L. Dennis, Proof planning coinduction, unpublished Ph.D. thesis, Edinburgh University (1998)."},{"key":"317325_CR16","doi-asserted-by":"crossref","unstructured":"M. Fiore, A coinduction principle for recursive data types based on bisimulation, in: Proceedings of the Eight IEEE Symposium on Logic in Computer Science (1993) pp. 110\u2013119.","DOI":"10.1109\/LICS.1993.287595"},{"key":"317325_CR17","first-page":"356","volume-title":"5th Conference on Automated Deduction","author":"J. Goguen","year":"1980","unstructured":"J. Goguen, How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation, in: 5th Conference on Automated Deduction, eds.W. Bibel and R. Kowalski, Lecture Notes in Computer Science, Vol. 87(Springer, Berlin, 1980) pp. 356\u2013373."},{"key":"317325_CR18","doi-asserted-by":"crossref","unstructured":"J. Goguen, K. Lin and G. Rosu, Circular Coinductive Rewriting, in: Proceedings, Automated Software Engineering (ASE)'00 (2000) o appear.","DOI":"10.1109\/ASE.2000.873657"},{"key":"317325_CR19","doi-asserted-by":"crossref","unstructured":"A.D. Gordon, Bisimilarity as a theory of functional programming, in: Proceedings of 11th Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Computer Science, Vol. 1(Elsevier, 1995).","DOI":"10.1016\/S1571-0661(04)80013-6"},{"key":"317325_CR20","doi-asserted-by":"crossref","unstructured":"A.D. Gordon, Bisimilarity for a first-order calculus of objects with subtyping, in: Proceedings, 23rd Symposium on Principles of Programming Languages (ACM SIGPLAN-SIGACT, 1996) pp. 386\u2013395.","DOI":"10.1145\/237721.237807"},{"key":"317325_CR21","volume-title":"Proceedings FoSSaCS'98","author":"A.D. Gordon","year":"1998","unstructured":"A.D. Gordon and L. Cardelli, Mobile ambients, in: Proceedings FoSSaCS'98, Lecture Notes in Computer Science, Vol. 1578(Springer, Berlin, 1998). Full version to appear in Theor. Comput. Sci."},{"key":"317325_CR22","doi-asserted-by":"crossref","unstructured":"P. Hudak, S. Peyton\u2013Jones, P.Wadler et al., Report on the functional programming language Haskell: A non-strict, purely functional language version 1.2, ACM SIGPLAN Notices 27(5) (1992).","DOI":"10.1145\/130697.130699"},{"key":"317325_CR23","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"A. Ireland and A. Bundy, Productive use of failure in inductive proof, J. Autom. Reason. 16(1\u20132) (1996) 79\u2013111. Also available as DAI Research Paper No. 716, Department of Artificial Intelligence, Edinburgh.","journal-title":"J. Autom. Reason."},{"key":"317325_CR24","first-page":"222","volume":"2","author":"B. Jacobs","year":"1997","unstructured":"B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bull. 2(1997) 222\u2013259.","journal-title":"EATCS Bull."},{"key":"317325_CR25","unstructured":"D. Park, Fixpoint induction and proofs of program properties, in: Machine Intelligence, Vol. 5, eds. D. Michie and B. Meltzer (1970) pp. 59\u201378."},{"key":"317325_CR26","unstructured":"L.C. Paulson, Co-induction and co-recursion in higher-order logic, Technical Report 304, University of Cambridge, Computer Laboratory (1993)."},{"key":"317325_CR27","volume-title":"The Implementation of Functional Programming Languages","author":"S.L. Peyton Jones","year":"1987","unstructured":"S.L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall, Englewood Cliffs, NJ, 1987)."},{"key":"317325_CR28","first-page":"138","volume-title":"Proc. of Second IEEE Int'l Symp. on Logic Programming","author":"U.S. Reddy","year":"1985","unstructured":"U.S. Reddy, Narrowing as the Operational Semantics of Functional Languages, in: Proc. of Second IEEE Int'l Symp. on Logic Programming (IEEE, New York, 1985) pp. 138\u2013151."},{"key":"317325_CR29","first-page":"25","volume":"89","author":"H.G. Rice","year":"1953","unstructured":"H.G. Rice, Classes of recursively enumerable sets and their decision problems, Trans. Amer. Math. Soc. 89(1953) 25\u201359.","journal-title":"Trans. Amer. Math. Soc."},{"key":"317325_CR30","unstructured":"G. Ro\u015fu and J. Goguen, Circular Coinduction, UCSD Technical Report CSE2000-064 (1999)."},{"key":"317325_CR31","volume-title":"Technical Report CS-R9652","author":"J. Rutten","year":"1996","unstructured":"J. Rutten, Universal coalgebra: A theory of systems, Technical Report CS-R9652, CWI, Amsterdam (1996)."},{"key":"317325_CR32","volume-title":"Circuit Design in Ruby","author":"M. Sheeran","year":"1990","unstructured":"M. Sheeran and G. Jones, Circuit Design in Ruby (North-Holland, Amsterdam, 1990)."},{"key":"317325_CR33","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math. 5(1955) 285\u2013309.","journal-title":"Pacific J. Math."},{"key":"317325_CR34","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1613\/jair.275","volume":"4","author":"T. Walsh","year":"1996","unstructured":"T. Walsh, A divergence critic for inductive proof, J. Artif. Intell. Res. 4(1996) 209\u2013235.","journal-title":"J. Artif. Intell. Res."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018940332714.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018940332714\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018940332714.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:38:49Z","timestamp":1747546729000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018940332714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":34,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["317325"],"URL":"https:\/\/doi.org\/10.1023\/a:1018940332714","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}