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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ching-Tsun Chou. A formal theory of undirected graphs in higher-order logic. In Thomas F. Melham and Juanito Camilleri, editors, 7th International Workshop on Higher-Order Logic Theorem Proving System and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 144–157. Springer-Verlag, 1994.
Ching-Tsun Chou. Mechanical verification of distributed algorithms in higher-order logic. In Thomas F. Melham and Juanito Camilleri, editors, 7th International Workshop on Higher-Order Logic Theorem Proving System and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 158–176. Springer-Verlag, 1994.
Frank Harary. Graph theory. Addison-Wesley series in mathematics. Addison-Wesley, London, 1969.
Thomas F. Melham. The HOL sets Library. University of Cambridge, Computer Laboratory, October 1991.
Thomas F. Melham. A package for inductive relation definition in HOL. In Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System, pages 27–30. IEEE Computer Society Press, August 1991.
Seiya Negami. Discrete Structures. Number 3 in Information Mathematics Lectures. Kyouritsu Shuppan, Tokyo, Japan, May 1993. (in Japanese).
University of Cambridge, Computer Laboratory. The HOL System: DESCRIPTION, March 1994.
Jan van Leeuwen. Graph Algorithms, volume A of Handbook of Theoretical Computer Science, chapter 10, pages 525–633. MIT Press, 1990.
Wai Wong. A simple graph theory and its application in railway signaling. In M. Archer et al., editor, Proc. of 1991 Workshop on the HOL Theorem Proving System and Its Applications, pages 395–409. IEEE Computer Society Press, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yamamoto, M., Nishizaki, Sy., Hagiya, M., Toda, Y. (1995). Formalization of planar graphs. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_77
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive