{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:32Z","timestamp":1740123332391,"version":"3.37.3"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,1,18]],"date-time":"2024-01-18T00:00:00Z","timestamp":1705536000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,18]],"date-time":"2024-01-18T00:00:00Z","timestamp":1705536000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s10817-023-09690-2","type":"journal-article","created":{"date-parts":[[2024,1,18]],"date-time":"2024-01-18T14:02:00Z","timestamp":1705586520000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry"],"prefix":"10.1007","volume":"68","author":[{"given":"David","family":"Braun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9477-4394","authenticated-orcid":false,"given":"Nicolas","family":"Magaud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Schreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,1,18]]},"reference":[{"key":"9690_CR1","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: International Conference on Certified Programs and Proofs, pp. 135\u2013150. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"9690_CR2","unstructured":"Armand, M., Gr\u00e9goire, G., Keller, B., Th\u00e9ry, L., Werner, B.: Verifying SAT and SMT in Coq for a fully automated decision procedure. In: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT\u201911) (2011)"},{"key":"9690_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201428th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 2\u20137 April 2022. Proceedings, Part I, Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9690_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-018-9606-x","author":"M Beeson","year":"2019","unstructured":"Beeson, M., Narboux, J., Wiedijk, F.: Proof-checking Euclid. Ann. Math. Artif. Intell. (2019). https:\/\/doi.org\/10.1007\/s10472-018-9606-x","journal-title":"Ann. Math. Artif. Intell."},{"issue":"5","key":"9690_CR5","first-page":"675","volume":"6","author":"PO Bell","year":"1955","unstructured":"Bell, P.O.: Generalized theorems of Desargues for n-dimensional projective space. Proc. Am. Math. Soc. 6(5), 675\u2013681 (1955)","journal-title":"Proc. Am. Math. Soc."},{"key":"9690_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Berlin (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9690_CR7","unstructured":"Blanchette, J.C., Paulson, L.C.: Hammering away: A user\u2019s guide to Sledgehammer for Isabelle\/HOL (2011)"},{"key":"9690_CR8","doi-asserted-by":"publisher","unstructured":"Bouton, T., Oliveira, D.C.B.D., D\u00e9harbe, D., Fontaine, P.: verit: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, 2\u20137 August 2009. Proceedings. Lecture Notes in Computer Science, vol. 5663, pp. 151\u2013156. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"9690_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9422-8","author":"P Boutry","year":"2017","unstructured":"Boutry, P., Gries, C., Narboux, J., Schreck, P.: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. J. Autom. Reason. (2017). https:\/\/doi.org\/10.1007\/s10817-017-9422-8","journal-title":"J. Autom. Reason."},{"key":"9690_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.jsc.2018.04.007","volume":"90","author":"P Boutry","year":"2019","unstructured":"Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symb. Comput. 90, 149\u2013168 (2019). https:\/\/doi.org\/10.1016\/j.jsc.2018.04.007","journal-title":"J. Symb. Comput."},{"key":"9690_CR11","unstructured":"Braun, D.: Approche combinatoire pour l\u2019automatisation en coq des preuves formelles en g\u00e9om\u00e9trie d\u2019incidence projective. PhD thesis, University of Strasbourg (2019)"},{"issue":"2\u20134","key":"9690_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s10472-018-9604-z","volume":"85","author":"D Braun","year":"2019","unstructured":"Braun, D., Magaud, N., Schreck, P.: Two cryptomorphic formalizations of projective incidence geometry. Ann. Math. Artif. Intell. 85(2\u20134), 193\u2013212 (2019). https:\/\/doi.org\/10.1007\/s10472-018-9604-z","journal-title":"Ann. Math. Artif. Intell."},{"key":"9690_CR13","doi-asserted-by":"publisher","unstructured":"Braun, D., Magaud, N., Schreck, P.: Two new ways to formally prove Dandelin\u2013Gallucci\u2019s theorem. In: Chyzak, F., Labahn , G. (eds.) ISSAC \u201921: International Symposium on Symbolic and Algebraic Computation, Virtual Event, Russia, 18\u201323 July 2021, pp. 59\u201366. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3452143.3465550","DOI":"10.1145\/3452143.3465550"},{"key":"9690_CR14","doi-asserted-by":"crossref","unstructured":"Buekenhout, F. (ed.): Handbook of Incidence Geometry. North Holland, Amsterdam (1995)","DOI":"10.1016\/B978-044488355-1\/50005-0"},{"key":"9690_CR15","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications, pp. 11\u201327. Citeseer (2003)"},{"key":"9690_CR16","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, Version 8.15. LogiCal Project (2022). http:\/\/coq.inria.fr"},{"key":"9690_CR17","volume-title":"Projective Geometry","author":"HSM Coxeter","year":"2003","unstructured":"Coxeter, H.S.M.: Projective Geometry. Springer, New York (2003)"},{"issue":"1\u20134","key":"9690_CR18","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141, Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1\u20134), 423\u2013453 (2018)","journal-title":"J. Autom. Reason."},{"key":"9690_CR19","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9690_CR20","doi-asserted-by":"publisher","unstructured":"Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: Smtcoq: a plug-in for integrating SMT solvers into coq. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification\u201429th International Conference, CAV 2017, Heidelberg, Germany, 24\u201328 July 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 126\u2013133. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"9690_CR21","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Marion, J., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Proceedings. LNCS, vol. 3920, pp. 167\u2013181. Springer, Berlin (2006)","DOI":"10.1007\/11691372_11"},{"issue":"2","key":"9690_CR22","first-page":"167","volume":"23","author":"\u00c1G Horv\u00e1th","year":"2019","unstructured":"Horv\u00e1th, \u00c1.G.: The theorem of Gallucci revisited. J. Geom. Graph. 23(2), 167\u2013178 (2019)","journal-title":"J. Geom. Graph."},{"key":"9690_CR23","doi-asserted-by":"publisher","DOI":"10.1155\/2014\/276108","volume":"2014","author":"D Kodokostas","year":"2014","unstructured":"Kodokostas, D.: Proving and generalizing Desargues\u2019 two-triangle theorem in 3-dimensional projective space. Geometry 2014, 276108 (2014). https:\/\/doi.org\/10.1155\/2014\/276108","journal-title":"Geometry"},{"key":"9690_CR24","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: International Conference on Computer Aided Verification, pp. 1\u201335. Springer, Cham (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9690_CR25","doi-asserted-by":"publisher","unstructured":"Magaud, N.: Integrating an automated prover for projective geometry as a new tactic in the coq proof assistant. In: Keller, C., Fleury, M. (eds.) Proceedings of 7th Workshop on Proof eXchange for Theorem Proving, Pittsburg, USA, 11 July 2021, Electronic Proceedings in Theoretical Computer Science, vol. 336, pp. 40\u201347. Open Publishing Association (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.4","DOI":"10.4204\/EPTCS.336.4"},{"key":"9690_CR26","doi-asserted-by":"crossref","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Automated Deduction in Geometry (ADG\u20192008). LNAI, vol. 6301, pp. 141\u2013162. Springer, Berlin (2008). http:\/\/hal.inria.fr\/inria-00305998","DOI":"10.1007\/978-3-642-21046-4_7"},{"issue":"8","key":"9690_CR27","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/j.comgeo.2010.06.004","volume":"45","author":"N Magaud","year":"2012","unstructured":"Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. Theory Appl. 45(8), 406\u2013424 (2012)","journal-title":"Comput. Geom. Theory Appl."},{"key":"9690_CR28","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: Electronic Notes in Theoretical Computer Science, vol. 144, pp. 43\u201351. Elsevier, Amsterdam (2006)","DOI":"10.1016\/j.entcs.2005.12.005"},{"issue":"5\u20136","key":"9690_CR29","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. Int. J. Comput. Geom. Appl. 16(5\u20136), 443\u2013460 (2006)","journal-title":"Int. J. Comput. Geom. Appl."},{"key":"9690_CR30","unstructured":"Moore, R.E.: Interval arithmetic and automatic error analysis in digital computing. Ph.D. thesis, Department of Computer Science, Stanford University (1962)"},{"key":"9690_CR31","doi-asserted-by":"publisher","unstructured":"Narboux, J.: Mechanical theorem proving in Tarski\u2019s geometry. In: Eugenio Roanes Lozano, F.B. (ed.) Automated Deduction in Geometry 2006. LNCS, vol. 4869, pp. 139\u2013156. Springer, Pontevedra (2006). https:\/\/doi.org\/10.1007\/978-3-540-77356-6","DOI":"10.1007\/978-3-540-77356-6"},{"key":"9690_CR32","volume-title":"Matroid Theory","author":"JG Oxley","year":"2006","unstructured":"Oxley, J.G.: Matroid Theory, vol. 3. Oxford University Press, Oxford (2006)"},{"key":"9690_CR33","doi-asserted-by":"crossref","unstructured":"Roanes-Mac\u00edas, E., Roanes-Lozano, E.: A maple package for automatic theorem proving and discovery in 3d-geometry. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Pontevedra, Spain, 31 August\u20132 September 2006. Revised Papers, Lecture Notes in Computer Science, vol. 4869, pp. 171\u2013188. Springer, Berlin (2006)","DOI":"10.1007\/978-3-540-77356-6_11"},{"key":"9690_CR34","doi-asserted-by":"crossref","unstructured":"Schreck, P., Magaud, N., Braun, D.: Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach. In: Automated Deduction in Geometry (ADG 2021) (2021). http:\/\/icube-publis.unistra.fr\/6-SMB21","DOI":"10.4204\/EPTCS.352.8"},{"key":"9690_CR35","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/j.jsc.2018.04.006","volume":"90","author":"P Schreck","year":"2019","unstructured":"Schreck, P., Mathis, P.: Using jointly geometry and algebra to determine rc-constructibility. J. Symb. Comput. 90, 124\u2013148 (2019). https:\/\/doi.org\/10.1016\/j.jsc.2018.04.006","journal-title":"J. Symb. Comput."},{"key":"9690_CR36","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP World\u2014infrastructure for automated reasoning. In: Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, No. 6355 in Lecture Notes in Artificial Intelligence, pp. 1\u201312. Springer, Dakar (2010)","DOI":"10.1007\/978-3-642-17511-4_1"},{"issue":"3","key":"9690_CR37","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BF02328447","volume":"2","author":"W Wen-Ts\u00fcn","year":"1986","unstructured":"Wen-Ts\u00fcn, W.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221\u2013252 (1986). https:\/\/doi.org\/10.1007\/BF02328447","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09690-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09690-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09690-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T13:13:10Z","timestamp":1710767590000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09690-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,18]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["9690"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09690-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,1,18]]},"assertion":[{"value":"22 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 November 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 January 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"3"}}