Formal System for Searching for the Shortest Proof Games using Coq (CROSBI ID 167700)
Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Maliković, Marko ; Čubrilo, Mirko
engleski
Formal System for Searching for the Shortest Proof Games using Coq
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.
Retrograde chess analysis; Shortest proof games; Trajectories; Coq
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano