Name
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]. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1016/j.jlamp.2018.09.005 | Journal of Logical and Algebraic Methods in Programming |
Keywords | Field | DocType |
Formal methods,Kleene algebras,Relation algebras,Stone algebras,Total correctness,Weighted graphs | HOL,Discrete mathematics,Extended real number line,Stone algebra,Generalization,Matrix (mathematics),Algorithm,Boolean algebra,Mathematics,Kruskal's algorithm,Minimum spanning tree | Journal |
Volume | Issue | ISSN |
101 | 1 | 2352-2208 |
Citations | PageRank | References |
1 | 0.35 | 16 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Walter Guttmann | 1 | 196 | 16.53 |