Speaker: Tobias Nipkow, Technische University München (Emeritus)
Tuesday 2025-03-11 14:00, Room to be announced
Abstract:
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. In this talk I will survey my recent formalizations and verifications of a number of standard variations of alpha-beta pruning. Findings include:
- Basic variants already having a property ascribed to an improved version
- Authors being confused about which algebraic structure they actually work in
- Generalizations to new algebraic structures
- The implementation in a famous paper is flawed
Warning: There are no new quantitative results and all algorithms are expressed functionally.
Bio: Tobias Nipkow obtained his MSc from Darmstadt, did time in Manchester (where he received his PhD) and the two Cambridges before moving to the Technical University of Munich in 1992 where he has been since. He is best known for work in Term Rewriting and especially as one of the developers and evangelists of the proof assistant Isabelle.