Email Gateway (May 17 2023 at 09:21): Email Gateway (May 17 2023 at 09:21):From: Tobias Nipkow <nipkow@in.tum.de>
Tree Enumeration
Nils Cremer
This thesis presents the verification of enumeration algorithms for trees. The
first algorithm is based on the well known Prüfer-correspondence and allows the
enumeration of all possible labeled trees over a fixed finite set of vertices.
The second algorithm enumerates rooted, unlabeled trees of a specified size up
to graph isomorphism. It allows for the efficient enumeration without the use of
an intermediate encoding of the trees with level sequences, unlike the algorithm
by Beyer and Hedetniemi it is based on. Both algorithms are formalized and
verified in Isabelle/HOL. The formalization of trees and other graph theoretic
results is also presented.
https://www.isa-afp.org/entries/Tree_Enumeration.html
Enjoy!
Email Gateway (May 17 2023 at 11:37):From: Tobias Nipkow <nipkow@in.tum.de>
Tree Enumeration
Nils Cremer
This thesis presents the verification of enumeration algorithms for trees. The
first algorithm is based on the well known Prüfer-correspondence and allows the
enumeration of all possible labeled trees over a fixed finite set of vertices.
The second algorithm enumerates rooted, unlabeled trees of a specified size up
to graph isomorphism. It allows for the efficient enumeration without the use of
an intermediate encoding of the trees with level sequences, unlike the algorithm
by Beyer and Hedetniemi it is based on. Both algorithms are formalized and
verified in Isabelle/HOL. The formalization of trees and other graph theoretic
results is also presented.
https://www.isa-afp.org/entries/Tree_Enumeration.html
Enjoy!
Last updated: Oct 31 2025 at 12:44 UTC