Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Knight's Tour Revisited Revisited


view this post on Zulip Email Gateway (Jan 04 2022 at 17:33):

From: Tobias Nipkow <nipkow@in.tum.de>
Knight's Tour Revisited Revisited
Lukas Koller

This is a formalization of the article "Knight's Tour Revisited" by Cull and De
Curtins where they prove the existence of a Knight's path for arbitrary n ×
m-boards with min(n,m) ≤ 5. If n · m is even, then there exists a Knight's
circuit. A Knight's Path is a sequence of moves of a Knight on a chessboard s.t.
the Knight visits every square of a chessboard exactly once. Finding a Knight's
path is a an instance of the Hamiltonian path problem. A Knight's circuit is a
Knight's path, where additionally the Knight can move from the last square to
the first square of the path, forming a loop. During the formalization two
mistakes in the original proof were discovered. These mistakes are corrected in
this formalization.

https://www.isa-afp.org/entries/Knights_Tour.html

Happy New Year!
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC