SYNTHESIS OF CHESS AND CHESS-LIKE ENDGAMES: A PROOF OF CORRECTNESS

Article type: Research Article

Authors: Coplan, K.P^{; 1}

Affiliations: University of Bradford, Bradfort, UK

Note: [1] School of Computing and Mathematics, Phoenix Building, University of Bradford, Richmond Road, Bradford BD7 1DP, England. Email: [email protected].

Abstract: An algorithm for synthesising correct and optimal game-playing programs in the domain of chess-like endgames from specifications is investigated and explained in detail. The central component of the algorithm is a routine that repeatedly transforms expanded win-in-n-ply predicates to equivalent but smaller expressions. The routine is designed to monitor its own execution in order to accelerate its progress through the problem space, drastically reducing execution time. The basis of this self-monitoring is to enable the reuse of computations avoiding redundancy in both the synthesis process itself, and its resulting output. The paper presents a formal proof of correctness for this routine. The problem of debugging implementations of the algorithm, due to the complexity of the predicates generated is discussed. The assistance provided by using the formal proof to identify coding errors is explained.

DOI: 10.3233/ICG-2001-24103

Journal: ICGA Journal, vol. 24, no. 1, pp. 16-29, 2001