{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:58Z","timestamp":1750220458306,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T00:00:00Z","timestamp":1626566400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,7,18]]},"DOI":"10.1145\/3452143.3465550","type":"proceedings-article","created":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T22:32:21Z","timestamp":1626215541000},"page":"59-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Two New Ways to Formally Prove Dandelin-Gallucci's Theorem"],"prefix":"10.1145","author":[{"given":"David","family":"Braun","sequence":"first","affiliation":[{"name":"ICube UMR 7357 CNRS, Universit\u00e9 de Strasbourg, Strasbourg, France"}]},{"given":"Nicolas","family":"Magaud","sequence":"additional","affiliation":[{"name":"ICube UMR 7357 CNRS, Universit\u00e9 de Strasbourg, Strasbourg, France"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[{"name":"ICube UMR 7357 CNRS, Universit\u00e9 de Strasbourg, Strasbourg, France"}]}],"member":"320","published-online":{"date-parts":[[2021,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373207.3404065"},{"key":"e_1_3_2_1_2_1","volume-title":"Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions. Springer, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2018.04.007"},{"key":"e_1_3_2_1_4_1","first-page":"130","volume-title":"Xiao-Shan Gao","author":"de la Tour Thierry Boy","year":"1998","unstructured":"Thierry Boy de la Tour, St\u00e9 phane F\u00e8 vre, and Dongming Wang. Clifford Term Rewriting for Geometric Reasoning in 3D. In Xiao-Shan Gao, Dongming Wang, and Lu Yang, editors, Automated Deduction in Geometry, ADG'98, Beijing, China, Proceedings, volume 1669, pages 130--155. LNCS, Springer, 1998."},{"key":"e_1_3_2_1_6_1","volume-title":"Two cryptomorphic formalizations of projective incidence geometry. Ann. Math. Artif. Intell., 85(2--4):193--212","author":"Braun David","year":"2019","unstructured":"David Braun, Nicolas Magaud, and Pascal Schreck. Two cryptomorphic formalizations of projective incidence geometry. Ann. Math. Artif. Intell., 85(2--4):193--212, 2019."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.12.023"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/39060"},{"key":"e_1_3_2_1_9_1","first-page":"183","volume-title":"G\u00e9 rard D","author":"Conti Pasqualina","year":"1995","unstructured":"Pasqualina Conti and Carlo Traverso. A case of automatic theorem proving in euclidean geometry: the maclane 8(mbox3 )theorem. In G\u00e9 rard D. Cohen, Marc Giusti, and Teo Mora, editors, Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, 11th International Symposium, AAECC-11, Paris, France, Proceedings, volume 948, pages 183--193. LNCS, Springer, 1995."},{"key":"e_1_3_2_1_10_1","volume-title":"LogiCal Project","author":"Coq","year":"2019","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, Version 8.9. LogiCal Project, 2019."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01584082"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.54870\/1551-3440.1034"},{"key":"e_1_3_2_1_13_1","first-page":"71","volume-title":"Certified Programs and Proofs, CPP","author":"Jean-David G\u00e9","year":"2011","unstructured":"Jean-David G\u00e9 nevaux, Julien Narboux, and Pascal Schreck. Formalization of Wu's Simple Method in Coq. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, CPP 2011, Kenting, Taiwan. Proceedings, volume 7086, pages 71--86. LNCS, Springer, 2011."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/190347.190354"},{"issue":"2","key":"e_1_3_2_1_15_1","first-page":"167","article-title":"The Theorem of Gallucci revisited","volume":"23","author":"Horv\u00e1th \u00c1kos G","year":"2019","unstructured":"\u00c1kos G Horv\u00e1th. The Theorem of Gallucci revisited. Journal of Geometry and Graphics, 23(2):167--178, 2019.","journal-title":"Journal of Geometry and Graphics"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comgeo.2010.06.004"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218195906002130"},{"key":"e_1_3_2_1_18_1","volume-title":"Matroid Theory","author":"Oxley James G","year":"2006","unstructured":"James G Oxley. Matroid Theory, volume 3. Oxford University Press, USA, 2006."},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2018","author":"Pogudin Gleb","year":"2018","unstructured":"Gleb Pogudin and \u00c1 gnes Sz\u00e1 nt\u00f3. Irredundant triangular decomposition. In Manuel Kauers, Alexey Ovchinnikov, and \u00c9 ric Schost, editors, Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2018, New York, NY, USA, pages 311--318. ACM, 2018."},{"key":"e_1_3_2_1_20_1","volume-title":"Connecting the 3D DGS Calques3D with the CAS Maple. Math. Comput. Simul., 80(6):1153--1176","author":"Roanes-Lozano Eugenio","year":"2010","unstructured":"Eugenio Roanes-Lozano, Nicolas van Labeke, and Eugenio Roanes-Mac'ias. Connecting the 3D DGS Calques3D with the CAS Maple. Math. Comput. Simul., 80(6):1153--1176, 2010."},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"171","volume-title":"Francisco Botana and Tom\u00e1 s Recio","author":"Eugenio Roanes-Lozano Eugenio","year":"2006","unstructured":"Eugenio Roanes-Mac'i as and Eugenio Roanes-Lozano. A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry. In Francisco Botana and Tom\u00e1 s Recio, editors, Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Pontevedra, Spain, Aug. 31-Sept. 2, 2006. Revised Papers, volume 4869 of Lecture Notes in Computer Science, pages 171--188. Springer, 2006."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1959-0101527-3"},{"key":"e_1_3_2_1_23_1","first-page":"207","article-title":"Basic principles of mechanical theorem proving in elementary geometries","volume":"4","author":"Wu W.T.","year":"1984","unstructured":"W.T. Wu. Basic principles of mechanical theorem proving in elementary geometries. Journal of Symbolic Computation, 4:207--235, 1984.","journal-title":"Journal of Symbolic Computation"}],"event":{"name":"ISSAC '21: International Symposium on Symbolic and Algebraic Computation","sponsor":["SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"],"location":"Virtual Event Russian Federation","acronym":"ISSAC '21"},"container-title":["Proceedings of the 2021 International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452143.3465550","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3452143.3465550","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:48:08Z","timestamp":1750193288000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452143.3465550"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,18]]},"references-count":22,"alternative-id":["10.1145\/3452143.3465550","10.1145\/3452143"],"URL":"https:\/\/doi.org\/10.1145\/3452143.3465550","relation":{},"subject":[],"published":{"date-parts":[[2021,7,18]]},"assertion":[{"value":"2021-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}