{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:03:00Z","timestamp":1771063380573,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642406713","type":"print"},{"value":"9783642406720","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40672-0_7","type":"book-chapter","created":{"date-parts":[[2013,9,2]],"date-time":"2013-09-02T11:49:04Z","timestamp":1378122544000},"page":"89-109","source":"Crossref","is-referenced-by-count":14,"title":["From Tarski to Hilbert"],"prefix":"10.1007","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","reference":[{"key":"7_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. Review of Symbolic Logic\u00a02, 700\u2013768 (2009)","journal-title":"Review of Symbolic Logic"},{"key":"7_CR2","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, Version 8.3. TypiCal Project (2010)"},{"key":"7_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-45410-1_17","volume-title":"Automated Deduction in Geometry","author":"C. Dehlinger","year":"2001","unstructured":"Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hilbert\u2019s Elementary Geometry. In: Richter-Gebert, J., Wang, D. (eds.) ADG 2000. LNCS (LNAI), vol.\u00a02061, pp. 306\u2013324. Springer, Heidelberg (2001)"},{"key":"7_CR4","unstructured":"Paulson, L.C.: The Isabelle reference manual (2006)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/10930755_21","volume-title":"Theorem Proving in Higher Order Logics","author":"L.I. Meikle","year":"2003","unstructured":"Meikle, L.I., Fleuriot, J.D.: Formalizing Hilberts Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003)"},{"key":"7_CR6","unstructured":"Scott, P.: Mechanising hilbert\u2019s foundations of geometry in isabelle. Master\u2019s thesis, University of Edinburgh (2008)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-25070-5_11","volume-title":"Automated Deduction in Geometry","author":"P. Scott","year":"2011","unstructured":"Scott, P., Fleuriot, J.: An Investigation of Hilbert\u2019s Implicit Reasoning through Proof Discovery in Idle-Time. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol.\u00a06877, pp. 182\u2013200. Springer, Heidelberg (2011)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. The Bulletin of Symbolic Logic\u00a05(2) (June 1999)","DOI":"10.2307\/421089"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer (1983) (in German)","DOI":"10.1007\/978-3-642-69418-9"},{"issue":"1","key":"7_CR10","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. Journal of Automated Reasoning\u00a05(1), 97\u2013118 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR11","unstructured":"Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)"},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"1113","DOI":"10.3166\/tsi.24.1113-1138","volume":"24","author":"F. Guilhot","year":"2005","unstructured":"Guilhot, F.: Formalisation en Coq et visualisation d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. TSI\u00a024, 1113\u20131138 (2005) (in French)","journal-title":"TSI"},{"key":"7_CR13","unstructured":"Pham, T.M.: Description formelle de propri\u00e9t\u00e9 g\u00e9om\u00e9triques. PhD thesis, Universit\u00e9 de Nice - Sophia-Antipolis (2011)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific (1994)","DOI":"10.1142\/2196"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30142-4_17","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Narboux","year":"2004","unstructured":"Narboux, J.: A decision procedure for geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 225\u2013240. Springer, Heidelberg (2004)"},{"key":"7_CR16","unstructured":"Narboux, J.: Formalisation et automatisation du raisonnement g\u00e9om\u00e9trique en Coq. PhD thesis, Universit\u00e9 Paris Sud (September 2006) (in French)"},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a048(4), 489\u2013532 (2012)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. D.\u00a0Reidel Publishing Company (1988)","DOI":"10.1007\/978-94-009-4037-6"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-25379-9_8","volume-title":"Certified Programs and Proofs","author":"J.-D. G\u00e9nevaux","year":"2011","unstructured":"G\u00e9nevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu\u2019s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 71\u201386. Springer, Heidelberg (2011)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-21898-9_32","volume-title":"Computational Science and Its Applications - ICCSA 2011","author":"T.-M. Pham","year":"2011","unstructured":"Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol.\u00a06785, pp. 368\u2013383. Springer, Heidelberg (2011)"},{"key":"7_CR21","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-77356-6_9","volume-title":"Automated Deduction in Geometry","author":"J. Narboux","year":"2007","unstructured":"Narboux, J.: Mechanical Theorem Proving in Tarski\u2019s geometry. In: Botana, F., Recio, T. (eds.) ADG 2006. LNCS (LNAI), vol.\u00a04869, pp. 139\u2013156. Springer, Heidelberg (2007)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40672-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:51:13Z","timestamp":1558054273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40672-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406713","9783642406720"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40672-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}