### 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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Relation_Algebra

- More_Boolean_Algebra
- Relation_Algebra
- Relation_Algebra_Vectors
- Relation_Algebra_Tests
- Relation_Algebra_Functions
- Relation_Algebra_Direct_Products
- Relation_Algebra_RTC
- Relation_Algebra_Models

### Depends on

- Kleene Algebra

### Used by

- Catoids, Categories, Groupoids
- Relational Characterisations of Paths
- Residuated Lattices

### Auto-related entries

- Transport via Partial Galois Connections and Equivalences
- Kleene Algebras with Domain
- Binary Multirelations

## Cite

×

Relation_Algebra-AFP

    @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   = {January},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Relation_Algebra.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jan 31, 2014 : Isabelle2013-2
- Jan 25, 2014 : Isabelle2013-2