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 19:04):

From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Transitive-Closure-II.shtml

Executable Transitive Closures
René Thiemann

We provide a generic work-list algorithm to compute the
(reflexive-)transitive closure of relations where only successors of
newly detected states are generated. In contrast to our previous work,
the relations do not have to be finite, but each element must only have
finitely many (indirect) successors. Moreover, a subsumption relation
can be used instead of pure equality. An executable variant of the
algorithm is available where the generic operations are instantiated
with list operations. This formalization was performed as part of the
IsaFoR/CeTA project, and it has been used to certify size-change
termination proofs where large transitive closures have to be computed.

Enjoy!


Last updated: Mar 29 2024 at 04:18 UTC