Formalization of a Strategy for the KRK Chess Endgame (CROSBI ID 644159)
Prilog sa skupa u zborniku | sažetak izlaganja sa skupa
Podaci o odgovornosti
Maliković, Marko ; Čubrilo, Mirko ; Janičić, Predrag
engleski
Formalization of a Strategy for the KRK Chess Endgame
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
Interactive theorem proving, Coq, automated theorem proving, linear arithmetic, chess endgames, KRK chess endgame
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
2012.
objavljeno
Podaci o matičnoj publikaciji
Podaci o skupu
Central European Conference on Information and Intelligent Systems
poster
19.09.2012-21.09.2012
Hrvatska