Relation Algebra

 

Title: Relation Algebra
Authors: Alasdair Armstrong, Simon Foster (simon /dot/ foster /at/ york /dot/ ac /dot/ uk), 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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Kleene_Algebra
Used by: Residuated_Lattices