{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:03:01Z","timestamp":1777424581529,"version":"3.51.4"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,4,29]],"date-time":"2016-04-29T00:00:00Z","timestamp":1461888000000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s10817-016-9374-4","type":"journal-article","created":{"date-parts":[[2016,4,29]],"date-time":"2016-04-29T10:17:25Z","timestamp":1461925045000},"page":"209-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["A Synthetic Proof of Pappus\u2019 Theorem in Tarski\u2019s Geometry"],"prefix":"10.1007","volume":"58","author":[{"given":"Gabriel","family":"Braun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,29]]},"reference":[{"key":"9374_CR1","unstructured":"Boutry, P., Braun, G., Narboux, J.: From Tarski to Descartes: formalization of the arithmetization of euclidean geometry. In: The 7th International Symposium on Symbolic Computation in Software (SCSS 2016), EasyChair Proceedings in Computing, p.\u00a015. Tokyo, Japan (2016)"},{"key":"9374_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Proof and computation in geometry. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012), Volume 7993 of Springer Lecture Notes in Artificial Intelligence, pp. 1\u201330. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-40672-0_1"},{"issue":"11","key":"9374_CR3","doi-asserted-by":"crossref","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. Log. 166(11), 1199\u20131273 (2015)","journal-title":"Ann. Pure Appl. Log."},{"key":"9374_CR4","volume-title":"Fundamentals of Mathematics: Geometry","author":"H Behnke","year":"1974","unstructured":"Behnke, H., Gould, S.H.: Fundamentals of Mathematics: Geometry. MIT Press, New York (1974)"},{"issue":"1","key":"9374_CR5","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s10817-007-9086-x","volume":"40","author":"M Bezem","year":"2008","unstructured":"Bezem, M., Hendriks, D.: On the mechanization of the proof of Hessenberg\u2019s theorem in coherent logic. J. Autom. Reason. 40(1), 61\u201385 (2008)","journal-title":"J. Autom. Reason."},{"key":"9374_CR6","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Post-Proceedings of Automated Deduction in Geometry 2012, Volume 7993 of LNCS, pp. 89\u2013109. Springer, Edinburgh (2012)","DOI":"10.1007\/978-3-642-40672-0_7"},{"key":"9374_CR7","unstructured":"Boutry, P., Narboux, J., Schreck, P.: A Reflexive Tactic for Automated Generation of Proofs of Incidence to an Affine Variety. October (2015)"},{"key":"9374_CR8","unstructured":"Boutry, P., Narboux, J., Schreck, P.: Parallel Postulates and Decidability of Intersection of Lines: A Mechanized Study Within Tarski\u2019s System of Geometry. Submitted, July (2015)"},{"key":"9374_CR9","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: Ashort note about case distinctions in Tarski\u2019s geometry. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry 2014, Proceedings of ADG 2014, pp. 1\u201315. Coimbra, Portugal (2014)"},{"key":"9374_CR10","unstructured":"Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility andreadability of formal proofs in geometry. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry2014, Proceedings of ADG 2014, pp. 1\u201319. Coimbra, Portugal (2014)"},{"key":"9374_CR11","unstructured":"Cast\u00e9ran, P.: Coq + $$\\epsilon $$ \u03f5 ? In: JFLA, pp. 1\u201315 (2007)"},{"key":"9374_CR12","doi-asserted-by":"crossref","unstructured":"Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert\u2019s elementary geometry. In: Automated Deduction in Geometry (2000)","DOI":"10.1007\/3-540-45410-1_17"},{"key":"9374_CR13","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Post-Proceedings of Automated Deduction in Geometry (ADG 2008), Number 6701 in Lecture Notes in Artificial Intelligence (2011)","DOI":"10.1007\/978-3-642-21046-4_3"},{"key":"9374_CR14","unstructured":"Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois, 1960. Second English edition, translated from the tenth German edition by Leo Unger. Original publication date (1899)"},{"issue":"4","key":"9374_CR15","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/s10817-010-9209-7","volume":"48","author":"P Janicic","year":"2012","unstructured":"Janicic, P., Narboux, J., Quaresma, P.: The area method: a recapitulation. J. Autom. Reason. 48(4), 489\u2013532 (2012)","journal-title":"J. Autom. Reason."},{"issue":"8","key":"9374_CR16","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/j.comgeo.2010.06.004","volume":"45","author":"N Magaud","year":"2012","unstructured":"Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8), 406\u2013424 (2012)","journal-title":"Comput. Geom."},{"key":"9374_CR17","doi-asserted-by":"crossref","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Botana, F., Lozano, E.R. (eds.), Post-Proceedings of Automated Deduction in Geometry 2006, Volume 4869 of LNCS, pp. 139\u2013156. Springer, Pontevedra, Spain (2007)","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9374_CR18","unstructured":"Oryszczyszyn, H., Prazmowski, K.: Classical configurations in affine planes. J. Formaliz. Math. 2 (1990)"},{"key":"9374_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-65611-8","volume-title":"Vorlesungen \u00fcber Neuere Geometrie","author":"M Pasch","year":"1976","unstructured":"Pasch, M.: Vorlesungen \u00fcber Neuere Geometrie. Springer, New York (1976)"},{"key":"9374_CR20","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, Volume 5170 of Lecture Notes in Computer Science, pp. 278\u2013293. Springer, New York (2008)","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"9374_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W Schwabh\u00e4user","year":"1983","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9374-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9374-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9374-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9374-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,7]],"date-time":"2019-09-07T04:12:29Z","timestamp":1567829549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9374-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,29]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["9374"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9374-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,29]]}}}