{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:02:40Z","timestamp":1771063360882,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T00:00:00Z","timestamp":1547078400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001832","name":"Radboud University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001832","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10472-018-9606-x","type":"journal-article","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T11:24:42Z","timestamp":1547119482000},"page":"213-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Proof-checking Euclid"],"prefix":"10.1007","volume":"85","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9259-1220","authenticated-orcid":false,"given":"Michael","family":"Beeson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,10]]},"reference":[{"key":"9606_CR1","doi-asserted-by":"publisher","first-page":"700","DOI":"10.1017\/S1755020309990098","volume":"2","author":"J Avigad","year":"2009","unstructured":"Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid\u2019s Elements. Rev. Symb. Log. 2, 700\u2013768 (2009)","journal-title":"Rev. Symb. Log."},{"key":"9606_CR2","doi-asserted-by":"publisher","first-page":"1199","DOI":"10.1016\/j.apal.2015.07.006","volume":"166","author":"M Beeson","year":"2015","unstructured":"Beeson, M.: A constructive version of Tarski\u2019s geometry. Ann. Pure Appl. Logic 166, 1199\u20131273 (2015)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9606_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/bsl.2015.41","volume":"22","author":"M Beeson","year":"2016","unstructured":"Beeson, M.: Constructive geometry and the parallel postulate. Bull. Symb. Log. 22, 1\u2013104 (2016)","journal-title":"Bull. Symb. Log."},{"key":"9606_CR4","volume-title":"Automated Theorem Proving: After 25 Years","author":"WW Bledsoe","year":"1983","unstructured":"Bledsoe, W. W., Loveland, D.: Automated Theorem Proving: After 25 Years. American Mathematical Society, Providence (1983)"},{"key":"9606_CR5","unstructured":"Boutry, P.: On the Formalization of Foundations of Geometry. PhD thesis, University of Strasbourg (2018)"},{"key":"9606_CR6","unstructured":"Boutry, P., Braun, G., Narboux, J.: From Tarski to Descartes: formalization of the arithmetization of Euclidean geometry. In: Davenport, J.H., Ghourabi, F. (eds.) SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, vol. 39 of EPiC Series in Computing, Tokyo, Japan, EasyChair, pp. 14\u201328 (2016)"},{"key":"9606_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.jsc.2018.04.007","volume":"90","author":"P Boutry","year":"2019","unstructured":"Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symb. Comput. 90, 149\u2013168 (2019). https:\/\/doi.org\/10.1016\/j.jsc.2018.04.007","journal-title":"J. Symb. Comput."},{"key":"9606_CR8","unstructured":"Boutry, P., Gries, C., Narboux, J., Schreck, P.: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. J. Autom. Reason., p. 68. https:\/\/link.springer.com\/article\/10.1007%2Fs10817-017-9422-8 (2017)"},{"key":"9606_CR9","unstructured":"Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: 11th International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, Strasbourg, France, p. 19 (2016)"},{"key":"9606_CR10","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry 2012 vol. 7993, Edinburgh, United Kingdom, Jacques Fleuriot, Springer, pp. 89\u2013109 (2012)","DOI":"10.1007\/978-3-642-40672-0_7"},{"key":"9606_CR11","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s10817-016-9374-4","volume":"58","author":"G Braun","year":"2017","unstructured":"Braun, G., Narboux, J.: A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry. J. Autom. Reason. 58, 23 (2017)","journal-title":"J. Autom. Reason."},{"key":"9606_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-4037-6","volume-title":"Mechanical Geometry Theorem Proving","author":"SC Chou","year":"1987","unstructured":"Chou, S. C.: Mechanical Geometry Theorem Proving. Kluwer Academic Publishers, Norwell (1987)"},{"key":"9606_CR13","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00244942","volume":"4","author":"SC Chou","year":"1988","unstructured":"Chou, S. C.: An introduction to Wu\u2019s method for mechanical theorem proving in geometry. J. Autom. Reason. 4, 237\u2013267 (1988)","journal-title":"J. Autom. Reason."},{"key":"9606_CR14","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. World Scientific (1994)","DOI":"10.1142\/2196"},{"key":"9606_CR15","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF02328448","volume":"2","author":"SC Chou","year":"1986","unstructured":"Chou, S. C., Schelter, W. F.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2, 253\u2013273 (1986)","journal-title":"J. Autom. Reason."},{"key":"9606_CR16","unstructured":"Corbineau, P.: A declarative language for the Coq proof assistant. In: Types for Proofs and Programs, vol. 4941 of LNCS, Springer (2008)"},{"key":"9606_CR17","unstructured":"Euclid: The Elements of Euclid, viz. the first six books, together with the eleventh and the twelfth, Nourse and Balfous, Edinburgh, 7th ed., 1787. Translated by Robert Simson. Available from Bibliotheque Nationale at http:\/\/gallica.bnf.fr\/ark:\/12148\/bpt6k1163221v"},{"key":"9606_CR18","volume-title":"The Thirteen Books of the Elements","author":"Euclid","year":"1956","unstructured":"Euclid: The Thirteen Books of the Elements. Dover, New York (1956). Three volumes. Includes commentary by the translator, Sir Thomas L. Heath"},{"key":"9606_CR19","unstructured":"Gelernter, H.: Realization of a geometry theorem-proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp 134\u2013152. McGraw-Hill, New York (1963)"},{"key":"9606_CR20","unstructured":"Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of a geometry-theorem proving machine. In: Feigenbaum, E., Feldman, J. (eds.) Computers and Thought, pp 153\u2013167. McGraw-Hill, New York (1963)"},{"key":"9606_CR21","volume-title":"Euclidean and non-Euclidean Geometries: Development and History","author":"MJ Greenberg","year":"2008","unstructured":"Greenberg, M. J.: Euclidean and non-Euclidean Geometries: Development and History, 4th edn. W. H. Freeman, New York (2008)","edition":"4th edn."},{"key":"9606_CR22","unstructured":"Gries, C.: Axiomes de continuit\u00e9 en g\u00e9om\u00e9trie neutre : Une \u00e9tude m\u00e9chanis\u00e9e en Coq. University of Strasbourg, internship report (2017)"},{"key":"9606_CR23","volume-title":"Contributions to the Axiomatic Foundations of Geometry","author":"HN Gupta","year":"1965","unstructured":"Gupta, H. N.: Contributions to the Axiomatic Foundations of Geometry. PhD Thesis, University of California, Berkeley (1965)"},{"key":"9606_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-22676-7","volume-title":"Geometry: Euclid and Beyond","author":"R Hartshorne","year":"2000","unstructured":"Hartshorne, R.: Geometry: Euclid and Beyond. Springer, New York (2000)"},{"key":"9606_CR25","unstructured":"Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois Second English edition, translated from the tenth German edition by Leo Unger. Original publication year (1899)"},{"key":"9606_CR26","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0004-3702(88)90050-1","volume":"37","author":"D Kapur","year":"1988","unstructured":"Kapur, D.: A refutational approach to geometry theorem proving. J. Artif. Intell. 37, 61\u201393 (1988)","journal-title":"J. Artif. Intell."},{"key":"9606_CR27","unstructured":"Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger\u2019s algorithm. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation (SYMSAC 86), Waterloo, 1986, B. Char, ed., pp. 209\u2013214 (1986)"},{"key":"9606_CR28","unstructured":"Manders, K.: The Euclidean diagram (1995). In: The Philosophy of Mathematical Practice, Paolo Mancosu. Oxford University Press ed. (2011)"},{"key":"9606_CR29","unstructured":"Miller, N.: A Diagrammatic Formal System for Euclidean Geometry. PhD thesis, Cornell University (2001)"},{"key":"9606_CR30","doi-asserted-by":"crossref","unstructured":"Miller, N.: Euclid and his twentieth century rivals: diagrams in the logic of Euclidean geometry. Studies in the theory and applications of diagrams, CSLI Publications, Stanford, Calif, 2007. OCLC: ocm71947628","DOI":"10.1007\/11783183_16"},{"key":"9606_CR31","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1215\/00294527-1626509","volume":"53","author":"N Miller","year":"2012","unstructured":"Miller, N.: On the inconsistency of Mumma\u2019s Eu. Notre Dame Journal of Formal Logic 53, 27\u201352 (2012)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"9606_CR32","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BF01449485","volume":"58","author":"J Mollerup","year":"1904","unstructured":"Mollerup, J.: Die Beweise der ebenen Geometrie ohne Benutzung der Gleichheit und Ungleichheit der Winkel. Math. Ann. 58, 479\u2013496 (1904)","journal-title":"Math. Ann."},{"key":"9606_CR33","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s11229-009-9509-9","volume":"175","author":"J Mumma","year":"2010","unstructured":"Mumma, J.: Proofs, pictures, and Euclid. Synthese 175, 255\u2013287 (2010)","journal-title":"Synthese"},{"key":"9606_CR34","unstructured":"Narboux, J., Jani\u010di\u0107, P., Fleuriot, J.: Computer-assisted theorem proving in synthetic geometry. In: Sitharam, M., John, A.S., Sidman, J. (eds.) Handbook of Geometric Constraint Systems Principles, Chapman and Hall\/CRC, ch. 2. in press (2018)"},{"key":"9606_CR35","volume-title":"Vorlesung \u00fcber Neuere Geometrie","author":"M Pasch","year":"1882","unstructured":"Pasch, M.: Vorlesung \u00fcber Neuere Geometrie. Teubner, Leipzig (1882)"},{"key":"9606_CR36","volume-title":"Principii de Geometria","author":"G Peano","year":"1889","unstructured":"Peano, G.: Principii de Geometria. Fratelli Bocca, Torino (1889)"},{"key":"9606_CR37","volume-title":"Euclid\u2019s Elements of Geometry [Books 1-6, 11,12] with Explanatory Notes; Together with a Selection of Geometrical Exercises. To which is Prefixed an Intr., Containing a Brief Outline of the History of Geometry","author":"R Potts","year":"1845","unstructured":"Potts, R.: Euclid\u2019s Elements of Geometry [Books 1-6, 11,12] with Explanatory Notes; Together with a Selection of Geometrical Exercises. To which is Prefixed an Intr., Containing a Brief Outline of the History of Geometry. Oxford University Press, Oxford (1845)"},{"key":"9606_CR38","doi-asserted-by":"crossref","DOI":"10.1515\/9780691214672","volume-title":"A Commentary on the First Book of Euclid","author":"Proclus","year":"1970","unstructured":"Proclus: A Commentary on the First Book of Euclid. Princeton University Press, Princeton (1970)"},{"key":"9606_CR39","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A Quaife","year":"1989","unstructured":"Quaife, A.: Automated development of Tarski\u2019s geometry. J. Autom. Reason. 5, 97\u2013118 (1989)","journal-title":"J. Autom. Reason."},{"key":"9606_CR40","doi-asserted-by":"crossref","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Teil II: Metamathematische Betrachtungen (Hochschultext). Springer\u2013Verlag, 1983. Reprinted 2011 by Ishi Press, with a new foreword by Michael Beeson","DOI":"10.1007\/978-3-642-69418-9"},{"key":"9606_CR41","first-page":"25","volume":"73","author":"S Stojanovic Durdevic","year":"2015","unstructured":"Stojanovic Durdevic, S., Narboux, J., Janicic, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski\u2019s geometry. Ann. Math. Artif. Intell. 73, 25 (2015)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9606_CR42","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF02018030","volume":"4","author":"J Strommer","year":"1973","unstructured":"Strommer, J.: \u00dcber die Kreisaxiome. Period. Math. Hung. 4, 3\u201316 (1973)","journal-title":"Period. Math. Hung."},{"key":"9606_CR43","doi-asserted-by":"publisher","first-page":"175","DOI":"10.2307\/421089","volume":"5","author":"A Tarski","year":"1999","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. Bull. Symb. Log. 5, 175\u2013214 (1999)","journal-title":"Bull. Symb. Log."},{"key":"9606_CR44","unstructured":"Veronese, G.: Fondamenti di geometria a pi\u00f9 dimensioni e a pi\u00f9 specie di unit\u00e0 rettilinee esposti in forma elementare. Lezioni per la scuola di magistero in matematica, Padova: Tipografia del Seminario, 1891 (1891)"},{"key":"9606_CR45","first-page":"reprinted in [4","volume":"21","author":"W-T Wu","year":"1978","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21, reprinted in [4] (1978)","journal-title":"Sci. Sinica"},{"key":"9606_CR46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6639-0","volume-title":"Mechanical Theorem Proving in Geometries: Basic Principles","author":"W-T Wu","year":"1994","unstructured":"Wu, W.-T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, Wien\/ New York (1994)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-018-9606-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-018-9606-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-018-9606-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,10]],"date-time":"2022-09-10T01:39:22Z","timestamp":1662773962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-018-9606-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,10]]},"references-count":46,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["9606"],"URL":"https:\/\/doi.org\/10.1007\/s10472-018-9606-x","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,10]]},"assertion":[{"value":"10 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}