Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP: The Königsberg Bridge Problem and the Fri...


view this post on Zulip Email Gateway (Aug 19 2022 at 11:22):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The following new entry is now available in the AFP:

The Königsberg Bridge Problem and the Friendship Theorem
by Wenda Li

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.

[http://afp.sourceforge.net/entries/Koenigsberg_Friendship.shtml]

Cheers,
Gerwin


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


Last updated: Apr 26 2024 at 12:28 UTC