{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:59:15Z","timestamp":1777424355639,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642210457","type":"print"},{"value":"9783642210464","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-21046-4_7","type":"book-chapter","created":{"date-parts":[[2011,5,3]],"date-time":"2011-05-03T14:57:03Z","timestamp":1304434623000},"page":"141-162","source":"Crossref","is-referenced-by-count":12,"title":["Formalizing Projective Plane Geometry in Coq"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Magaud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a040(1), 61\u201385 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR3","volume-title":"Handbook of Incidence Geometry","year":"1995","unstructured":"Buekenhout, F. (ed.): Handbook of Incidence Geometry. North-Holland, Amsterdam (1995)"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1016\/S0315-0860(03)00049-1","volume":"31","author":"C. Cerroni","year":"2004","unstructured":"Cerroni, C.: Non-Desarguian Geometries and the Foundations of Geometry from David Hilbert to Ruth Moufang. Historia Mathematica\u00a031(3), 320\u2013336 (2004)","journal-title":"Historia Mathematica"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-39185-1_6","volume-title":"Types for Proofs and Programs","author":"L. Chicli","year":"2003","unstructured":"Chicli, L., Pottier, L., Simpson, D.: Mathematical quotients and quotient types in coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 95\u2013107. Springer, Heidelberg (2003)"},{"key":"7_CR6","series-title":"Series on Applied Mathematics","doi-asserted-by":"publisher","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. Series on Applied Mathematics. World Scientific, Singapore (1994)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrz\u0105szcz","year":"2003","unstructured":"Chrz\u0105szcz, J.: Implementing Modules in the Coq System. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"7_CR8","unstructured":"Coq development team, The: The Coq Proof Assistant Reference Manual, Version 8.0. LogiCal Project (2004)"},{"key":"7_CR9","volume-title":"Projective Geometry","author":"H.S.M. Coxeter","year":"1987","unstructured":"Coxeter, H.S.M.: Projective Geometry. Springer, Heidelberg (1987)"},{"key":"7_CR10","unstructured":"Cr\u00e9ci, J., Pottier, L.: Gb: une proc\u00e9dure de d\u00e9cision pour Coq. In: Actes JFLA 2004 (2004) (in french)"},{"key":"7_CR11","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_CR12","unstructured":"Duprat, J.: Une axiomatique de la g\u00e9om\u00e9trie plane en Coq. In: Actes des JFLA 2008, pp. 123\u2013136. INRIA (2008) (in french)"},{"key":"7_CR13","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) (in french)","journal-title":"Revue des Sciences et Technologies de l\u2019Information, Technique et Science Informatiques, Langages applicatifs"},{"key":"7_CR14","first-page":"160","volume-title":"The Axiomatic Method, with Special Reference to Geometry and Physics","author":"A. Heyting","year":"1959","unstructured":"Heyting, A.: Axioms for intuitionistic plane affine geometry. In: Suppes, P., Henkin, A.T.L. (eds.) The Axiomatic Method, with Special Reference to Geometry and Physics, pp. 160\u2013173. North-Holland, Amsterdam (1959)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1016\/B978-044451104-1\/50022-8","volume-title":"Handbook of Computer Aided Geometric Design","author":"C.M. Hoffmann","year":"2002","unstructured":"Hoffmann, C.M., Joan-Arinyo, R.: Parametric Modeling. In: Handbook of Computer Aided Geometric Design, pp. 519\u2013541. Elsevier, Amsterdam (2002)"},{"issue":"5-6","key":"7_CR16","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1142\/S0218195906002105","volume":"16","author":"C. Jermann","year":"2006","unstructured":"Jermann, C., Trombettoni, G., Neveu, B., Mathis, P.: Decomposition of Geometric Constraint Systems: a Survey. International Journal of Computational Geometry and Application\u00a016(5-6), 379\u2013414 (2006)","journal-title":"International Journal of Computational Geometry and Application"},{"issue":"5","key":"7_CR17","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1016\/S0747-7171(03)00067-1","volume":"36","author":"H. Li","year":"2003","unstructured":"Li, H., Wu, Y.: Automated Short Proof Generation for Projective Geometric Theorems with Cayley and Bracket Algebras: I. incidence geometry. J. Symb. Comput.\u00a036(5), 717\u2013762 (2003)","journal-title":"J. Symb. Comput."},{"key":"7_CR18","volume-title":"Proceedings of the ACM Symposium on Applied Computing, SAC 2009","author":"N. Magaud","year":"2009","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues\u2019 theorem in Coq using ranks. In: Proceedings of the ACM Symposium on Applied Computing, SAC 2009. ACM Press, New York (2009)"},{"key":"7_CR19","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 hilbert\u2019s grundlagen in isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003)"},{"key":"7_CR20","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.I. Meikle","year":"2006","unstructured":"Meikle, L.I., Fleuriot, J.D.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/1128888.1128915","volume-title":"SPM 2006: Proceedings of the 2006 ACM Symposium on Solid and Physical Modeling","author":"D. Michelucci","year":"2006","unstructured":"Michelucci, D., Foufou, S., Lamarque, L., Schreck, P.: Geometric constraints solving: some tracks. In: SPM 2006: Proceedings of the 2006 ACM Symposium on Solid and Physical Modeling, pp. 185\u2013196. ACM Press, New York (2006)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-39185-1_14","volume-title":"Types for Proofs and Programs","author":"A. Miquel","year":"2003","unstructured":"Miquel, A., Werner, B.: The Not So Simple Proof-Irrelevant Model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 240\u2013258. Springer, Heidelberg (2003)"},{"issue":"2","key":"7_CR23","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1090\/S0002-9947-1902-1500595-3","volume":"3","author":"F.R. Moulton","year":"1902","unstructured":"Moulton, F.R.: A Simple Non-Desarguesian Plane Geometry. Transactions of the American Mathematical Society\u00a03(2), 192\u2013195 (1902)","journal-title":"Transactions of the American Mathematical Society"},{"key":"7_CR24","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_CR25","series-title":"Lecture Notes in Artificial Intelligence","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_CR26","unstructured":"Paulson, L.C.: The Isabelle reference manual (2006)"},{"key":"7_CR27","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 Hull Algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 346\u2013361. Springer, Heidelberg (2001)"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"von Plato, J.: The Axioms of Constructive Geometry. In: Annals of Pure and Applied Logic, vol.\u00a076, pp. 169\u2013200 (1995)","DOI":"10.1016\/0168-0072(95)00005-2"},{"issue":"1-2","key":"7_CR29","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF01531327","volume":"13","author":"J. Richter-Gebert","year":"1995","unstructured":"Richter-Gebert, J.: Mechanical Theorem Proving in Projective Geometry. Ann. Math. Artif. Intell.\u00a013(1-2), 139\u2013172 (1995)","journal-title":"Ann. Math. Artif. Intell."},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Schreck, P.: Robustness in CAD Geometric Construction. In: 5th International Conference on Information Visualisation IV 2001, London, pp. 111\u2013116 (July 2001)","DOI":"10.1109\/IV.2001.942046"},{"key":"7_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W. Schwabhauser","year":"1983","unstructured":"Schwabhauser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Heidelberg (1983) (in german)"},{"key":"7_CR32","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)"},{"key":"7_CR33","first-page":"16","volume-title":"The Axiomatic Method, with Special Reference to Geometry and Physics","author":"A. Tarski","year":"1959","unstructured":"Tarski, A.: What is Elementary Geometry? In: Henkin, L., Suppes, P., Tarski, A. (eds.) The Axiomatic Method, with Special Reference to Geometry and Physics, pp. 16\u201329. North-Holland, Amsterdam (1959)"}],"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-21046-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T10:37:17Z","timestamp":1741171037000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21046-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642210457","9783642210464"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21046-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}