{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:03:11Z","timestamp":1777424591150,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540773559","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77356-6_9","type":"book-chapter","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T06:23:13Z","timestamp":1196922193000},"page":"139-156","source":"Crossref","is-referenced-by-count":25,"title":["Mechanical Theorem Proving in Tarski\u2019s Geometry"],"prefix":"10.1007","author":[{"given":"Julien","family":"Narboux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Coq development team, The: The Coq proof assistant reference manual, Version 8.0. LogiCal Project (2004)"},{"key":"9_CR2","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), http:\/\/www.springerlink.com\/content\/p2mh1ad6ede09g6x\/"},{"key":"9_CR3","unstructured":"Paulson, L.C.: The Isabelle reference manual (2006)"},{"key":"9_CR4","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. Meikle","year":"2003","unstructured":"Meikle, L., Fleuriot, J.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003), http:\/\/springerlink.metapress.com\/content\/6ngakhj9k7qj71th\/?p=e4d2c272843b41148f0550f9c5ad8a2a&pi=20"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. The bulletin of Symbolic Logic\u00a05(2) (1999)","DOI":"10.2307\/421089"},{"key":"9_CR6","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)"},{"issue":"1","key":"9_CR7","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":"9_CR8","unstructured":"Narboux, J.: Toward the use of a proof assistant to teach mathematics. In (ICTMT7). Proceedings of the 7th International Conference on Technology in Mathematics Teaching (2005)"},{"key":"9_CR9","unstructured":"Narboux, J.: A graphical user interface for formal proofs in geometry. The Journal of Automated Reasoning special issue on User Interface for Theorem Proving\u00a039(2) (2007), http:\/\/www.informatik.uni-bremen.de\/%7Ecxl\/uitp-jar\/ , http:\/\/springerlink.metapress.com\/content\/b60418176x313vx6\/?p=aa2ae37923ab455291ee15f6c9c39b9b&pi=3"},{"key":"9_CR10","first-page":"1113","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. Revue des Sciences et Technologies de l\u2019Information, Technique et Science Informatiques, Langages applicatifs\u00a024, 1113\u20131138 (2005)","journal-title":"Revue des Sciences et Technologies de l\u2019Information, Technique et Science Informatiques, Langages applicatifs"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hulls algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 346\u2013361. Springer, Heidelberg (2001)"},{"key":"9_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry","author":"L. Meikle","year":"2006","unstructured":"Meikle, L., Fleuriot, J.: Mechanical theorem proving in computation geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"9_CR13","volume-title":"Pattern Recognition","author":"J.F. Dufourd","year":"2007","unstructured":"Dufourd, J.F.: Design and formal proof of a new optimal image segmentation program with hypermaps. In: Pattern Recognition, vol.\u00a040(11), Elsevier, Amsterdam (2007), http:\/\/portal.acm.org\/citation.cfm?id=1274191.1274325&coll=GUIDE&dl=%23url.coll"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2004)"},{"key":"9_CR15","unstructured":"Narboux, J.: Formalisation et automatisation du raisonnement g\u00e9om\u00e9trique en Coq. PhD thesis, Universit\u00e9 Paris Sud (September 2006)"},{"key":"9_CR16","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S.C. Chou","year":"1994","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. University of California Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"9_CR18","unstructured":"Tarski, A.: The completeness of elementary algebra and geometry (1967)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Tarski, A.: What is elementary geometry? In: Henkin, L., Tarski, P.S. (eds.) The axiomatic Method, with special reference to Geometry and Physics, Amsterdam, North-Holland, pp. 16\u201329 (1959)","DOI":"10.1016\/S0049-237X(09)70017-5"},{"key":"9_CR20","unstructured":"Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)"},{"key":"9_CR21","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant - A tutorial - Version 8.0 (April 2004)"},{"key":"9_CR22","series-title":"An EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG-88. LNCS, vol.\u00a0417, Springer, Heidelberg (1990)"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(95)00005-2","volume":"76","author":"J. Plato von","year":"1995","unstructured":"von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic\u00a076, 169\u2013200 (1995)","journal-title":"Annals of Pure and Applied Logic"},{"key":"9_CR25","unstructured":"Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution, Coq V5.10 (1995)"}],"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-540-77356-6_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,29]],"date-time":"2021-08-29T20:12:44Z","timestamp":1630267964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77356-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540773559"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77356-6_9","relation":{},"subject":[]}}