REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

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 Theoremreal projective planGrassmann- Plücker relationProver9 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łymstokuCC-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 RozmiarFormat