Relation Algebra

Title:	Relation Algebra
Authors:	Alasdair Armstrong, Simon Foster, Georg Struth and Tjark Weber (tjark /dot/ weber /at/ it /dot/ uu /dot/ se)
Submission date:	2014-01-25
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.
BibTeX:	@article{Relation_Algebra-AFP, 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://isa-afp.org/entries/Relation_Algebra.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Kleene_Algebra
Used by:	Relational_Paths, Residuated_Lattices
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.