### Abstract

This development provides a formalization of undirected graphs and simple graphs, which are based on Benedikt Nordhoff and Peter Lammich's simple formalization of labelled directed graphs in the archive. Then, with our formalization of graphs, we show both necessary and sufficient conditions for Eulerian trails and circuits as well as the fact that the Königsberg Bridge Problem does not have a solution. In addition, we show the Friendship Theorem in simple graphs.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Koenigsberg_Friendship

- MoreGraph
- KoenigsbergBridge
- FriendshipTheory

### Depends on

- Dijkstra’s Shortest Path Algorithm

## Cite

×

Koenigsberg_Friendship-AFP

    @article{Koenigsberg_Friendship-AFP,
      author  = {Wenda Li},
      title   = {The Königsberg Bridge Problem and the Friendship Theorem},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Koenigsberg_Friendship.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Jul 26, 2013 : Isabelle2013