{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:10:15Z","timestamp":1743127815956,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642250699"},{"type":"electronic","value":"9783642250705"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25070-5_11","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T20:30:55Z","timestamp":1320784255000},"page":"182-200","source":"Crossref","is-referenced-by-count":6,"title":["An Investigation of Hilbert\u2019s Implicit Reasoning through Proof Discovery in Idle-Time"],"prefix":"10.1007","author":[{"given":"Phil","family":"Scott","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/BF02844894","volume":"36","author":"G. Birkhoff","year":"1987","unstructured":"Birkhoff, G., Bennett, M.: Hilbert\u2019s Grundlagen der Geometrie. Rendiconti del Circolo Matematico di Palermo\u00a036, 343\u2013389 (1987)","journal-title":"Rendiconti del Circolo Matematico di Palermo"},{"key":"11_CR2","unstructured":"Boulton, R.: Efficiency in a Fully-Expansive Theorem Prover. Ph.D. thesis. Cambridge University (1993)"},{"key":"11_CR3","unstructured":"Boyer, C.B.: A History of Mathematics. John Wiley & Sons (1991)"},{"key":"11_CR4","unstructured":"de Bruijn, N.G.: The Mathematical Vernacular, a language for Mathematics with typed sets. In: Dybjer, P., et al. (eds.) Proceedings from the Workshop on Programming Logic, vol.\u00a037 (1987)"},{"key":"11_CR5","unstructured":"Euclid: Elements (1998), \n                  \n                    http:\/\/aleph0.clarku.edu\/~djoyce\/java\/elements\/elements.html"},{"key":"11_CR6","unstructured":"Hales, T.: Introduction to the Flyspeck Project, \n                  \n                    http:\/\/drops.dagstuhl.de\/opus\/newlinevolltexte\/2006\/432\/pdf\/05021.HalesThomas.Paper.432.pdf"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: a Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"11_CR8","unstructured":"Heath, T.L.: Euclid: The Thirteen Books of The Elements, vol.\u00a01. Dover Publications (1956)"},{"key":"11_CR9","unstructured":"Hilbert, D.: Foundations of Geometry. Open Court Classics, 10th edn. (1971)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues\u2019 theorem in Coq using ranks. In: Symposium on Applied Computing, pp. 1110\u20131115 (2009)","DOI":"10.1145\/1529282.1529527"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/10930755_21","volume-title":"Theorem Proving in Higher Order Logics","author":"L.I. Meikle","year":"2003","unstructured":"Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003)"},{"key":"11_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry","author":"L.I. Meikle","year":"2006","unstructured":"Meikle, L.I., Fleuriot, J.D.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"issue":"1522","key":"11_CR14","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1098\/rsta.1984.0067","volume":"312","author":"R. Milner","year":"1984","unstructured":"Milner, R., Bird, R.S.: The Use of Machines to Assist in Rigorous Proof [and Discussion]. Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences\u00a0312(1522), 411\u2013422 (1984)","journal-title":"Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1090\/S0002-9947-1902-1500592-8","volume":"3","author":"E.H. Moore","year":"1902","unstructured":"Moore, E.H.: On the projective axioms of geometry. Transactions of the American Mathematical Society\u00a03, 142\u2013158 (1902)","journal-title":"Transactions of the American Mathematical Society"},{"key":"11_CR16","unstructured":"Scott, P.: Mechanising Hilbert\u2019s Foundations of Geometry in Isabelle. Master\u2019s thesis. University of Edinburgh (2008)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-22863-6_28","volume-title":"Interactive Theorem Proving","author":"P. Scott","year":"2011","unstructured":"Scott, P., Fleuriot, J.: Composable Discovery Engines for Interactive Theorem Proving. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 370\u2013375. Springer, Heidelberg (2011)"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1090\/S0002-9904-1944-08178-0","volume":"50","author":"H. Weyl","year":"1944","unstructured":"Weyl, H.: David Hilbert and his mathematical work. Bulletin of the American Mathematical Society\u00a050, 635 (1944)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44755-5_26","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Wiedijk","year":"2001","unstructured":"Wiedijk, F.: Mizar Light for HOL Light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 378\u2013394. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25070-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:30:21Z","timestamp":1558297821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25070-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250699","9783642250705"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25070-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}