Formalization of a Strategy for the KRK Chess Endgame (CROSBI ID 589752)
Prilog sa skupa u časopisu | izvorni znanstveni rad | međunarodna recenzija
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
29-36.
2012.
nije evidentirano
objavljeno
Podaci o matičnoj publikaciji
Central European conference on information and intelligent systems
Varaždin:
1847-2001
Podaci o skupu
Central European Conference on Information and Intelligent Systems
predavanje
19.09.2012-21.09.2012
Hrvatska