Alternative Graph Structures

Abstract

We define the notion of a graph anew without using the available Mizar structures. In our approach, we model graph structure as a finite function whose domain is a subset of natural numbers. The elements of the do main of the function play the role of selectors for accessing the components of the structure. As these selectors are first class objects, many future extensions of the new graph structure turned out to be easier to formalize in Mizar than with the traditional Mizar structures. After introducing graph structure, we define its selectors and then conditions that the structure needs to satisfy to form a directed graph (in the spirit of [13]). For these graphs we define a collection of basic graph notions; the presentation of these notions is continued in articles [16, 15, 17]. We have tried to follow a number of graph theory books in choosing graph terminology but since the terminology is not commonly agreed upon, we had to make a number of compromises, see [14].