Font Size: 

Various analyses of chess endgames are made with different purposes. These analyzes are usually based on exhaustive analysis using previous generated corresponding databases. It is often not investigated whether the endgame positions are legal (or why are not legal). Legality of endgame positions can be proven in several ways, and in this paper we present one of them: high-level computer-assisted proof based on reduction to propositional logic, more precisely to SAT. As case study we focus on a King and Rook vs. King endgame, and reduction to SAT is performed by using a constraint solving system URSA. We are not aware of other computer-assisted high-level proof of a legality of some chess endgame. The presented methodology can be applied to other chess endgames. Therefore, the point of this paper is not only presenting a proof of legality of an endgame, but also presenting a new methodology for computer-assisted proving of legality of chess endgames in general.