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: Jan 04 2025 at 20:18 UTC