Computer Theorem Proving and HoTT

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ LOGIC THEORY MACHINE of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

WCCC 2013: the 20th World Computer Chess Championship

The 20th World Computer Chess Championship took place in Yokohama, Japan during August 2013. It was narrowly won by JUNIOR from JONNY with HIARCS, PANDIX, SHREDDER and MERLIN occupying the remaining positions. There are references to the detailed chess biographies of the engines and engine-authors in the Chessprogramming Wiki. The games, occasionally annotated, are available here.

WCCC 2015: the 21st world computer chess championship

Nine chess programs competed in July 2015 in the ICGA's World Computer Chess Championship at the Computer Science department of Leiden University. This is the official report of the event.

Gentlemen, stop your engines!

For fifty years, computer chess has pursued an original goal of Artificial Intelligence, to produce a chess-engine to compete at the highest level. The goal has arguably been achieved, but that success has made it harder to answer questions about the relative playing strengths of man and machine. The proposal here is to approach such questions in a counter-intuitive way, handicapping or stopping-down chess engines so that they play less well. The intrinsic lack of man-machine games may be side-stepped by analysing existing games to place computer engines as accurately as possible on the FIDE ELO scale of human play. Move-sequences may also be assessed for likelihood if computer-assisted cheating is suspected.

6-man chess solved

Eugene Nalimov has completed the computation of a set of endgame tables for 6-man chess, and independently, Marc Bourzutschky has completed tables for 3-3 chess and for 4-2 chess where Black is not just ‘KP’. The ICGA salutes both achievements and looks ahead.

Chess endgames: data and strategy

While Nalimov’s endgame tables for Western Chess are the most used today, their Depth-to-Mate metric is not the only one and not the most effective in use. The authors have developed and used new programs to create tables to alternative metrics and recommend better strategies for endgame play.

Model endgame analysis

A reference model of Fallible Endgame Play has been implemented and exercised with the chess engine WILHELM. Various experiments have demonstrated the value of the model and the robustness of decisions based on it. Experimental results have also been compared with the theoretical predictions of a Markov model of the endgame and found to be in close agreement.

Self-play: statistical significance

Heinz recently completed a comprehensive experiment in self-play using the FRITZ chess engine to establish the ‘decreasing returns’ hypothesis with specific levels of statistical confidence. This note revisits the results and recalculates the confidence levels of this and other hypotheses. These appear to be better than Heinz’ initial analysis suggests.

Reference fallible endgame play

A reference model of fallible endgame play is defined in terms of a spectrum of endgame players whose play ranges in competence from the optimal to the anti-optimal choice of move. They may be used as suitably skilled practice partners, to assess a player, to differentiate between otherwise equi-optimal moves, to promote or expedite a game result, to run Monte-Carlo simulations, and to identify the difficulty of a position or a whole endgame.

The ICGA on the Web

The ICGA and its members can now communicate with each other and a wider public, as never before. The ICGA website ICGA_W, www.icga.org, will complement the ICGA Journal, providing more space and access to an evolving and wider range of items including both topical news and definitive reference material.

Secrets of Pawnless Endings

It is now 32 years since Ströhlein’s pioneering computation of KRKN and ten years since the publication of Nunn’s Secrets of Rook Endings. This book defined a new genre under his authorship and editorship (Nunn, 1992, 1994, 1995; Müller and Lamprecht, 1999, 2001) and has merited a second edition. Now comes the second edition of Secrets of Pawnless Endings.

ken

From the beginning, the world of game-playing by machine has been fortunate in attracting contributions from the leading names of computer science. Charles Babbage, Konrad Zuse, Claude Shannon, Alan Turing, John von Neumann, John McCarthy, Alan Newell, Herb Simon and Ken Thompson all come to mind, and each reader will wish to add to this list. Recently, the Journal has saluted both Claude Shannon and Herb Simon. Ken’s retirement from Lucent Technologies’ Bell Labs to the start-up Entrisphere is also a good moment for reflection.

Ken Thompson's 6-man Tables

Ken Thompson recently communicated some results mined from his set of 64 6-man endgame tables. These list some positions of interest, namely, mutual zugzwangs and those of maximum depth. The results have been analysed by the authors and found to be identical or compatible with the available or published findings of Karrer, Nalimov, Stiller and Wirth.

Space-efficient Indexing of Chess Endgame Tables

Chess endgame tables should provide efficiently the value and depth of any required position during play. The indexing of an endgame’s positions is crucial to meeting this objective. This paper updates Heinz’ previous review of approaches to indexing and describes the latest approach by the first and third authors. Heinz’ and Nalimov’s endgame tables (EGTs) encompass the en passant rule and have the most compact index schemes to date. Nalimov’s EGTs, to the Distance-to-Mate (DTM) metric, require only 30.6 × 10^9 elements in total for all the 3-to-5-man endgames and are individually more compact than previous tables. His new index scheme has proved itself while generating the tables and in the 1999 World Computer Chess Championship where many of the top programs used the new suite of EGTs.