## Relation Algebra

Alasdair Armstrong, Simon Foster, Georg Struth, and Tjark Weber. Archive of Formal Proofs, January 2014. Formal proof development.

### Abstract

Tarski's algebra of binary relations is formalised along the lines of the standard textbooks of Maddux and Schmidt and Ströhlein. This includes relation-algebraic concepts such as subidentities, vectors and a domain operation as well as various notions associated to functions. Relation algebras are also expanded by a reflexive transitive closure operation, and they are linked with Kleene algebras and models of binary relations and Boolean matrices.

### Download

The original publication is available at http://afp.sf.net/entries/Relation_Algebra.shtml.

### BibTeX

@article{armstrong13kleene,
author = {Alasdair Armstrong and Simon Foster and Georg Struth and Tjark Weber},
title = {Relation Algebra},
journal = {Archive of Formal Proofs},
month = jan,
year = {2014},
note = {\url{http://afp.sf.net/entries/Relation_Algebra.shtml}, Formal proof development}
}

Last modified: 2014-07-03