Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
A formal proof of Euler's polyhedron formula
2009
slgr-formal-proof
Euler's polyhedron formula asserts for a polyhedron [i]p[/i] that [i]V[/i] - [i]E[/i] + [i]F[/i] = 2, where [i]V[/i], [i]E[/i], and [i]F[/i] are, respectively, the numbers of vertices, edges, and faces of [i]p[/i]. This paper concerns a formal proof in the MIZAR system of Euler's polyhedron formula carried out by the author. We discuss the informal proof (Poincaré's) on which the formal proof is based, the formalism in which the proof was carried out, notable features of the formalization, and related projects.
Journal
Jesse Alama
Studies in Logic, Grammar and Rhetoric
University of Białystok
-
18
31
9-23
978-83-7431-229-5
0860-150X
-
http://logika.uwb.edu.pl/studies/index.html
Export formats
Jesse Alama, A formal proof of Euler's polyhedron formula, Studies in Logic, Grammar and Rhetoric, Vol. 18, No. 31, Pag. 9-23, University of Białystok, ISBN 978-83-7431-229-5, ISSN 0860-150X, (http://logika.uwb.edu.pl/studies/index.html), 2009.
<b><a href="/people/members/view.php?code=d18f2a73808637adda0742073904f056" class="author">Jesse Alama</a></b>, <u>A formal proof of Euler's polyhedron formula</u>, Studies in Logic, Grammar and Rhetoric, Vol. 18, No. 31, Pag. 9-23, University of Białystok, ISBN 978-83-7431-229-5, ISSN 0860-150X, (<a href="http://logika.uwb.edu.pl/studies/index.html" target="_blank">url</a>), 2009.
@article {slgr-formal-proof, author = {Jesse Alama}, title = {A formal proof of Euler's polyhedron formula}, journal = {Studies in Logic, Grammar and Rhetoric}, publisher = {University of Białystok}, volume = {18}, number = {31}, pages = {9-23}, isbn = {978-83-7431-229-5}, issn = {0860-150X}, url = {http://logika.uwb.edu.pl/studies/index.html}, abstract = {Euler's polyhedron formula asserts for a polyhedron [i]p[/i] that [i]V[/i] - [i]E[/i] + [i]F[/i] = 2, where [i]V[/i], [i]E[/i], and [i]F[/i] are, respectively, the numbers of vertices, edges, and faces of [i]p[/i]. This paper concerns a formal proof in the MIZAR system of Euler's polyhedron formula carried out by the author. We discuss the informal proof (Poincar{\'e}'s) on which the formal proof is based, the formalism in which the proof was carried out, notable features of the formalization, and related projects.}, year = {2009}, }
Publication's urls
/publications/view.php?code=25d18610f8817e4269879308b964698c
/publications/view.php?code=slgr-formal-proof
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT