Title: Playing Logic Programs with the Alpha-Beta Algorithm
Authors: Roberto Di Cosmo, Jean-Vincent Loddo

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
correction 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 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 to apply Alpha-Beta to new domains, like
constraint logic programming.