Artificial Intelligence Blog

So, I am a bit disappointed that there do not seem to be any great methods for automated proving of theorems for games.  The best seems to be “Automated Theorem Proving for General Game Playing” (Schiffel & Thielsche 2009) and “A Temporal Proof System for General Game Playing” (Thielscher & Voigt 2010).  In the first paper, their program (which uses a sophisticated “answer set programming” theorem prover) proves theorems like ”

• proving that the argument of the control(P) feature is
unique in every state (provided the feature exists);
• proving that the contents of a board cell is unique (to which
end boards were identified manually);
• proving that the contents of a board cell is unique given
the information that the argument of control(P) is;
• proving that the game is zero-sum;
• systematic search for unique arguments as described at the
end of the preceding section.”

It is great that the authors combine automated theorem provers with game playing, but I am still somewhat disappointed because most people who play a game can easily read the rules and almost immediately answer questions about the game like “Is it zero-sum?” or “Do the squares only have one piece?”.  I was hoping for deeper theorems.  It is also disappointing that one of our best automated theorem proving algorithms cannot even prove these simple theorems for many games.

On the other hand, maybe we should only prove simple properties like this. When playing chess about the only theorems I ever apply are:  1) when in check, there are only three possible options – move the king, interpose a piece, or capture the attacking piece, and 2) if a piece is blocking an attack on its king, it cannot move (a pin). Really, I don’t think I use any theorems deeper than this while playing chess and those two theorems are not at all useful to a computer because the computer can easily list all the possible moves.

In other games, I guess I do use theorems like “if I lead the third highest card in bridge, a finesse will succeed if the player on my left has the second highest card and my partner has the highest card (assuming no trump)” or “if my team holds 11 of the hearts, then the other team’s hearts will split 1-1 52% of the time.”

If computers are going to reason about games, then we probably need fuzzy logic (as in this paper) and/or probability theory.

In the paper “Automated Theorem Proving for General Game Playing” by Stephan Schiffel and Michael Thielscher, the authors apply answer set programming (similar to Prolog) to improve performance in general game playing. They point out that it is important for the AI to classify what type of game it is playing and to apply appropriate techniques for that class of game. For example null moves, upper confidence trees (UCT), alpha-beta search, Bellman equations (dynamic programming), and temporal difference learning would all be appropriate for two-player, zero-sum, and turn-taking games.  Also it is important to recognize concepts “like boards, pieces, and mobility.” Apparently, van der Hoek pioneered using automated theorem proving to extract appropriate concepts from the game rules.  Shiffel and Thielscher extend the theorem proving to “automatically prove properties that hold across all legal positions.”