| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
The Königsberg Bridge Problem and the Friendship Theorem
| Title: | The Königsberg Bridge Problem and the Friendship Theorem |
| Author: | Wenda Li |
| Submission date: | 2013-07-19 |
| 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. |
| BibTeX: |
@article{Koenigsberg_Friendship-AFP,
author = {Wenda Li},
title = {The Königsberg Bridge Problem and the Friendship Theorem},
journal = {Archive of Formal Proofs},
month = jul,
year = 2013,
note = {\url{http://isa-afp.org/entries/Koenigsberg_Friendship.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Dijkstra_Shortest_Path |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |