{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:28:51Z","timestamp":1759638531736},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,10,7]],"date-time":"2006-10-07T00:00:00Z","timestamp":1160179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,2]]},"DOI":"10.1007\/s10817-006-9036-z","type":"journal-article","created":{"date-parts":[[2006,10,6]],"date-time":"2006-10-06T12:33:50Z","timestamp":1160138030000},"page":"311-344","source":"Crossref","is-referenced-by-count":5,"title":["Mathematical Induction in Otter-Lambda"],"prefix":"10.1007","volume":"36","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,10,7]]},"reference":[{"key":"9036_CR1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P. Andrews","year":"1996","unstructured":"Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem proving system for classical type theory. J. Autom. Reason. 16, 321\u2013353 (1996)","journal-title":"J. Autom. Reason."},{"key":"9036_CR2","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(79)90034-3","volume":"9","author":"R. Aubin","year":"1979","unstructured":"Aubin, R.: Mechanizing structural induction, Part I: Formal system. Theor. Comput. Sci. 9, 329\u2013345 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"9036_CR3","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/0304-3975(79)90035-5","volume":"9","author":"R. Aubin","year":"1979","unstructured":"Aubin, R.: Mechanizing structural induction, Part II: Strategies. Theor. Comput. Sci. 9, 347\u2013362 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"9036_CR4","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Lambda logic. In: Basin, D., Rusinowitch, M. (eds.) Proceedings of Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4\u20138, 2004, vol. 3097 of Lecture Notes in Artificial Intelligence, pp. 460\u2013474. Springer (2004)","DOI":"10.1007\/978-3-540-25984-8_34"},{"key":"9036_CR5","unstructured":"Beeson, M.: Implicit typing in lambda logic. Presented at the ESHOL Workshop at LPAR-12 and available at the Otter-lambda website [7]. (Dec. 2005)"},{"key":"9036_CR6","unstructured":"Beeson, M.: MathXpert calculus assistant, software available from (and described at) www.HelpWithMath.com"},{"key":"9036_CR7","unstructured":"Beeson, M.: The Otter- $\\lambda$ website: http:\/\/www.MichaelBeeson.com\/research\/Otter-lambda\/index.php"},{"key":"9036_CR8","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, JS.: A Computational Logic Handbook. Academic, Boston (1988)"},{"key":"9036_CR9","unstructured":"Bundy, A.: The Automation of Proof by Mathematical Induction, Chapter 13 of [13]."},{"key":"9036_CR10","doi-asserted-by":"crossref","unstructured":"Bundy, A., Van Harnelen, F., Horn, C., Smaill, A.: The Oyster\u2013Clam system. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, vol. 449 of Lecture Notes in Artificial Intelligence, pp. 647\u2013648. Springer (1990)","DOI":"10.1007\/3-540-52885-7_123"},{"issue":"2","key":"9036_CR11","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Zhang, H.: An overview of Rewrite Rule Laboratory (RRL). J. Comput. Math. Appl. 29(2), 91\u2013114 (1995)","journal-title":"J. Comput. Math. Appl."},{"key":"9036_CR12","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"10th International Conference on Automated Deduction","author":"W. McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, pp. 663\u2013664. Springer, Berlin\/Heidelberg (1990)"},{"key":"9036_CR13","volume-title":"Handbook of Automated Reasoning, vol. II","author":"A. Robinson","year":"2001","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. II. Elsevier Science B.V., Amsterdam (2001). Co-published in the U.S. and Canada by MIT Press, Cambridge, Massachusetts"},{"issue":"2","key":"9036_CR14","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/BF00243005","volume":"5","author":"C. Wick","year":"1989","unstructured":"Wick, C., McCune, W.: Automated reasoning about elementary point-set topology. J. Autom. Reason. 5(2), 239\u2013255 (1989)","journal-title":"J. Autom. Reason."},{"key":"9036_CR15","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing","author":"L. Wos","year":"1999","unstructured":"Wos, L., Pieper, G.: A Fascinating Country in the World of Computing. World Scientific, Singapore (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9036-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9036-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9036-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:46Z","timestamp":1559265706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9036-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,7]]},"references-count":15,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,1,2]]}},"alternative-id":["9036"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9036-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,7]]}}}