Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Binary Multirelations


view this post on Zulip Email Gateway (Aug 22 2022 at 10:12):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Binary Multirelations
by Hitoshi Furusawa and Georg Struth

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.

Available at:
http://afp.sourceforge.net/entries/Multirelations.shtml

Enjoy!
Gerwin


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


Last updated: Apr 24 2024 at 08:20 UTC