### Abstract

Binary multirelations associate elements of a set with its subsets; hence they are binary relations from a set to its power set. Applications include alternating automata, models and logics for games, program semantics with dual demonic and angelic nondeterministic choices and concurrent dynamic logics. This proof document supports an arXiv article that formalises the basic algebra of multirelations and proposes axiom systems for them, ranging from weak bi-monoids to weak bi-quantales.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Multirelations

- C_Algebras
- Multirelations

### Depends on

- Kleene Algebra

### Auto-related entries

- Transport via Partial Galois Connections and Equivalences
- Inner Structure, Determinism and Modal Algebra of Multirelations
- Kleene Algebras with Domain
- Relation Algebra

## Cite

×

Multirelations-AFP

    @article{Multirelations-AFP,
      author  = {Hitoshi Furusawa and Georg Struth},
      title   = {Binary Multirelations},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Multirelations.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
- Jun 13, 2015 : Isabelle2015