Naslov
Solving Shortest Proof Games by Generating Trajectories using Coq Proof Management System

Autori
Maliković, Marko ; Čubrilo, Mirko

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of 21st Central European Conference on Information and Intelligent Systems, 2010 / - Varaždin, 2010, 11-18

Skup
21st Central European Conference on Information and Intelligent Systems

Mjesto i datum
Varaždin, Hrvatska, 22.09.2010. - 24.09.2010

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Retrograde chess analysis; Shortest proof games; Trajectories; Coq

Sažetak
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. First we give an overview of existing computer programs for solving SPG's, but due to the absence of any research 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 shortest trajectories (shortest planning paths which certain pieces might follow from initial square to achieve the target square), admissible trajectories (trajectories longer than the shortest trajectory) and bundles of trajectories. We show how these forms can be recursively generated using Coq and how they can be used in order to solve an SPG.

Izvorni jezik
Engleski

Znanstvena područja
Informacijske i komunikacijske znanosti

POVEZANOST RADA