Pregled bibliografske jedinice broj: 856886
Formalization of a Strategy for the KRK Chess Endgame
Formalization of a Strategy for the KRK Chess Endgame // Central European Conference on Information and Intelligent Systems
Hrvatska, 2012. (poster, nije recenziran, sažetak, ostalo)
CROSBI ID: 856886 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Formalization of a Strategy for the KRK Chess Endgame
Autori
Maliković, Marko ; Čubrilo, Mirko ; Janičić, Predrag
Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, ostalo
Skup
Central European Conference on Information and Intelligent Systems
Mjesto i datum
Hrvatska, 19.09.2012. - 21.09.2012
Vrsta sudjelovanja
Poster
Vrsta recenzije
Nije recenziran
Ključne riječi
Interactive theorem proving, Coq, automated theorem proving, linear arithmetic, chess endgames, KRK chess endgame
Sažetak
Chess has always been a challenging subject for various computer analyses and methodologies, and they often brought more general advances in the related computer science fields, such as search strategies, AI planning, data-mining, etc. However, interactive theorem proving has hardly been applied to chess. In this paper we present our formalization, within the Coq proof assistant, of one fragment of the chess game - KRK chess ending and several conjectures relevant for this endgame. We show that most of the considered notions and conjectures can be expressed in a simple theory such as linear arithmetic. In addition, in this paper we present a formalization of Bratko's strategy for the KRK endgame. The presented formalization will serve as a key step towards formal correctness proof for Bratko's strategy
Izvorni jezik
Engleski
Znanstvena područja
Računarstvo, Informacijske i komunikacijske znanosti
