### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Knights_Tour

- KnightsTour

## Cite

×

Knights_Tour-AFP

    @article{Knights_Tour-AFP,
      author  = {Lukas Koller},
      title   = {Knight's Tour Revisited Revisited},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Knights_Tour.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jan 6, 2022 : Isabelle2021-1
- Jan 4, 2022 : Isabelle2021-1