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.