Abstract
We present a formalization of flow networks and the Min-Cut-Max-Flow
theorem. Our formal proof closely follows a standard textbook proof,
and is accessible even without being an expert in Isabelle/HOL, the
interactive theorem prover used for the formalization.
License
Topics
Session Flow_Networks
- Fofu_Abs_Base
- Fofu_Impl_Base
- Refine_Add_Fofu
- Graph
- Network
- Residual_Graph
- Augmenting_Flow
- Augmenting_Path
- Ford_Fulkerson
- Graph_Impl
- Network_Impl
- NetCheck