Skip to Content

Graph Saturation

An Isabelle/HOL Formalisation of Graph Saturation

Here you can download the Graph Saturation formalization. After installing Isabelle, you can simply open the .thy files to inspect them. To build the formalization and generate a proof document (which you may want to do to check that ‘quick and dirty mode’ is not used), you can type:

    isabelle build -c -d . -v Graph-Saturation