@MISC{LEXBFS.MIZ,
  AUTHOR = {Arneson, Broderick and Rudnicki, Piotr},
  TITLE = {Recognizing Chordal Graphs:
   Lex {BFS} and {MCS}},
  NOTE = {This work has been partially supported by the NSERC grant OGP 9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Miscellany on Graphs},
  SECTION3 = {Graphs with Two Vertex Labels},
  SECTION4 = {More on Graph Sequences},
  SECTION5 = {Vertices Numbering Sequences},
  SECTION6 = {Lexicographical Breadth-First Search},
  SECTION7 = {The Maximum Cardinality Search Algorithm},
  DAY = {17},
  MONTH = {November},
  YEAR = {2006},
  ADDRESS1 = {University of Alberta\\Edmonton, Canada},
  ADDRESS2 = {University of Alberta\\Edmonton, Canada},
  SUMMARY = {We are formalizing the algorithm for recognizing
  chordal graphs by lexicographic breadth-first search
  as presented in \cite[Section 3 of Chapter 4, pp.~81--84]{Golumbic}.
  Then we follow with a formalization of another algorithm
  serving the same end but based on maximum cardinality
  search as presented by Tarjan and Yannakakis~\cite{TY84}.\par
  This work is a part of the MSc work of the first author
  under supervision of the second author.
  We would like to thank one of the anonymous reviewers
  for very useful suggestions.}}

