{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:08Z","timestamp":1749124088561},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_66","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:05:42Z","timestamp":1330279542000},"page":"200-213","source":"Crossref","is-referenced-by-count":18,"title":["Inductive definitions: Automation and application"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/BF01459088","volume":"99","author":"W. Ackermann","year":"1928","unstructured":"Wilhelm Ackermann. Zum Hilbertschen Aufbau der reellen Zahlen. Mathematische Annalen, 99:118\u2013133, 1928. English translation, \u2018On Hilbert's construction of the real numbers', in [24], pp. 493\u2013507.","journal-title":"Mathematische Annalen"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Peter Aczel. An introduction to inductive definitions. In J. Barwise and H.J. Keisler, editors, Handbook of mathematical logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739\u2013782. North-Holland, 1991.","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"14_CR3","volume-title":"BRICS Report Series RS-94-44","author":"S. Agerholm","year":"1994","unstructured":"Sten Agerholm. A HOL basis for reasoning about functional programs. BRICS Report Series RS-94-44, Centre of the Danish National Research Foundation, Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark, 1994."},{"key":"14_CR4","first-page":"367","volume-title":"Recursive boolean functions in HOL","author":"F. Andersen","year":"1991","unstructured":"Flemming Andersen and Kim Dam Petersen. Recursive boolean functions in HOL. In Archer et al. [5], pages 367\u2013377."},{"volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","year":"1991","key":"14_CR5","unstructured":"Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors. Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA, 1991. IEEE Computer Society Press."},{"key":"14_CR6","volume-title":"Technical Report 265","author":"J. Camilleri","year":"1992","unstructured":"Juanito Camilleri and Tom Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1992."},{"volume-title":"volume A-20 of IFIP Transactions A: Computer Science and Technology","year":"1992","key":"14_CR7","unstructured":"Luc J. M. Claesen and Michael J. C. Gordon, editors. Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, 1992. North-Holland."},{"key":"14_CR8","unstructured":"J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Raymond T. Yeh, editor, Current Trends in Programming Methodologies, volume IV, pages 80\u2013149. Prentice-Hall, 1978."},{"key":"14_CR9","first-page":"561","volume-title":"volume A-20 of IFIP Transactions A: Computer Science and Technology","author":"E. L. Gunter","year":"1992","unstructured":"Elsa L. Gunter. Why we can't have SML style datatype declarations in HOL. In Claesen and Gordon [7], pages 561\u2013568."},{"key":"14_CR10","first-page":"141","volume-title":"volume 780 of Lecture Notes in Computer Science","author":"E. L. Gunter","year":"1993","unstructured":"Elsa L. Gunter. A broader class of trees for recursive type definitions for HOL. In Joyce and Seger [13], pages 141\u2013154."},{"key":"14_CR11","unstructured":"John Harrison and Konrad Slind. A reference version of HOL. Presented in poster session of 1994 HOL Users Meeting and only published in participants' supplementary proceedings. Available on the Web from http:\/\/www.dcs.glasgow.ac.uk\/\u223chug94\/sproc.html, 1994."},{"key":"14_CR12","unstructured":"Nathan Jacobson. Basic Algebra I. W. H. Freeman, 2nd edition, 1989."},{"volume-title":"volume 780 of Lecture Notes in Computer Science","year":"1993","key":"14_CR13","unstructured":"Jeffrey J. Joyce and Carl Seger, editors. Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, 1993. Springer-Verlag."},{"key":"14_CR14","first-page":"133","volume":"6","author":"B. Knaster","year":"1927","unstructured":"B. Knaster. Un th\u00e9or\u00e8me sur les fonctions, d'ensembles. Annales de la Soci\u00e9t\u00e9 Polonaise de Math\u00e9matique, 6:133\u2013134, 1927. Volume published in 1928.","journal-title":"Annales de la Soci\u00e9t\u00e9 Polonaise de Math\u00e9matique"},{"key":"14_CR15","unstructured":"Tim Leonard. The HOL numeral library. Distributed with HOL system, 1993."},{"key":"14_CR16","first-page":"350","volume-title":"A package for inductive relation definitions in HOL","author":"T. F. Melham","year":"1991","unstructured":"Thomas F. Melham. A package for inductive relation definitions in HOL. In Archer et al. [5], pages 350\u2013357."},{"key":"14_CR17","first-page":"3","volume-title":"volume A-20 of IFIP Transactions A: Computer Science and Technology","author":"T. F. Melham","year":"1992","unstructured":"Thomas F. Melham. The HOL logic extended with quantification over type variables. In Claesen and Gordon [7], pages 3\u201318."},{"key":"14_CR18","volume-title":"Technical Report 320","author":"L. C. Paulson","year":"1993","unstructured":"Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. Technical Report 320, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1993."},{"key":"14_CR19","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/BF01472200","volume":"111","author":"R. P\u00e9ter","year":"1935","unstructured":"R. P\u00e9ter. Konstruktion nichtrekursiver Funktionen. Mathematische Annalen, 111:42\u201360, 1935.","journal-title":"Mathematische Annalen"},{"key":"14_CR20","first-page":"358","volume-title":"Defining recursive functions in HOL","author":"W. Ploegaerts","year":"1991","unstructured":"Wim Ploegaerts, Luc Claesen, and Hugo De Man. Defining recursive functions in HOL. In Archer et al. [5], pages 358\u2013366."},{"key":"14_CR21","first-page":"129","volume-title":"volume 780 of Lecture Notes in Computer Science","author":"R. E. O. Roxas","year":"1993","unstructured":"Rachel E. O. Roxas. A HOL package for reasoning about relations defined by mutual induction. In Joyce and Seger [13], pages 129\u2013140."},{"key":"14_CR22","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285\u2013309, 1955.","journal-title":"Pacific Journal of Mathematics"},{"key":"14_CR23","first-page":"117","volume-title":"volume A-20 of IFIP Transactions A: Computer Science and Technology","author":"M. Voort van der","year":"1992","unstructured":"Mark van der Voort. Introducing well-founded function definitions in HOL. In Claesen and Gordon [7], pages 117\u2013132."},{"key":"14_CR24","unstructured":"Jean van Heijenoort, editor. From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879\u20131931. Harvard University Press, 1967."},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Glynn Winskel. The formal semantics of programming languages: an introduction. Foundations of computing. MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_66.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:35:36Z","timestamp":1619573736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_66"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_66","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}