{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:02:52Z","timestamp":1771063372421,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642250699","type":"print"},{"value":"9783642250705","type":"electronic"}],"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_2","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T20:30:55Z","timestamp":1320784255000},"page":"34-50","source":"Crossref","is-referenced-by-count":2,"title":["Exploring the Foundations of Discrete Analytical Geometry in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Fleuriot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"10","key":"2_CR1","doi-asserted-by":"publisher","first-page":"2220","DOI":"10.1016\/j.patcog.2008.12.005","volume":"42","author":"A. Chollet","year":"2009","unstructured":"Chollet, A., Wallet, G., Fuchs, L., Largeteau-Skapin, G., Andres, E.: Insight in discrete geometry and computational content of a discrete model of the continuum. Pattern Recognition\u00a042(10), 2220\u20132228 (2009)","journal-title":"Pattern Recognition"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-12712-0_3","volume-title":"Computational Modeling of Objects Represented in Images","author":"A. Chollet","year":"2010","unstructured":"Chollet, A., Wallet, G., Andres, E., Fuchs, L., Largeteau-Skapin, G., Richard, A.: \u03a9-Arithmetization of Ellipses. In: Barneva, R.P., Brimkov, V.E., Hauptman, H.A., Natal Jorge, R.M., Tavares, J.M.R.S. (eds.) CompIMAGE 2010. LNCS, vol.\u00a06026, pp. 24\u201335. Springer, Heidelberg (2010)"},{"key":"2_CR3","unstructured":"Collected Work of L. Euler, vol. 11 (1913), vol. 12 (1914)"},{"key":"2_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BFb0054241","volume-title":"Automated Deduction - CADE-15","author":"J.D. Fleuriot","year":"1998","unstructured":"Fleuriot, J.D., Paulson, L.C.: A Combination of Nonstandard Analysis and Geometry Theorem Proving, With Application to Newton\u2019s Principia. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 3\u201316. Springer, Heidelberg (1998)"},{"key":"2_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-47997-X_4","volume-title":"Automated Deduction in Geometry","author":"J.D. Fleuriot","year":"1999","unstructured":"Fleuriot, J.D., Paulson, L.C.: Proving Newton\u2019s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. In: Wang, D., Yang, L., Gao, X.-S. (eds.) ADG 1998. LNCS (LNAI), vol.\u00a01669, pp. 47\u201366. Springer, Heidelberg (1999)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-44659-1_10","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Fleuriot","year":"2000","unstructured":"Fleuriot, J.: On the Mechanization of Real Analysis in Isabelle\/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 145\u2013161. Springer, Heidelberg (2000)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Fleuriot, J.: Theorem Proving in Infinitesimal Geometry. Logic Journal of the IGPL\u00a09(3) (2001)","DOI":"10.1093\/jigpal\/9.3.447"},{"key":"2_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-85729-329-9","volume-title":"A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton\u2019s Principia","author":"J. Fleuriot","year":"2001","unstructured":"Fleuriot, J.: A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton\u2019s Principia. Springer, Heidelberg (2001)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-79126-3_4","volume-title":"Discrete Geometry for Computer Imagery","author":"L. Fuchs","year":"2008","unstructured":"Fuchs, L., Largeteau-Skapin, G., Wallet, G., Andres, E., Chollet, A.: A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis. In: Coeurjolly, D., Sivignon, I., Tougne, L., Dupont, F. (eds.) DGCI 2008. LNCS, vol.\u00a04992, pp. 21\u201332. Springer, Heidelberg (2008)"},{"key":"2_CR10","unstructured":"Harthong, J.: Une th\u00e9orie du Continu. La Math\u00e9Matique Non Standard. Editions du CNRS, 307\u2013329 (1989)"},{"key":"2_CR11","unstructured":"Magaud, N., Chollet, A., Fuchs, L.: Formalizing a Discrete Model of the Continuum in Coq From a Discrete Geometry Perspective. In: Proceedings of the Automated Deduction in Geometry Workshop, Munich (2010)"},{"issue":"6","key":"2_CR12","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1090\/S0002-9904-1977-14398-X","volume":"83","author":"E. Nelson","year":"1977","unstructured":"Nelson, E.: Internal set theory: A new approach to nonstandard analysis. Bulletin of the American Mathematical Society\u00a083(6), 1165\u20131198 (1977)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"2_CR13","volume-title":"Isabelle - A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle - A Generic Theorem Prover. Springer, Heidelberg (1994)"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BF02127796","volume":"16","author":"J.-P. Reveill\u00e8s","year":"1996","unstructured":"Reveill\u00e8s, J.-P., Richard, D.: Back and Forth Between Continuous and Discrete For The Working Computer Scientist. Annals of Mathematics and Artifical Intelligence\u00a016, 89\u2013152 (1996)","journal-title":"Annals of Mathematics and Artifical Intelligence"},{"key":"2_CR15","unstructured":"Robinson, A.: Non-standard analysis. North-Holland (1966)"},{"key":"2_CR16","first-page":"517","volume":"9","author":"G. Wallet","year":"2008","unstructured":"Wallet, G.: Integer Calculus on the Harthong-Reeb Line. Revue Arima\u00a0(9), 517\u2013536 (2008)","journal-title":"Revue Arima"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:30:09Z","timestamp":1558297809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25070-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250699","9783642250705"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25070-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}