@MISC{GLIB_012.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {About Graph Complements},
  SECTION1 = {Loopfull Graphs},
  SECTION2 = {Adding Loops to a Graph},
  SECTION3 = {Directed Graph Complement with Loops},
  SECTION4 = {Undirected Graph Complement with Loops},
  SECTION5 = {Directed Graph Complement without Loops},
  SECTION6 = {Undirected Graph Complement without Loops},
  SECTION7 = {Self-complementary Graphs},
  DAY = {30},
  MONTH = {December},
  YEAR = {2019},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {This article formalizes different variants of the complement graph 
  in the Mizar system \cite{FourDecades}, based on the formalization of graphs in 
  \cite{GLIB_000.ABS}.},
  INTRODUCTION = {In the first section of this article, the property of a graph to be reflexive is   rigorously introduced. But since the irreflexive attribute was called \texttt{loopless} in 
  \cite{GLIB_000.ABS}, \texttt{loopfull} was chosen this time.\par
   The following section introduces a mode to add loops to a subset of the vertices of a graph. 
   It is shown that for a finite subset this operation can be done by adding a loop at a time 
  (cf. \cite{GLIB_008.ABS}). It is also shown that adding loops can preserve isomorphism between 
  graphs, if the subset of vertices of the second graph the loops are added to is the image 
  under an isomorphism of the subset of vertices of the first graphs the loops are added 
  to.\par
  The next four sections formalize the directed complement with loops, the undirected complement 
  with loops, the directed complement without loops and the undirected complement without 
  loops, respectively. Given a simple undirected graph, its complement is usually defined on 
  the same vertex set; two different vertices being adjacent iff they weren't adjacent in the 
  original graph \cite{GERWAG,GERDIE,MULTI}. A similar definition can be given for simple 
  digraphs \cite{MULTI}. The loop variants are introduced on the base of similarity between 
  graphs and relations. In contrast to the literature the definitions formalized allow 
  to take the complement of any graphs, with parallel edges simply being ignored. 
  So any complement of a graph is also a complement of that graph with its parallel 
  edges removed. Furthermore on a technical note, the vertex sets of the graph and its 
  complement are required to be the same, while the edge sets have to be disjoint. 
  This choice was made to ensure the union of a graph and its complement would be complete 
  and its intersection edgeless. Since the edge set of the complement graph is otherwise 
  unspecified, for each complement type all possible complements of a graph are only isomorphic 
  to each other. Other theorems include:
  \begin{itemize}
    \item Involutiveness of the graph complement: 
    If a graph is of the right type (e.g. simple for undirected complement without loops), 
    then it is the complement of its complement.
    \item The complement of an edgeless graph is complete.
    \item The undirected complement without loops of a complete graph is edgeless.
    \item The complement of an unconnected graph is connected.
    \item The neighbors of a vertex in a complement without loops of 
    a graph is the complement of the neighbors in the original graph.
    \item If a graph has order at least $3$, no vertex can be an endvertex in 
    both that graph and its directed complement without loops 
   ($K_2$ as its own complement with its edge seen as directed is the exception here.)
    \item If a graph has order at least $4$, no vertex can be an endvertex in both 
  that graph and its undirected complement without loops 
  ($P_3$ with its complement $K_2+K_1$ is the exception here.)
  \end{itemize}\par
  The last section briefly introduces the property of a graph to be self-complementary, 
  for all four variants, but without going into depth. However, it is shown that these 
  four variants are mutually exclusive, except for $K_1$ which is self-complementary with 
  respect to the directed or undirected complement, without loops in both cases.}}

@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{GERWAG,
  title = {Graphentheorie},
  series = {B.I-Hochschultaschenbücher ; 248},
  author = {Wagner, Klaus},
  address = {Mannheim [u.a.]},
  publisher = {Bibliograph. Inst.},
  year = {1970},
  ISBN = {3-411-00248-4},
  pages = {220 S.}
}
@book{GERDIE,
  title = {Graphentheorie},
  author = {Diestel, Reinhard},
  address = {Heidelberg [u.a.]},
  publisher = {Springer},
  year = {2012},
  edition = {4. Aufl., erster, korr. Nachdr.},
  ISBN = {978-3-642-14911-5},
}
@book{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate texts in mathematics ; 244},
  AUTHOR = {Bondy, John Adrian ; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ; 
   http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; 
  http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}