## Formalization of graph theory in HOL: the Maxflow-Mincut theorem

### Niccolò Veltri

Dip. di Matematica "Ulisse Dini"

Università di Firenze

Wednesday, 12 September 2012, 14:00 (note the unusual weekday)

Cybernetica Bldg (Akadeemia tee 21), room B126 (note the unusual room)

Slides from the talk [pdf]

**Abstract**: In my Master's degree thesis I created the
foundation for the development of a library about graphs in the
theorem prover HOL Light of the family of provers Isabelle/HOL. The
library would contain lots of basic and advanced graph theoretical
theorems, as well as algorithms concerning graphs in the vein of other
well-known libraries on graphs like ocamlgraph or The Stanford
GraphBase. In particular during the development of the library I
formalized the famous Maxflow-Mincut theorem that exhibit how to
construct a flow with maximal value for a network. That turned out to
be the most difficult task that I faced in the construction of the
library and for this reason in this seminar speech I would like to
show my personal formalization in higher order logic of this important
theorem.

N. Veltri's visit is funded by ETAG (ETF) grant 9475.

Tarmo Uustalu

Last update 15.9.2012