{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T18:40:55Z","timestamp":1649184055385},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425250","type":"print"},{"value":"9783540447559","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_5","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"43-58","source":"Crossref","is-referenced-by-count":3,"title":["An Irrational Construction of \u211d from \u2124"],"prefix":"10.1007","author":[{"given":"Rob D.","family":"Arthan","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"5_CR1","unstructured":"R.D. Arthan. A Report on ICL HOL. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Philip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications. IEEE Computer Society Press, 1992."},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BF01187947","volume":"63","author":"F.A. Behrend","year":"1956","unstructured":"F.A. Behrend. A Contribution to the Theory of Magnitudes and the Foundations of Analysis. Mathematische Zeitschrift, 63:345\u2013362, 1956.","journal-title":"Mathematische Zeitschrift"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"John H. Conway. On Numbers and Games. A.K. Peters Ltd., Second edition, 2001.","DOI":"10.1201\/9781439864159"},{"key":"5_CR4","unstructured":"B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990."},{"key":"5_CR5","unstructured":"H.-D. Ebbinghaus, H. Hermes, F. Hirzebruch, M. Koecher, K. Mainzer, J. Neukirch, A. Prestel, and R. Remmert. Numbers. Springer-Verlag, 1990."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"F. Faltin, N. Metropolis, B. Ross, and G.-C. Rota. The Real Numbers as a Wreath Product. Advances in Mathematics, 16, 1975.","DOI":"10.1016\/0001-8708(75)90115-2"},{"key":"5_CR7","unstructured":"Michael J.C. Gordon and Tom F. Melham, editors. Introduction to HOL. Cambridge University Press, 1993."},{"key":"5_CR8","unstructured":"John Harrison. Theorem Proving with the Real Numbers. Technical report, University of Cambridge Computer Laboratory, 1996."},{"key":"5_CR9","unstructured":"O. H\u00f6lder. Die Axiome der Quantit\u00e4t und die Lehre vom Mass. Ber. Verh. Kon. Sch. Ges. Wiss., pages 1\u201364, 1901."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"R.B. Jones. Methods and Tools for the Verification of Critical Properties. In R. Shaw, editor, 5th Refinement Workshop, Workshops in Computing. Springer-Verlag\/BCS-FACS, 1992.","DOI":"10.1007\/978-1-4471-3550-0_6"},{"key":"5_CR11","unstructured":"E. Kamke. Mengenlehre. Berlin, 1928. Reprinted by Dover in an English translation by F. Bagemihl as Theory of Sets. 1950."},{"key":"5_CR12","unstructured":"D.J. King and R.D. Arthan. Development of Practical Verification Tools. Ingenuity \u2014 the ICL Technical Journal, 1996."},{"key":"5_CR13","unstructured":"Saunders MacLane and Garrett Birkhoff. Algebra. AMS Chelsea Publishing, Third edition, 1999."},{"key":"5_CR14","unstructured":"Walter Rudin. Principles of Mathematical Analysis. McGraw-Hill Book Company, 1974."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"C. T. Sennett. Demonstrating the Compliance of Ada Programs with Z Specifications. In R. Shaw, editor, 5th Refinement Workshop, Workshops in Computing. Springer-Verlag\/BCS-FACS, 1992.","DOI":"10.1007\/978-1-4471-3550-0_5"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:10:36Z","timestamp":1556748636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":15,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-44755-5_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2001]]}}}