Depth First Search

 

Title:	Depth First Search
Author:	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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Depth-First-Search-2009-04-29.tar.gz Isabelle 2008: afp-Depth-First-Search-2008-06-10.tar.gz Isabelle 2007: afp-Depth-First-Search-2007-11-27.tar.gz Isabelle 2005: afp-Depth-First-Search-2005-10-14.tar.gz Isabelle 2004: afp-Depth-First-Search-2004-06-24.tar.gz