Solving Shortest Proof Games by Generating Trajectories using Coq Proof Management System (CROSBI ID 566344)
Prilog sa skupa u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Maliković, Marko ; Čubrilo, Mirko
engleski
Solving Shortest Proof Games by Generating Trajectories using Coq Proof Management System
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.
Retrograde chess analysis; Shortest proof games; Trajectories; Coq
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
11-18.
2010.
nije evidentirano
objavljeno
Podaci o matičnoj publikaciji
Central European conference on information and intelligent systems
Varaždin:
1847-2001
Podaci o skupu
21st Central European Conference on Information and Intelligent Systems
predavanje
22.09.2010-24.09.2010
Varaždin, Hrvatska