Tree Decomposition

Christoph Dittmann 🌐

May 31, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Tree_Decomposition

Cite

× 
@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},
}
Download

Download

× Download latest

Older releases: