Title
Formalization of Planar Graphs
Abstract
Among many fields of mathematics and computer science, discrete mathematics is one of the most difficult fields to formalize because we prove theorems using intuitive inferences that have not been rigorously formalized yet. This paper focuses on graph theory from discrete mathematics and formalizes planar graphs. Although planar graphs are usually defined by embeddings into the two-dimensional real space, this definition can hardly be used for actually developing a formal theory of planar graphs. In this paper, we take another approach; we inductively define planar graphs and prove their properties based on the inductive definition. Before the definition of planar graphs, the theory of cycles is also introduced and used as a foundation of planar graphs. As an application of the theory of planar graphs, Euler's formula is proved.
Year
DOI
Venue
1995
10.1007/3-540-60275-5_77
TPHOLs
Keywords
Field
DocType
planar graphs,planar graph,graph theory,discrete mathematics
Graph theory,Discrete mathematics,Outerplanar graph,Forbidden graph characterization,Computer science,Planar straight-line graph,Theoretical computer science,Book embedding,Pathwidth,Topological graph theory,Planar graph
Conference
ISBN
Citations 
PageRank 
3-540-60275-5
8
0.74
References 
Authors
4
4
Name
Order
Citations
PageRank
Mitsuharu Yamamoto19111.09
Shin-ya Nishizaki2389.21
Masami Hagiya3649102.85
Yozo Toda4111.27