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]).
@article{bwmeta1.element.doi-10_1515_forma-2017-0011,
author = {Roland Coghetto},
title = {Pascal's Theorem in Real Projective Plane},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {107-119},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0011}
}
Roland Coghetto. Pascal’s Theorem in Real Projective Plane. Formalized Mathematics, Tome 25 (2017) pp. 107-119. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0011/