### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms/Graph
- Mathematics/Graph theory
- Mathematics/Combinatorics

### Related publications

- Cremer, Nils. (2023). Verified Enumeration of Trees [Bachelor's Thesis, Technische Universität München]. mediaTUM. https://mediatum.ub.tum.de/1709010

### Session Tree_Enumeration

- Tree_Graph
- Labeled_Tree_Enumeration
- Rooted_Tree
- Rooted_Tree_Enumeration

### Depends on

- Undirected Graph Theory

## Cite

×

Tree_Enumeration-AFP

    @article{Tree_Enumeration-AFP,
      author  = {Nils Cremer},
      title   = {Tree Enumeration},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Tree_Enumeration.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- May 17, 2023 : Isabelle2022