Naslov
A formal system for automated reasoning about retrograde chess problems using Coq

Autori
Maliković, Marko

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

Izvornik
Proceedings of 19th Central European Conference on Information and Intelligent Systems / - Varaždin, 2008, 465-475

ISBN
978-953-6071-04-3

Skup
19th Central European Conference on Information and Intelligent Systems

Mjesto i datum
Varaždin, Hrvatska, 24.09.2008. - 26.09.2008

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
retrograde chess analysis; formal system; Coq; automated reasoning

Sažetak
This paper presents a formal system for automated reasoning about retrograde chess problems using Coq – a formal proof management system. The system is divided into two parts. The first part describes the environment that includes the axioms, definitions and hypotheses of chess objects, and also the functions for computing changes in states. The second part is developed for generating possible retrograde chess moves and includes Coq’ s tactics combined with the use of tacticals (elements of Ltac - the Coq’ s language for combining tactics). All of these tactics are defined as one Ltac function. This approach enables reasoning about retrograde chess problems with respect to reasoning about sequences of retrograde moves. In the aforementioned Ltac function, a number of heuristic solutions are implemented with the aim of solving the problems within a big search space such as retrograde chess analysis. These heuristics, as well as tactics and tacticals, are not the subject of this article.

Izvorni jezik
Engleski

Znanstvena područja
Informacijske i komunikacijske znanosti

Napomena
(Indexed in CSA database)

POVEZANOST RADA