Font Size: 

In this paper we focus on Shortest Proof Games (SPG) as one important genre of retrograde chess analysis. SPG's serve to establish the legality of a position in given chess problems by searching for the shortest sequence of moves that lead to the initial chess position. We give an overview of existing computer programs for solving SPG's, but due to the absence of any scientific papers on the topic, we provide informal descriptions obtained by the authors via e-mail and from partial information from programs' Web sites. In the second part of the paper we propose some systematic ideas for the establishment of a formal system for solving SPG's by using Coq - a formal proof management system. Our approach is based on the language of shortest trajectories (shortest planning paths which certain pieces might follow from initial point to achieve the target point), on admissible trajectories (trajectories which are longer than the shortest trajectory) and bundles of trajectories. We show how these forms can be recursively generated using Coq and how impossible trajectories can be eliminated in order to solve an SPG. Our opinion is that the approach used in this paper can be applied to a wide spectrum of other complex practical problems.