# Depth First Search

 Title: Depth First Search Authors: Toshiaki Nishihara and Yasuhiko Minamide Submission date: 2004-06-24 Abstract: Depth-first search of a graph is formalized with recdef. It is shown that it visits all of the reachable nodes from a given list of nodes. Executable ML code of depth-first search is obtained using the code generation feature of Isabelle/HOL. BibTeX: @article{Depth-First-Search-AFP, author = {Toshiaki Nishihara and Yasuhiko Minamide}, title = {Depth First Search}, journal = {Archive of Formal Proofs}, month = jun, year = 2004, note = {\url{https://isa-afp.org/entries/Depth-First-Search.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License