Naslov
Formal System for Searching for the Shortest Proof Games using Coq

Autori
Maliković, Marko ; Čubrilo, Mirko

Izvornik
International Review on Computers and Software (1828-6003) 5 (2010), 6; 746-756

Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni

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

Sažetak
In this paper we propose a formal system for solving shortest proof games as one important genre of retrograde chess analysis. Shortest proof games serve to establish the legality of a position in chess problems by searching for the shortest sequence of moves that lead from initial to given chess position. For the establishment of such a system we use Coq – a computer tool for verifying theorem proofs in higher-order logic. 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), bundles of trajectories (sets of trajectories which all have the same starting and end square) and circular trajectories (trajectories whose starting and end square coincide). We show how these forms can be generated using Coq, how they can be used in order to solve an shortest proof game and how can it be concluded which of these forms should be generated in order to solve given problem.

Izvorni jezik
Engleski

Znanstvena područja
Informacijske i komunikacijske znanosti

POVEZANOST RADA