Commit 299d80d0 authored by nipkow's avatar nipkow
Browse files

New entry: Relational_Minimum_Spanning_Trees

parent caaedd506d3d
......@@ -9953,3 +9953,14 @@ abstract =
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
title = Relational Minimum Spanning Tree Algorithms
author = Walter Guttmann <>, Nicolas Robinson-O'Brien<>
topic = Computer science/Algorithms/Graph
date = 2020-12-08
notify =
abstract =
We verify the correctness of Prim's, Kruskal's and
Borůvka's minimum spanning tree algorithms based on algebras for
aggregation and minimisation.
......@@ -446,6 +446,7 @@ Relation_Algebra
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
chapter AFP
session Relational_Minimum_Spanning_Trees (AFP) = Aggregation_Algebras +
options [timeout = 600]
@STRING{afp = {Archive of Formal Proofs}}
@STRING{dm = {Discrete Mathematics}}
@STRING{jlamp = {Journal of Logical and Algebraic Methods in Programming}}
@STRING{lncs = {Lecture Notes in Computer Science}}
@STRING{sv = {Springer}}
@STRING{tcs = {Theoretical Computer Science}}
author = {Bor\r{u}vka, O.},
title = {O jist{\'e}m probl{\'e}mu minim{\'a}ln{\'i}m},
journal = {Pr{\'a}ce moravsk{\'e} p{\v{r}}{\'i}rodo\-v{\v{e}}deck{\'e} spole{\v{c}}nosti},
volume = 3,
number = 3,
pages = {37--58},
year = 1926,
note = {}
author = {Graham, R. L. and Hell, P.},
title = {On the History of the Minimum Spanning Tree Problem},
journal = {Annals of the History of Computing},
volume = 7,
number = 1,
pages = {43--57},
year = 1985,
note = {}
author = {Guttmann, W.},
title = {Relation-Algebraic Verification of {Prim's} Minimum Spanning Tree Algorithm},
editor = {Sampaio, A. and Wang, F.},
booktitle = {Theoretical Aspects of Computing -- ICTAC 2016},
publisher = sv,
series = lncs,
volume = 9965,
pages = {51--68},
year = 2016,
note = {}
author = {Guttmann, W.},
title = {Aggregation Algebras},
journal = afp,
year = 2018,
note = {}
author = {Guttmann, W.},
title = {An Algebraic Framework for Minimum Spanning Tree Problems},
journal = tcs,
volume = 744,
pages = {37--55},
year = 2018,
note = {}
author = {Guttmann, W.},
title = {Verifying Minimum Spanning Tree Algorithms with {Stone} Relation Algebras},
journal = jlamp,
volume = 101,
pages = {132--150},
year = 2018,
note = {}
author = {Ne{\v{s}}et{\v{r}}il, J. and Milkov{\'a}, E. and Ne{\v{s}}et{\v{r}}ilov{\'a}, H.},
title = {Otakar {Bor\r{u}vka} on minimum spanning tree problem -- {Translation} of both the 1926 papers, comments, history},
journal = dm,
volume = 233,
number = {1--3},
pages = {3--36},
year = 2001,
note = {}
author = {Robinson-O'Brien, N.},
title = {A formal correctness proof of {Bor\r{u}vka's} minimum spanning tree algorithm},
school = {University of Canterbury},
year = 2020,
note = {\url{}}
\title{Relational Minimum Spanning Tree Algorithms}
\author{Walter Guttmann and Nicolas Robinson-O'Brien}
We verify the correctness of Prim's, Kruskal's and Bor\r{u}vka's minimum spanning tree algorithms based on algebras for aggregation and minimisation.
The theories described in this document prove the correctness of Prim's, Kruskal's and Bor\r{u}vka's minimum spanning tree algorithms.
Specifications and algorithms work in Stone-Kleene relation algebras extended by operations for aggregation and minimisation.
The algorithms are implemented in a simple imperative language and their proof uses Hoare logic.
The correctness proofs are discussed in \cite{Guttmann2016c,Guttmann2018b,Guttmann2018c,RobinsonOBrien2020}.
\subsection{Prim's and Kruskal's minimum spanning tree algorithms}
A framework based on Stone relation algebras and Kleene algebras and extended by operations for aggregation and minimisation was presented by the first author in \cite{Guttmann2016c,Guttmann2018b} and used to formally verify the correctness of Prim's minimum spanning tree algorithm.
It was extended in \cite{Guttmann2018c} and applied to prove the correctness of Kruskal's minimum spanning tree algorithm.
Two theories, one each for Prim's and Kruskal's algorithms, prove total correctness of these algorithms.
As case studies for the algebraic framework, these two theories combined were originally part of another AFP entry \cite{Guttmann2018a}.
\subsection{Bor\r{u}vka's minimum spanning tree algorithm}
Otakar Bor\r{u}vka formalised the minimum spanning tree problem and proposed a solution to it \cite{Boruvka1926}.
Bor\r{u}vka's original paper is written in Czech; translations of varying completeness can be found in \cite{GrahamHell1985,NesetrilMilkovaNesetrilova2001}.
The theory for Bor\r{u}vka's minimum spanning tree algorithm proves partial correctness of this algorithm.
This work is based on the same algebraic framework as the proof of Kruskal's algorithm; in particular it uses many theories from the hierarchy underlying \cite{Guttmann2018a}.
The theory for Bor\r{u}vka's algorithm formally verifies results from the second author's Master's thesis \cite{RobinsonOBrien2020}.
Certain lemmas in this theory are numbered for easy correlation to theorems from the thesis.
......@@ -139,7 +139,7 @@ based on linearly ordered commutative semigroups.</td>
<td class="data"><a href="Stone_Kleene_Relation_Algebras.html">Stone_Kleene_Relation_Algebras</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Relational_Disjoint_Set_Forests.html">Relational_Disjoint_Set_Forests</a>, <a href="Relational_Paths.html">Relational_Paths</a> </td></tr>
<td class="data"><a href="Relational_Disjoint_Set_Forests.html">Relational_Disjoint_Set_Forests</a>, <a href="Relational_Minimum_Spanning_Trees.html">Relational_Minimum_Spanning_Trees</a>, <a href="Relational_Paths.html">Relational_Paths</a> </td></tr>
......@@ -141,7 +141,9 @@ operation and a find operation with path compression.</td>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Aggregation_Algebras.html">Aggregation_Algebras</a>, <a href="Stone_Kleene_Relation_Algebras.html">Stone_Kleene_Relation_Algebras</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Relational_Minimum_Spanning_Trees.html">Relational_Minimum_Spanning_Trees</a> </td></tr>
This diff is collapsed.
......@@ -88,6 +88,15 @@ of a scientific journal, is indexed by <a href="
<td class="head">2020</td>
<td class="entry">
2020-12-08: <a href="entries/Relational_Minimum_Spanning_Trees.html">Relational Minimum Spanning Tree Algorithms</a>
<a href="">Walter Guttmann</a>
and Nicolas Robinson-O'Brien
<td class="entry">
2020-12-05: <a href="entries/Relational_Method.html">The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols</a>
......@@ -9,7 +9,18 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
<pubDate>05 Dec 2020 00:00:00 +0000</pubDate>
<pubDate>08 Dec 2020 00:00:00 +0000</pubDate>
<title>Relational Minimum Spanning Tree Algorithms</title>
<dc:creator> Walter Guttmann, Nicolas Robinson-O'Brien </dc:creator>
<pubDate>08 Dec 2020 00:00:00 +0000</pubDate>
We verify the correctness of Prim&#39;s, Kruskal&#39;s and
Borůvka&#39;s minimum spanning tree algorithms based on algebras for
aggregation and minimisation.</description>
<title>The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols</title>
......@@ -578,19 +589,5 @@ with $a_n &gt;1$ for all large n. The results are due to P. Erdős and E. G. Str
In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1.
The latter is an application of Theorem 2.1 involving the prime numbers.</description>
<title>Recursion Theorem in ZF</title>
<dc:creator> Georgy Dunaev </dc:creator>
<pubDate>11 May 2020 00:00:00 +0000</pubDate>
This document contains a proof of the recursion theorem. This is a
mechanization of the proof of the recursion theorem from the text &lt;i&gt;Introduction to
Set Theory&lt;/i&gt;, by Karel Hrbacek and Thomas Jech. This
implementation may be used as the basis for a model of Peano arithmetic in
ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development
is much easier to follow.</description>
This diff is collapsed.
......@@ -171,6 +171,7 @@
<a href="entries/Gabow_SCC.html">Gabow_SCC</a> &nbsp;
<a href="entries/Kruskal.html">Kruskal</a> &nbsp;
<a href="entries/Prim_Dijkstra_Simple.html">Prim_Dijkstra_Simple</a> &nbsp;
<a href="entries/Relational_Minimum_Spanning_Trees.html">Relational_Minimum_Spanning_Trees</a> &nbsp;
<a href="entries/DiskPaxos.html">DiskPaxos</a> &nbsp;
<a href="entries/GenClock.html">GenClock</a> &nbsp;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment