@MISC{GLIB_000.MIZ,
  AUTHOR = {Lee, Gilbert and Rudnicki, Piotr},
  NOTE1 = {Part of author's MSc work.},
  TITLE = {Alternative Graph Structures},
  NOTE = {This work has been partially supported by grants from NSERC,
          Alberta Ingenuity Fund and iCORE.},
  SECTION1 = {Definitions},
  SECTION2 = {Theorems},
  DAY = {22},
  MONTH = {February},
  YEAR = {2005},
  ADDRESS1 = {University of Victoria, Victoria, Canada},
  ADDRESS2 = {University of Alberta, Edmonton, Canada},
  SUMMARY = {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 domain 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.
    \par
    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 \cite{GRAPH_1.ABS}).  
    For these graphs we define a collection of basic graph notions;
    the presentation of these notions is continued in 
    articles \cite{GLIB_001.ABS,GLIB_002.ABS,GLIB_003.ABS}.
    \par
    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 \cite{gl04}.}}

@techreport(gl04,
  author=        {Gilbert Lee},
  title=         {Verification of graph algorithms in {M}izar},
  institution=   {Dept. of Comp. Sci., University of Alberta, Edmonton, Canada},
  type=          {{\tt http://http://www.cs.ualberta.ca/\char126piotr/Mizar/Doc/GL-thesis.ps}},
  year=          2004,
  note=          {M Sc thesis})
