{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:41Z","timestamp":1749124061702,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054241","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia"],"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":[[2006,5,25]]},"reference":[{"issue":"No.3","key":"2_CR1","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1145\/322017.322018","volume":"24","author":"A. M. Ballantyne","year":"1977","unstructured":"A. M. Ballantyne and W. W. Bledsoe. Automatic Proofs of Theorems in Analysis Using Nonstandard Analysis. J. of the Association of Computing Machinery, Vol. 24, No. 3, July 1977, 353\u2013374.","journal-title":"J. of the Association of Computing Machinery"},{"key":"2_CR2","volume-title":"Liciendo en Mathematica con Mencion en Computation Thesis","author":"T. Bedrax","year":"1993","unstructured":"T. Bedrax. Infmal: Prototype of an Interactive Theorem Prover based on Infinitesimal Analysis. Liciendo en Mathematica con Mencion en Computation Thesis. Pontifica Universidad Catolica de Chile, Santiago, Chile, 1993."},{"key":"2_CR3","first-page":"288","volume-title":"The World of Mathematics, Vol. 1","author":"G. Berkeley","year":"1956","unstructured":"G. Berkeley. The Analyst: A Discourse Addressed to an Infidel Mathematician. The World of Mathematics, Vol. 1, London. Allen and Unwin, 1956, 288\u2013293."},{"key":"2_CR4","doi-asserted-by":"publisher","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\n                        17 (1996), 325\u2013347.","journal-title":"J. Automated Reasoning"},{"key":"2_CR5","doi-asserted-by":"crossref","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.","journal-title":"J. Automated Reasoning"},{"key":"2_CR6","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864126","volume-title":"Force and Geometry in Newton's Principia","author":"F. De Gandt","year":"1995","unstructured":"F. De Gandt. Force and Geometry in Newton's Principia. Princeton University Press, Princeton, New Jersey, 1995."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"D. Kapur. Geometry Theorem Proving using Hilbert's Nullstellensatz. Proceedings of SYMSAC'86, Waterloo, 1986, 202\u2013208.","DOI":"10.1145\/32439.32479"},{"key":"2_CR8","volume-title":"Foundations of Infinitesimal Calculus","author":"H. J. Keisler","year":"1976","unstructured":"H. J. Keisler. Foundations of Infinitesimal Calculus. Prindle, Weber & Schmidt, 20 Newbury Street, Boston, Massachusetts, 1976."},{"key":"2_CR9","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."},{"key":"2_CR10","unstructured":"S Novak Jr. Diagrams for Solving Physical Problems. Diagrammatic Reasoning: Cognitive and Computational Perspectives, AAAI Press\/MIT Press, 753\u2013774, 1995. (Eds. Janice Glasgow, N. Hari Narayana, and B. Chandrasekaram)."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.","DOI":"10.1007\/BFb0030541"},{"key":"2_CR12","unstructured":"A. Robinson. Non-Standard Analysis. North-Holland Publishing Company, 1980. 1966, first edition."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"R. Chuaqui and P. Suppes. Free-Variable Axiomatic Foundations of Infinitesimal Analysis: A Fragment with Finitary Consistency Proof. J. Symbolic Logic, Vol. 60, No. 1, March 1995.","DOI":"10.2307\/2275512"},{"key":"2_CR14","first-page":"213","volume":"1138","author":"D. Wang","year":"1996","unstructured":"D. Wang. Geometry Machines: From AI to SMC. 3rd Internationa Conference on Artificial Intelligence and Symbolic Mathematical Computation. (Stey, Austria, September 1996), LNCS 1138, 213\u2013239.","journal-title":"LNCS"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"D. T. Whiteside. The Mathematical Principles Underlying Newton's Principia Mathematica. Glasgow University Publication 138, 1970.","DOI":"10.1177\/002182867000100203"},{"key":"2_CR16","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1090\/conm\/029\/12","volume":"29","author":"W. Wu","year":"1984","unstructured":"W.-t. Wu. On the Decision Problem and the Mechanization of Theorem in Elementary Geometry. Automated Theorem Proving: After 25 years. A.M.S., Contemporary Mathematics, 29 (1984), 213\u2013234.","journal-title":"Contemporary Mathematics"},{"key":"2_CR17","first-page":"171","volume":"7","author":"W. Wu","year":"1991","unstructured":"W.-t. Wu. Mechanical Theorem Proving of Differential Geometries and Some of its Applications in Mechanics. J. Automated Reasoning\n                        7 (1991), 171\u2013191.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054241","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T20:12:09Z","timestamp":1675714329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054241"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0054241","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}