# Tree Decomposition

 Title: Tree Decomposition Author: Christoph Dittmann Submission date: 2016-05-31 Abstract: We formalize tree decompositions and tree width in Isabelle/HOL, proving that trees have treewidth 1. We also show that every edge of a tree decomposition is a separation of the underlying graph. As an application of this theorem we prove that complete graphs of size n have treewidth n-1. BibTeX: @article{Tree_Decomposition-AFP, author = {Christoph Dittmann}, title = {Tree Decomposition}, journal = {Archive of Formal Proofs}, month = may, year = 2016, note = {\url{https://isa-afp.org/entries/Tree_Decomposition.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License