The Formalization of Simple Graphs

Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

The Formalization of Simple Graphs

Yozo Toda: Information Processing Center, Chiba University

Summary.

A graph is simple when \begin{itemize} \parskip -1mm \item it is non-directed, \item there is at most one edge between two vertices, \item there is no loop of length one. \end{itemize} A formalization of simple graphs is given from scratch. There is already an article [10], dealing with the similar subject. It is not used as a starting-point, because [10] formalizes directed non-empty graphs. Given a set of vertices, edge is defined as an (unordered) pair of different two vertices and graph as a pair of a set of vertices and a set of edges.\par The following concepts are introduced: \begin{itemize} \parskip -1mm \item simple graph structure, \item the set of all simple graphs, \item equality relation on graphs. \item the notion of degrees of vertices; the number of edges connected to, or the number of adjacent vertices, \item the notion of subgraphs, \item path, cycle, \item complete and bipartite complete graphs, \end{itemize}\par Theorems proved in this articles include: \begin{itemize} \parskip -1mm \item the set of simple graphs satisfies a certain minimality condition, \item equivalence between two notions of degrees. \end{itemize}

MML Identifier: SGRAPH1

The terminology and notation used in this paper have been introduced in the following articles [12] [7] [15] [13] [2] [1] [4] [5] [6] [3] [9] [8] [14] [11]