{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:20:33Z","timestamp":1725488433315},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"},{"type":"electronic","value":"9783540447559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_14","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"185-200","source":"Crossref","is-referenced-by-count":4,"title":["Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain"],"prefix":"10.1007","author":[{"given":"Louise A.","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"issue":"1\u20132","key":"14_CR2","doi-asserted-by":"publisher","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\u20132):147\u2013180, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR3","unstructured":"R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, 1988. Perspectives in Computing, Vol 23."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th International 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":"14_CR5","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. Artificial Intelligence, 62:185\u2013253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"Artificial Intelligence"},{"key":"14_CR6","unstructured":"Alan Bundy. The automation of proof by mathematical induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier., 1998. Forthcoming."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAAP\u201996, Coll. on Trees in Algebra and Programming","author":"A. Cichon","year":"1996","unstructured":"A. Cichon and H. Touzet. An ordinal calculus for proving termination in term rewriting. In Proceedings of CAAP\u201996, Coll. on Trees in Algebra and Programming, number 1059 in Lecture Notes in Computer Science. Springer, 1996."},{"key":"14_CR8","unstructured":"Th. Coquand. Une Th\u00e9orie des Constructions. PhD thesis, University of Paris VII, 1985."},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Herbert B. Enderton. Elements of Set Theory. Academic Press, 1977.","DOI":"10.1016\/S0049-237X(08)71114-5"},{"issue":"11","key":"14_CR10","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"9","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: an interactive mathematical proof system. Journal of Automated Reasoning, 9(11):213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"A. Felty. A logic programming approach to implementing higher-order term rewriting. In L-H Eriksson et al., editors, Second International Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 135\u201361. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0013606"},{"key":"14_CR12","unstructured":"Lego group. Lego home page. http:\/\/www.dcs.ed.ac.uk\/home\/lego\/ ."},{"key":"14_CR13","volume-title":"Naive Set Theory","author":"P. Halmos","year":"1960","unstructured":"P. Halmos. Naive Set Theory. Van Nostrand, Princeton, NJ, 1960."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"A. G. Hamilton. Numbers, sets and axioms: the apparatus of mathematics. Cambridge University Press, 1982.","DOI":"10.1017\/CBO9781139171618"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming, Madrid, Spain, 1991.","DOI":"10.1007\/3-540-54233-7_155"},{"key":"14_CR16","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: An integrated approach to specification and verification. Tech report, SRI International, 1992."},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"L.C. Paulson. Set theory for verification: II. induction and recursion. Journal of Automated Reasoning, 15:353\u2013389, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"L.C. Paulson and K. Grabczewski. Mechanizing set theory: cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, pages 291\u2013323, 1996.","DOI":"10.1007\/BF00283132"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"J.D.C Richardson, A. Smaill, and Ian Green. System description: proof planning in higher-order logic with LambdaCLAM. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, editors, 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Artificial Intelligence, pages 129\u2013133, Lindau, Germany, July 1998.","DOI":"10.1007\/BFb0054254"},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A. Smaill","year":"1996","unstructured":"Alan Smaill and Ian Green. Higher-order annotated terms for proof search. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996, volume 1275 of Lecture Notes in Computer Science, pages 399\u2013414, Turku, Finland, 1996. Springer-Verlag. Also available as DAI Research Paper 799."},{"key":"14_CR21","volume-title":"Axiomatic Set Theory","author":"P. Suppes","year":"1960","unstructured":"P. Suppes. Axiomatic Set Theory. Van Nostrand, Princeton, NJ, 1960."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:10:52Z","timestamp":1556748652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}