Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/12385
Tytuł: | Pappus’s Hexagon Theorem in Real Projective Plane |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Pappus’s Hexagon Theorem real projective plan Grassmann- Plücker relation Prover9 |
Data wydania: | 2021 |
Data dodania: | 3-sty-2022 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 29, Issue 2, Pages 69-76 |
Abstrakt: | In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points A, B, C, and another set of collinear points a, b, c, then the intersection points X, Y, Z of line pairs Ab and aB, Ac and aC, Bc and bC are collinear”2. More precisely, we prove that the structure ProjectiveSpace TOP-REAL3 [10] (where TOP-REAL3 is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leonczuk and Krzysztof Prazmowski. Eugeniusz Kusak andWojciech Leonczuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” [12]. Secondly, Pascal’s theorem [4] is used. In both cases, to prove some lemmas, we use Prover93, the successor of the Otter prover and ott2miz by Josef Urban4 [13], [8], [7]. In Coq, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3]. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
Sponsorzy: | This work has been supported by the “Centre autonome de formation et de recherche en mathématiques et sciences avec assistants de preuve” ASBL (non-profit organization). Enterprise number: 0777.779.751. Belgium. |
URI: | http://hdl.handle.net/11320/12385 |
DOI: | 10.2478/forma-2021-0007 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4901-0766 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2021 University of Białymstoku CC-BY-SA License ver. 3.0 or later |
Występuje w kolekcji(ach): | Formalized Mathematics, 2021, Volume 29, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2021-0007.pdf | 298,71 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL