Pascal’s Theorem in Real Projective Plane

• Autorzy: Roland Coghetto
• 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]).

Słowa kluczowe

EN

Pascal’s theorem; real projective plane; Grassman-Plücker relation

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 51N15: Projective analytic geometry
• 51E15: Affine and projective planes

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 2
• Strony: 107-119

Daty

wydano

2017-07-01

otrzymano

2017-06-27

online

2017-09-23

Twórcy

autor

Roland Coghetto

• Rue de la Brasserie 5, ,

Identyfikatory

DOI

10.1515/forma-2017-0011