PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2017 | 25 | 2 | 107-119
Tytuł artykułu

Pascal’s Theorem in Real Projective Plane

Autorzy
Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
In 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]).
Wydawca
Rocznik
Tom
25
Numer
2
Strony
107-119
Opis fizyczny
Daty
wydano
2017-07-01
otrzymano
2017-06-27
online
2017-09-23
Twórcy
  • Rue de la Brasserie 5, ,
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_1515_forma-2017-0011
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.