diff --git a/thys/Aggregation_Algebras/ROOT b/thys/Aggregation_Algebras/ROOT --- a/thys/Aggregation_Algebras/ROOT +++ b/thys/Aggregation_Algebras/ROOT @@ -1,15 +1,12 @@ chapter AFP session Aggregation_Algebras (AFP) = Stone_Kleene_Relation_Algebras + options [timeout = 600] theories Semigroups_Big Aggregation_Algebras Matrix_Aggregation_Algebras Linear_Aggregation_Algebras - Hoare_Logic - Hoare_Logic_Examples - Minimum_Spanning_Trees document_files "root.tex" - "root.bib" \ No newline at end of file + "root.bib" diff --git a/thys/Aggregation_Algebras/document/root.bib b/thys/Aggregation_Algebras/document/root.bib --- a/thys/Aggregation_Algebras/document/root.bib +++ b/thys/Aggregation_Algebras/document/root.bib @@ -1,56 +1,64 @@ @STRING{afp = {Archive of Formal Proofs}} @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}} @InProceedings{Guttmann2016c, 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 = {} } @InProceedings{Guttmann2017b, author = {Guttmann, W.}, title = {Stone Relation Algebras}, editor = {H{\"o}fner, P. and Pous, D. and Struth, G.}, booktitle = {Relational and Algebraic Methods in Computer Science}, publisher = sv, series = lncs, volume = 10226, pages = {127--143}, year = 2017, note = {} } @Article{Guttmann2017c, author = {Guttmann, W.}, title = {Stone-{Kleene} Relation Algebras}, journal = afp, year = 2017, note = {} } @Article{Guttmann2018a, author = {Guttmann, W.}, title = {An Algebraic Framework for Minimum Spanning Tree Problems}, journal = tcs, year = 2018, note = {\url{https://doi.org/10.1016/j.tcs.2018.04.012}} } @Article{Guttmann2018b, author = {Guttmann, W.}, title = {Verifying Minimum Spanning Tree Algorithms with {Stone} Relation Algebras}, journal = jlamp, year = 2018, note = {\url{https://doi.org/10.1016/j.jlamp.2018.09.005}} } +@Article{GuttmannRobinsonOBrien2020, + author = {Guttmann, W. and Robinson-O'Brien, N.}, + title = {Relational Minimum Spanning Tree Algorithms}, + journal = afp, + year = 2020, + note = {} +} + diff --git a/thys/Aggregation_Algebras/document/root.tex b/thys/Aggregation_Algebras/document/root.tex --- a/thys/Aggregation_Algebras/document/root.tex +++ b/thys/Aggregation_Algebras/document/root.tex @@ -1,51 +1,53 @@ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{amssymb,ragged2e} \usepackage{pdfsetup} \isabellestyle{it} \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}} \renewcommand\labelitemi{$*$} \begin{document} \title{Aggregation Algebras} \author{Walter Guttmann} \maketitle \begin{abstract} We develop algebras for aggregation and minimisation for weight matrices and for edge weights in graphs. - We verify the correctness of Prim's and Kruskal's minimum spanning tree algorithms based on these algebras. - We also show numerous instances of these algebras based on linearly ordered commutative semigroups. + We show numerous instances of these algebras based on linearly ordered commutative semigroups. \end{abstract} \tableofcontents \section{Overview} -This document describes the following seven theory files: +This document describes the following four theory files: \begin{itemize} \item Big sums over semigroups generalises parts of Isabelle/HOL's theory of finite summation \texttt{Groups\_Big.thy} from commutative monoids to commutative semigroups with a unit element only on the image of the semigroup operation. \item Aggregation Algebras introduces s-algebras, m-algebras and m-Kleene-algebras with operations for aggregating the elements of a weight matrix and finding the edge with minimal weight. \item Matrix Aggregation Algebras introduces aggregation orders, aggregation lattices and linear aggregation lattices. Matrices over these structures form s-algebras and m-algebras. \item Linear Aggregation Algebras shows numerous instances based on linearly ordered commutative semigroups. They include aggregations used for the minimum weight spanning tree problem and for the minimum bottleneck spanning tree problem, as well as arbitrary t-norms and t-conorms. -\item Hoare Logic is a light-weight modification of Isabelle/HOL's theory \texttt{Hoare/Hoare\_Logic.thy} for total-correctness proofs. -\item Hoare Logic Examples gives a few simple total-correctness proof examples. -\item Minimum Spanning Trees proves total correctness of Kruskal's and Prim's algorithms based on m-Kleene-algebras using Hoare logic. +\end{itemize} +Three theory files, which were originally part of this entry, have been moved elsewhere: +\begin{itemize} +\item A theory for total-correctness proofs in Hoare logic became part of Isabelle/HOL's theory \texttt{Hoare/Hoare\_Logic.thy}. +\item A theory with simple total-correctness proof examples became Isabelle/HOL's theory \texttt{Hoare/ExamplesTC.thy}. +\item A theory proving total correctness of Kruskal's and Prim's minimum spanning tree algorithms based on m-Kleene-algebras using Hoare logic was split into two theories that became part of AFP entry \cite{GuttmannRobinsonOBrien2020}. \end{itemize} The development is based on Stone-Kleene relation algebras \cite{Guttmann2017b,Guttmann2017c}. The algebras for aggregation and minimisation, their application to weighted graphs and the verification of Prim's and Kruskal's minimum spanning tree algorithms, and various instances of aggregation are described in \cite{Guttmann2016c,Guttmann2018a,Guttmann2018b}. Related work is discussed in these papers. \begin{flushleft} \input{session} \end{flushleft} \bibliographystyle{abbrv} \bibliography{root} \end{document}