
@article{noschinski_2015,
	title = {A {Graph} {Library} for {Isabelle}},
	volume = {9},
	issn = {1661-8270, 1661-8289},
	doi = {10.1007/s11786-014-0183-z},
	abstract = {In contrast to other areas of mathematics such as calculus, number theory or probability theory, there is currently no standard library for graph theory for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general inﬁnite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs. We use this library to formalize a characterization of Euler Digraphs and to verify a method of checking Kuratowski subgraphs used in the LEDA library.},
	language = {en},
	number = {1},
	urldate = {2020-03-10},
	journal = {Mathematics in Computer Science},
	author = {Noschinski, Lars},
	month = mar,
	year = {2015},
	note = {http://link.springer.com/10.1007/s11786-014-0183-z},
	pages = {23--39},
	annote = {Intended to be a general graph theory library.
Focuses on enabling automation
Formalises directed graphs allowing for loops and parallel arcs.
Gives definitions for basic concepts such as connectedness, walks, trails, etc. Also basic operations such as modifications on a graph etc.
Applies to computational proof of an algorithm for planar properties and more traditional graph theorey proof: existence of a euler trail.},
	file = {Noschinski - 2015 - A Graph Library for Isabelle.pdf:C\:\\Users\\cledm\\Zotero\\storage\\M8WUA7CC\\Noschinski - 2015 - A Graph Library for Isabelle.pdf:application/pdf;Noschinski_2015_A Graph Library for Isabelle.pdf:C\:\\Users\\cledm\\Zotero\\storage\\W2HDXP6B\\Noschinski_2015_A Graph Library for Isabelle.pdf:application/pdf},
}

@inproceedings{noschinski_2012,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Proof {Pearl}: {A} {Probabilistic} {Proof} for the {Girth}-{Chromatic} {Number} {Theorem}},
	volume = {7406},
	url = {https://link-springer-com.ezp.lib.cam.ac.uk/chapter/10.1007/978-3-642-32347-8_27},
	urldate = {2020-06-15},
	booktitle = {Interactive {Theorem} {Proving}. {ITP} 2012.},
	publisher = {Springer Berlin Heidelberg},
	author = {Noschinski, Lars},
	year = {2012},
	file = {Proof Pearl\: A Probabilistic Proof for the Girth-Chromatic Number Theorem | SpringerLink:C\:\\Users\\cledm\\Zotero\\storage\\E7ZHIM6P\\978-3-642-32347-8_27.html:text/html},
}

@article{edmonds_roths,
	title = {Roth's {Theorem} on {Arithmetic} {Progressions}},
	issn = {2150-914x},
	journal = {Archive of Formal Proofs},
	author = {Edmonds, Chelsea and Koutsoukou-Argyraki, Angeliki and Paulson, Lawrence C.},
	month = dec,
	year = {2021},
	annote = {https://isa-afp.org/entries/Roth\_Arithmetic\_Progressions.html, Formal proof development},
}

@article{edmonds_szemeredis,
	title = {Szemerédi's {Regularity} {Lemma}},
	issn = {2150-914x},
	journal = {Archive of Formal Proofs},
	author = {Edmonds, Chelsea and Koutsoukou-Argyraki, Angeliki and Paulson, Lawrence C.},
	month = nov,
	year = {2021},
	annote = {https://isa-afp.org/entries/Szemeredi\_Regularity.html, Formal proof development},
}

@article{Hupel_Random,
  author  = {Lars Hupel},
  title   = {Properties of Random Graphs -- Subgraph Containment},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Random_Graph_Subgraph_Threshold.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
