Playing logic programs with the alpha-beta algorithm

Abstract

Alpha-Beta is a well known optimized algorithm used to compute the values of classical combinatorial games, like chess and checkers. The known proofs of correctness of Alpha-Beta do rely on very specific properties of the values used in the classical context (integers or reals), and on the finiteness of the game tree. In this paper we prove that Alpha-Beta correctly computes the value of a game tree even when these values are chosen in a much wider set of partially ordered domains, which can be pretty far apart from integer and reals, like in the case of the lattice of idempotent substitutions or ex-equations used in logic programming. We do so in a more general setting that allows us to deal with infinite games, and we actually prove that for potentially infinite games Alpha-Beta correctly computes the value of the game whenever it terminates. This correctness proofs allows us to apply Alpha-Beta to new domains, like constraint logic programming.