{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,3]],"date-time":"2026-01-03T14:42:17Z","timestamp":1767451337758},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_3","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"43-59","source":"Crossref","is-referenced-by-count":23,"title":["Without Loss of Generality"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Contemporary Mathematics","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1090\/conm\/029\/14","volume-title":"Automated Theorem Proving: After 25 Years","author":"S.-C. Chou","year":"1984","unstructured":"Chou, S.-C.: Proving elementary geometry theorems using Wu\u2019s algorithm. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics, vol.\u00a029, pp. 243\u2013286. American Mathematical Society, Providence (1984)"},{"key":"3_CR2","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"3_CR4","unstructured":"Hales, T.C.: Easy pieces in geometry (2007), http:\/\/www.math.pitt.edu\/~thales\/papers\/"},{"key":"3_CR5","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"T.C. Hales","year":"2007","unstructured":"Hales, T.C.: The Jordan curve theorem, formally and informally. The American Mathematical Monthly\u00a0114, 882\u2013894 (2007)","journal-title":"The American Mathematical Monthly"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"issue":"1892-3","key":"3_CR7","first-page":"460","volume":"2","author":"F. Klein","year":"1893","unstructured":"Klein, F.: Vergleichende Betrachtungen ber neuere geometrische Forschungen. Mathematische Annalen\u00a043, 63\u2013100 (1893); Based on the speech given on admission to the faculty of the Univerity of Erlang in 1872. English translation \u201cA comparative review of recent researches in geometry\u201d in Bulletin of the New York Mathematical Society 2, 460\u2013497 (1892-1893)","journal-title":"Mathematische Annalen\u00a043, 63\u2013100 ; Based on the speech given on admission to the faculty of the Univerity of Erlang in 1872"},{"key":"#cr-split#-3_CR8.1","unstructured":"Noether, E.: Invariante Variationsprobleme. Nachrichten von der K??niglichen Gesellschaft der Wissenschaften zu Gttingen: Mathematisch-physikalische Klasse, 235???257 (1918);"},{"key":"#cr-split#-3_CR8.2","doi-asserted-by":"crossref","unstructured":"English translation ???Invariant variation problems??? by M.A. Travel in ???Transport Theory and Statistical Physics???, 1, 183???207 (1971)","DOI":"10.1080\/00411457108231446"},{"key":"3_CR9","unstructured":"Solovay, R.M., Arthan, R., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482 (2009); submitted to Annals of Pure and Applied Logic, http:\/\/arxiv.org\/PS_cache\/arxiv\/pdf\/0904\/0904.3482v1.pdf"}],"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\/978-3-642-03359-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T02:48:21Z","timestamp":1558493301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}