Walter Guttmann, Georg Struth, and Tjark Weber. In Peter Höfner, Annabelle McIver, and Georg Struth, editors, Proceedings of the First Workshop on Automated Theory Engineering, volume 760 of CEUR Workshop Proceedings, pages 30-39, July 2011.
We have implemented a repository of algebraic structures and theorems in the theorem proving environment Isabelle/HOL. It covers variants of Kleene algebras and relation algebras with many of their models. Most theorems have been obtained by automated theorem proving within Isabelle. Main purposes of the repository are the engineering of algebraic theories for computing systems and their application in formal program development. This paper describes the present state of the repository, illustrates its potential by a theory engineering and a program verification example, and discusses the most important directions for future work.
@inproceedings{guttmann11repository,
author = {Walter Guttmann and Georg Struth and Tjark Weber},
title = {A Repository for {Tarski}-{Kleene} Algebras},
editor = {Peter H{\"o}fner and Annabelle McIver and Georg Struth},
booktitle = {Proceedings of the First Workshop on Automated Theory Engineering},
volume = {760},
series = {CEUR Workshop Proceedings},
pages = {30--39},
month = jul,
year = {2011},
issn = {1613-0073},
url = {http://ceur-ws.org/Vol-760/paper5.pdf}
}