{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T02:05:26Z","timestamp":1783908326117,"version":"3.55.0"},"reference-count":15,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>In this article, we check with the Mizar system [1], [2], the converse of Desargues\u2019 theorem and the converse of Pappus\u2019 theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [11], [9], [15], [8]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean\/Hott [5], Isabelle\/Hol [3], Coq [13], [14], [4], Agda [6], . . . .<\/jats:p>\n                  <jats:p>\n                    Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [13] - the section on duality: \u201c[...] For every theorem we prove, we can easily derive its dual using our function swap [...]\n                    <jats:sup>2<\/jats:sup>\n                    \u201d).\n                  <\/jats:p>\n                  <jats:p>In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leo\u0144czuk and Pra\u017cmowski of the projective plane [12]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code.<\/jats:p>\n                  <jats:p>In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [12] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional).<\/jats:p>\n                  <jats:p>We hope that this methodology will allow us to continued more quickly the proof started in [7] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [10]).<\/jats:p>","DOI":"10.2478\/forma-2021-0016","type":"journal-article","created":{"date-parts":[[2022,7,9]],"date-time":"2022-07-09T16:34:17Z","timestamp":1657384457000},"page":"161-173","source":"Crossref","is-referenced-by-count":1,"title":["Duality Notions in Real Projective Plane"],"prefix":"10.2478","volume":"29","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"cafr-MSA2P asbl , Rue de la Brasserie 5 , La Louvi\u00e8re , Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2022,7,9]]},"reference":[{"key":"2026071215073947391_j_forma-2021-0016_ref_001","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071215073947391_j_forma-2021-0016_ref_002","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071215073947391_j_forma-2021-0016_ref_003","unstructured":"[3] Anthony Bordg. Projective geometry. Archive of Formal Proofs, jun 2018."},{"key":"2026071215073947391_j_forma-2021-0016_ref_004","unstructured":"[4] David Braun. Approche combinatoire pour l\u2019automatisation en Coq des preuves formelles en g\u00e9om\u00e9trie d\u2019incidence projective. PhD thesis, Universit\u00e9 de Strasbourg, 2019."},{"key":"2026071215073947391_j_forma-2021-0016_ref_005","doi-asserted-by":"crossref","unstructured":"[5] Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pages 1\u20138. IEEE, 2017.10.1109\/LICS.2017.8005146","DOI":"10.1109\/LICS.2017.8005146"},{"key":"2026071215073947391_j_forma-2021-0016_ref_006","doi-asserted-by":"crossref","unstructured":"[6] Guillermo Calder\u00f3n. Formalizing constructive projective geometry in Agda. Electronic Notes in Theoretical Computer Science, 338:61\u201377, 2018.10.1016\/j.entcs.2018.10.005","DOI":"10.1016\/j.entcs.2018.10.005"},{"key":"2026071215073947391_j_forma-2021-0016_ref_007","doi-asserted-by":"crossref","unstructured":"[7] Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21\u201332, 2018. doi:10.2478\/forma-2018-0003.","DOI":"10.2478\/forma-2018-0003"},{"key":"2026071215073947391_j_forma-2021-0016_ref_008","unstructured":"[8] Harold Scott Macdonald Coxeter. The real projective plane. Springer Science & Business Media, 1992."},{"key":"2026071215073947391_j_forma-2021-0016_ref_009","unstructured":"[9] Nikolai Vladimirovich Efimov. G\u00e9om\u00e9trie sup\u00e9rieure. Mir, 1981."},{"key":"2026071215073947391_j_forma-2021-0016_ref_010","doi-asserted-by":"crossref","unstructured":"[10] Adam Grabowski. Tarski\u2019s geometry modelled in Mizar computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gda\u0144sk, Poland, September 11\u201314, 2016, pages 373\u2013381, 2016. doi:10.15439\/2016F290.","DOI":"10.15439\/2016F290"},{"key":"2026071215073947391_j_forma-2021-0016_ref_011","unstructured":"[11] Robin Hartshorne. Foundations of projective geometry. Citeseer, 1967."},{"key":"2026071215073947391_j_forma-2021-0016_ref_012","unstructured":"[12] Wojciech Leo\u0144czuk and Krzysztof Pra\u017cmowski. Projective spaces \u2013 part I. Formalized Mathematics, 1(4):767\u2013776, 1990."},{"key":"2026071215073947391_j_forma-2021-0016_ref_013","doi-asserted-by":"crossref","unstructured":"[13] Nicolas Magaud, Julien Narboux, and Pascal Schreck. Formalizing projective plane geometry in Coq. In Automated Deduction in Geometry, pages 141\u2013162. Springer, 2008.10.1007\/978-3-642-21046-4_7","DOI":"10.1007\/978-3-642-21046-4_7"},{"key":"2026071215073947391_j_forma-2021-0016_ref_014","doi-asserted-by":"crossref","unstructured":"[14] Nicolas Magaud, Julien Narboux, and Pascal Schreck. A case study in formalizing projective geometry in Coq: Desargues theorem. Computational Geometry, 45(8):406\u2013424, 2012.","DOI":"10.1016\/j.comgeo.2010.06.004"},{"key":"2026071215073947391_j_forma-2021-0016_ref_015","doi-asserted-by":"crossref","unstructured":"[15] J\u00fcrgen Richter-Gebert. Pappos\u2019s Theorem: Nine Proofs and Three Variations, pages 3\u201331. Springer Berlin Heidelberg, 2011. ISBN 978-3-642-17286-1. doi:10.1007\/978-3-642-17286-1_1.","DOI":"10.1007\/978-3-642-17286-1_1"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2021-0016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T01:08:13Z","timestamp":1783904893000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2021-0016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,1]]},"references-count":15,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2022,7,9]]},"published-print":{"date-parts":[[2021,12,1]]}},"alternative-id":["10.2478\/forma-2021-0016"],"URL":"https:\/\/doi.org\/10.2478\/forma-2021-0016","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,1]]}}}