| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Binary Multirelations
| Title: | Binary Multirelations |
| Authors: | Hitoshi Furusawa and Georg Struth |
| Submission date: | 2015-06-11 |
| 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. |
| BibTeX: |
@article{Multirelations-AFP,
author = {Hitoshi Furusawa and Georg Struth},
title = {Binary Multirelations},
journal = {Archive of Formal Proofs},
month = jun,
year = 2015,
note = {\url{http://isa-afp.org/entries/Multirelations.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Kleene_Algebra |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|