Nalazite se na CroRIS probnoj okolini. Ovdje evidentirani podaci neće biti pohranjeni u Informacijskom sustavu znanosti RH. Ako je ovo greška, CroRIS produkcijskoj okolini moguće je pristupi putem poveznice www.croris.hr
izvor podataka: crosbi !

Formal System for Searching for the Shortest Proof Games using Coq (CROSBI ID 167700)

Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija

Maliković, Marko ; Čubrilo, Mirko Formal System for Searching for the Shortest Proof Games using Coq // International Review on Computers and Software, 5 (2010), 6; 746-756

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

Podaci o izdanju

5 (6)

2010.

746-756

objavljeno

1828-6003

Povezanost rada

Informacijske i komunikacijske znanosti

Indeksiranost