Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/6279
Tytuł: | Pascal’s Theorem in Real Projective Plane |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Pascal’s theorem real projective plane Grassman-Plücker relation |
Data wydania: | 2017 |
Data dodania: | 8-lut-2018 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 25, Issue 2, Pages 107–119 |
Abstrakt: | SummaryIn this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines. For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s work. With HOL Light, he has the proof of Pascal’s theorem2. For a lemma, we use PROVER93 and OTT2MIZ by Josef Urban4 [12, 6, 7]. We note, that we don’t use Skolem/Herbrand functions (see “Skolemization” in [1]). |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/6279 |
DOI: | 10.1515/forma-2017-0011 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2017, Volume 25, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2017-0011.pdf | 315,36 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL