Alpha-Beta Pruning

Tobias Nipkow 📧

June 13, 2024


Alpha-beta pruning is an efficient search strategy for two-player game trees. It was invented in the late 1950s and is at the heart of most implementations of combinatorial game playing programs. These theories formalize and verify a number of variations of alpha-beta pruning, in particular fail-hard and fail-soft, and valuations into linear orders, distributive lattices and domains with negative values. A detailed presentation of these theories can be found in the chapter Alpha-Beta Pruning in the (forthcoming) book Functional Data Structures and Algorithms --- A Proof Assistant Approach.


BSD License


Session Alpha_Beta_Pruning