# Pascal’s Theorem in Real Projective Plane

Formalized Mathematics (2017)

- Volume: 25, Issue: 2, page 107-119
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topRoland Coghetto. "Pascal’s Theorem in Real Projective Plane." Formalized Mathematics 25.2 (2017): 107-119. <http://eudml.org/doc/288381>.

@article{RolandCoghetto2017,

abstract = {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]).},

author = {Roland Coghetto},

journal = {Formalized Mathematics},

keywords = {Pascal’s theorem; real projective plane; Grassman-Plücker relation},

language = {eng},

number = {2},

pages = {107-119},

title = {Pascal’s Theorem in Real Projective Plane},

url = {http://eudml.org/doc/288381},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Roland Coghetto

TI - Pascal’s Theorem in Real Projective Plane

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 2

SP - 107

EP - 119

AB - 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]).

LA - eng

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

UR - http://eudml.org/doc/288381

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.