[isabelle] New in the Archive of Formal Proofs
Many thanks to Georg Struth and Tjark Weber for this contribution!
Title: Relation Algebra
Entry name: Relation_Algebra
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and