Back to Search
Start Over
Pascal’s Theorem in Real Projective Plane
- Source :
- Formalized Mathematics, Vol 25, Iss 2, Pp 107-119 (2017)
- Publication Year :
- 2017
- Publisher :
- Walter de Gruyter GmbH, 2017.
-
Abstract
- Summary 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]).
- Subjects :
- 0102 computer and information sciences
02 engineering and technology
grassman-plücker relation
01 natural sciences
03b35
Real projective plane
QA1-939
0202 electrical engineering, electronic engineering, information engineering
Projective space
Pascal's theorem
Non-Desarguesian plane
Projective geometry
Mathematics
Discrete mathematics
Brianchon's theorem
Applied Mathematics
Mathematics::History and Overview
real projective plane
Line at infinity
020207 software engineering
pascal’s theorem
Computational Mathematics
51e15
010201 computation theory & mathematics
Projective plane
51n15
Subjects
Details
- ISSN :
- 18989934 and 14262630
- Volume :
- 25
- Database :
- OpenAIRE
- Journal :
- Formalized Mathematics
- Accession number :
- edsair.doi.dedup.....3a41798eaae05590d82aaf64a49b60dc