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.