Napredna pretraga

Pregled bibliografske jedinice broj: 594346

Formalization of a Strategy for the KRK Chess Endgame


Maliković, Marko; Čubrilo, Mirko; Janičić, Predrag
Formalization of a Strategy for the KRK Chess Endgame // Proceedings of 23st Central European Conference on Information and Intelligent Systems
Varaždin, 2012. str. 29-36 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


Naslov
Formalization of a Strategy for the KRK Chess Endgame

Autori
Maliković, Marko ; Čubrilo, Mirko ; Janičić, Predrag

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

Izvornik
Proceedings of 23st Central European Conference on Information and Intelligent Systems / - Varaždin, 2012, 29-36

Skup
Central European Conference on Information and Intelligent Systems

Mjesto i datum
Varaždin, Hrvatska, 19-21.09.2012

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

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
Informacijske i komunikacijske znanosti



POVEZANOST RADA


Projekt / tema
016-0161741-1739 - Razvoj informacijske infrastrukture i deduktivnih mehanizama Semantičkog Weba (Mirko Čubrilo, )

Ustanove
Filozofski fakultet, Rijeka,
Fakultet organizacije i informatike, Varaždin