{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:45:50Z","timestamp":1725482750947},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540666721"},{"type":"electronic","value":"9783540479970"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-47997-x_4","type":"book-chapter","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T10:14:18Z","timestamp":1175768058000},"page":"47-66","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Proving Newton\u2019s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle"],"prefix":"10.1007","author":[{"given":"Jacques D.","family":"Fleuriot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,11,17]]},"reference":[{"key":"4_CR1","volume-title":"Great Books of the Western World","author":"Apollonius.","year":"1939","unstructured":"Apollonius. Conics. Translation by R. Catesby Taliaferro. In Great Books of the Western World, Vol. 11, Chicago, Encyclopedia Britannica (1939) 51, 56, 59"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/0315-0860(89)90097-9","volume":"16","author":"J. B. Brackenridge","year":"1989","unstructured":"J. B. Brackenridge. Newton\u2019s mature dynamics and the Principia: A simplified solution to the Kepler Problem. Historia Mathematica 16(1989), 36\u201345. 55","journal-title":"Historia Mathematica"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"J. B. Brackenridge. The Key to Newton\u2019s Dynamics: The Kepler Problem and Newton\u2019s Principia. University of California Press, 1995. 55","DOI":"10.1525\/9780520916852"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005819428156","volume":"21","author":"H.-B. Li","year":"1998","unstructured":"H.-B. Li and M.-T. Cheng. Clifford algebraic reduction method for mechanical theorem proving in differential geometry. J. Automated Reasoning 21(1998), 1\u201321. 64","journal-title":"J. Automated Reasoning"},{"key":"4_CR5","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"S. C. Chou, X. S. Gao, and J. Z. Zhang. Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation. J. Automated Reasoning 17 (1996), 325\u2013347. 48","journal-title":"J. Automated Reasoning"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":". S. C. Chou","year":"1996","unstructured":". S. C. Chou, X. S. Gao, and J. Z. Zhang. Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. J. Automated Reasoning 17 (1996), 349\u2013370. 48","journal-title":"J. Automated Reasoning"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00881835","volume":"10","author":"S. C. Chou","year":"1993","unstructured":"S. C. Chou, X. S. Gao. Automated reasoning in differential geometry and mechanics: II. Mechanical theorem proving. J. Automated Reasoning 10 (1993), 173\u2013189. 64","journal-title":"J. Automated Reasoning"},{"key":"4_CR8","unstructured":"S. C. Chou, X. S. Gao. Automated reasoning in differential geometry and mechanics: III. Mechanical formula derivation. IFIP Transaction on Automated Reasoning 1\u201312, North-Holland, 1993. 64"},{"key":"4_CR9","volume-title":"Newton\u2019s Principia: The Central Argument","author":"D. Densmore","year":"1996","unstructured":"D. Densmore. Newton\u2019s Principia: The Central Argument. Green Lion Press, Santa Fe, New Mexico, 1996. 48"},{"key":"4_CR10","unstructured":"Euclid. Elements. Translation by Thomas L. Heath. Dover Publications Inc., 1956. 49, 58"},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-61732-9_60","volume-title":"Proceedings of the 3rd International Conference on Artificial Intelligence and Symbolic Mathematical Computation (Stey, Austria, September 1996)","author":"D. Wang","year":"1996","unstructured":"D. Wang. Geometry Machines: From AI to SMC. Proceedings of the 3rd International Conference on Artificial Intelligence and Symbolic Mathematical Computation (Stey, Austria, September 1996), LNCS 1138, 213\u2013239. 64"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"S. Fevre and D. Wang. Proving geometric theorems using Clifford algebra and rewrite rules. Proceedings of the 15th International Conference on Automated Deduction (CADE-15) (Lindau, Germany, July 5\u201310, 1998), LNAI 1421, 17\u201332. 64","DOI":"10.1007\/BFb0054242"},{"key":"4_CR13","unstructured":"J. D. Fleuriot and L. C. Paulson. A combination of nonstandard analysis and geometry theorem proving, with application to Newton\u2019s Principia. Proceedings of the 15th International Conference on Automated Deduction (CADE-15) (Lindau, Germany, July 5\u201310, 1998), LNAI 1421, 3\u201316. 47, 48, 49, 51, 52, 54, 55, 61, 64"},{"key":"4_CR14","unstructured":"I. Newton. The Mathematical Principles of Natural Philosophy. Third edition, 1726. Translation by A. Motte (1729). Revised by F. Cajory (1934). University of California Press. 47"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"D. T. Whiteside. The mathematical principles underlying Newton\u2019s Principia Mathematica. Glasgow University Publication 138, 1970. 52","DOI":"10.1177\/002182867000100203"},{"key":"4_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BFb0022723","volume-title":"Automated Deduction in Geometry","author":"D. Wang","year":"1997","unstructured":"D. Wang. Clifford algebraic calculus for geometric reasoning with application to computer vision. Automated Deduction in Geometry (D. Wang et al., Eds.), LNAI 1360, Springer-Verlag, Berlin Heidelberg, 1997, 115\u2013140. 64"},{"key":"4_CR17","first-page":"171","volume":"7","author":"W.-t. Wu","year":"1991","unstructured":"W.-t. Wu. Mechanical theorem proving of differential geometries and some of its applications in mechanics. J. Automated Reasoning 7 (1991), 171\u2013191. 64","journal-title":"J. Automated Reasoning"}],"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\/3-540-47997-X_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T09:47:25Z","timestamp":1683798445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47997-X_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666721","9783540479970"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-47997-x_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 November 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}