Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Executable Transitive Closures ...


view this post on Zulip Email Gateway (Aug 18 2022 at 17:21):

From: Tobias Nipkow <nipkow@in.tum.de>
Executable Transitive Closures of Finite Relations
Christian Sternagel and René Thiemann

We provide a generic work-list algorithm to compute the transitive
closure of finite relations where only successors of newly detected
states are generated. This algorithm is then instantiated for lists over
arbitrary carriers and red black trees (which are faster but require a
linear order on the carrier), respectively. Our formalization was
performed as part of the IsaFoR/CeTA project where reflexive transitive
closures of large tree automata have to be computed.

http://afp.sourceforge.net/entries/Transitive-Closure.shtml


Last updated: Apr 19 2024 at 12:27 UTC