{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:52:25Z","timestamp":1777423945301,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642250699","type":"print"},{"value":"9783642250705","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-25070-5_3","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T20:30:55Z","timestamp":1320784255000},"page":"51-67","source":"Crossref","is-referenced-by-count":8,"title":["A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/0021-8693(85)90043-2","volume":"96","author":"M. Barnabei","year":"1985","unstructured":"Barnabei, M., Brini, A., Rota, G.C.: On the Exterior Calculus of Invariant Theory. Journal of Algebra\u00a096, 120\u2013160 (1985)","journal-title":"Journal of Algebra"},{"key":"3_CR2","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. Springer, Heidelberg (2004)"},{"key":"3_CR3","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, Version 8.2. LogiCal Project (2008), http:\/\/coq.inria.fr"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Crapo, H., Richter-Gebert, J.: Automatic proving of geometric theorems. In: White [16], pp. 167\u2013196","DOI":"10.1007\/978-94-015-8402-9_8"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Dorst, L., Fontijne, D., Mann, S.: Geometric Algebra for Computer Science: An Object Oriented Approach to Geometry. Morgan Kauffmann Publishers (2007)","DOI":"10.1016\/B978-012369465-2\/50004-9"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1002\/sapm1974533185","volume":"53","author":"P. Doubilet","year":"1974","unstructured":"Doubilet, P., Rota, G.C., Stein, J.: On the foundations of combinatorial theory. IX. Combinatorial methods in invariant theory. Studies in Applied Mathematics\u00a053, 185\u2013216 (1974)","journal-title":"Studies in Applied Mathematics"},{"issue":"8","key":"3_CR7","doi-asserted-by":"publisher","first-page":"2909","DOI":"10.1073\/pnas.91.8.2909","volume":"91","author":"M. Hawrylycz","year":"1994","unstructured":"Hawrylycz, M.: A geometric identity for Pappus\u2019 theorem. Proceedings of the National Academy of Sciences U.S.A.\u00a091(8), 2909 (1994)","journal-title":"Proceedings of the National Academy of Sciences U.S.A."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Hestenes, D., Sobczyk, G.: Clifford Algebra to Geometric Calculus: A Unified Language for Mathematics and Physics. In: Fundamental Theories of Physics, vol.\u00a05, Kluwer Academic Publishers (1984)","DOI":"10.1119\/1.14223"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Janicic, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning (2010) (published online)","DOI":"10.1007\/s10817-010-9209-7"},{"key":"3_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-540-24616-9_7","volume-title":"Automated Deduction in Geometry","author":"H. Li","year":"2004","unstructured":"Li, H.: Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol.\u00a02930, pp. 106\u2013123. Springer, Heidelberg (2004)"},{"issue":"5","key":"3_CR11","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. Journal of Symbolic Computation\u00a036(5), 717\u2013762 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-21046-4_7","volume-title":"Automated Deduction in Geometry","author":"N. Magaud","year":"2011","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane Geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol.\u00a06301, pp. 141\u2013162. Springer, Heidelberg (2011)"},{"key":"3_CR13","doi-asserted-by":"crossref","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, ACM Press (March 2009), http:\/\/lsiit.u-strasbg.fr\/Publications\/2009\/MNS09","DOI":"10.1145\/1529282.1529527"},{"issue":"5-6","key":"3_CR14","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1142\/S0218195906002130","volume":"16","author":"D. Michelucci","year":"2006","unstructured":"Michelucci, D., Schreck, P.: Incidence constraints: A combinatorial approach. International Journal of Computational Geometry & Applications\u00a016(5-6), 443\u2013460 (2006)","journal-title":"International Journal of Computational Geometry & Applications"},{"key":"3_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-4368-1","volume-title":"Algorithms in Invariant Theory","author":"B. Sturmfels","year":"1993","unstructured":"Sturmfels, B.: Algorithms in Invariant Theory. Springer, New York (1993)"},{"key":"3_CR16","volume-title":"Invariants Methods in Discrete and Computational Geometry","year":"1995","unstructured":"White, N.L. (ed.): Invariants Methods in Discrete and Computational Geometry. Kluwer, Dordrecht (1995)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"White, N.L.: A tutorial on Grassmann-Cayley algebra. In: Invariants Methods in Discrete and Computational Geometry [16], pp. 93\u2013106","DOI":"10.1007\/978-94-015-8402-9_5"},{"key":"3_CR18","first-page":"881","volume-title":"Handbook of Discrete and Computational Geometry","author":"N.L. White","year":"1997","unstructured":"White, N.L.: Geometric applications of the Grassmann-Cayley algebra. In: Handbook of Discrete and Computational Geometry, pp. 881\u2013892. CRC Press, Inc., Boca Raton (1997)"}],"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-25070-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T04:01:28Z","timestamp":1560916888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25070-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250699","9783642250705"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25070-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}