Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
11002451 | Journal of Logical and Algebraic Methods in Programming | 2018 | 24 Pages |
Abstract
We study a generalisation of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. Many theorems of relation algebras generalise with no or small changes. Weighted graphs represented as matrices over extended real numbers form an instance. Relational concepts and methods can thus be applied to weighted graphs. We formally specify the problem of computing minimum spanning forests and express Kruskal's algorithm in relation-algebraic terms. We give a total-correctness proof of the algorithm. All results are formally verified in Isabelle/HOL. This paper is an extended version of [40].
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Walter Guttmann,