[isabelle] new AFP entry: Binary Multirelations

Binary Multirelations
  by Hitoshi Furusawa and Georg Struth

  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:



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.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.