{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:17:30Z","timestamp":1725455850194},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627173"},{"type":"electronic","value":"9783540684909"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027288","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T07:00:45Z","timestamp":1132383645000},"page":"135-147","source":"Crossref","is-referenced-by-count":1,"title":["Using the rippling heuristic in set membership proofs"],"prefix":"10.1007","author":[{"given":"Ina","family":"Kraan","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"9_CR1","first-page":"295","volume-title":"Difference matching","author":"D. Basin","year":"1992","unstructured":"D. Basin and T. Walsh. Difference matching. In Deepak Kapur, editor, 11th Conference on Automated Deduction, pages 295\u2013309, Saratoga Springs, NY, USA, June 1992. Published as Springer Lecture Notes in Artificial Intelligence, No 607."},{"key":"9_CR2","unstructured":"D. Basin and T. Walsh. Difference unification. In Proceedings of the 13th IJCAI. International Joint Conference on Artificial Intelligence, 1993. Also available as Technical Report MPI-I-92-247, Max-Planck-Institut f\u00fcr Informatik."},{"issue":"1\/2","key":"9_CR3","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"David Basin and Toby Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1\/2):147\u2013180, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR4","volume-title":"Technical Monograph PRG-107","author":"S. M. Brien","year":"1992","unstructured":"S. M. Brien and J. E. Nicholls. Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK, November 1992. Accepted for ISO standardization, ISO\/IEC JTC1\/SC22."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111\u2013120. Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349.","DOI":"10.1007\/BFb0012826"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"9_CR7","doi-asserted-by":"crossref","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. Artificial Intelligence, 62:185\u2013253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"I. Kraan and P. Baumann. Implementing Z in Isabelle. In J.P. Bowen and M.G. Hinchey, editors, Proceedings of ZUM'95: The Z Formal Specification Notation, Lecture Notes in Computer Science 967, pages 355\u2013373. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60271-2_130"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"I. Kraan and P. Baumann. Logical frameworks as a basis for verification tools: A case study. In Proceedings of the Tenth Knowledge-Based Software Engineering Conference, 1995.","DOI":"10.1109\/KBSE.1995.490117"},{"key":"9_CR10","unstructured":"S. Negrete-Yankelevich. Proof Planning with Logic Presentations. Unpublished PhD thesis, Department of Artificial Inte lligence, University of Edinburgh, 1996."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"B.L. Richards, I. Kraan, A. Smaill, and G.A. Wiggins. Mollusc: a general proof development shell for sequent-based logics. In A. Bundy, editor, 12th Conference on Automated Deduction, pages 826\u201330. Springer-Verlag, 1994. Lecture Notes in Artificial Intelligence, vol 814; Also available from Edinburgh as DAI Research paper 723.","DOI":"10.1007\/3-540-58156-1_69"},{"key":"9_CR12","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice Hall International, 2nd edition, 1992."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"T. Walsh, A. Nunes, and A. Bundy. The use of proof plans to sum series. In D. Kapur, editor, 11th Conference on Automated Deduction, pages 325\u2013339. Springer Verlag, 1992. Lecture Notes in Computer Science No. 607. Also available from Edinburgh as DAI Research Paper 563.","DOI":"10.1007\/3-540-55602-8_175"},{"key":"9_CR14","volume-title":"Technical Report TBA","author":"T. Yoshida","year":"1994","unstructured":"Tetsuya Yoshida, Alan Bundy, Ian Green, Toby Walsh, and David Basin. Coloured rippling: An extension of a theorem proving heuristic. Technical Report TBA, Dept. of Artificial Intelligence, Edinburgh, 1994."}],"container-title":["Lecture Notes in Computer Science","ZUM '97: The Z Formal Specification Notation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027288","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T01:31:13Z","timestamp":1586568673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027288"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627173","9783540684909"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0027288","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}