Date:
Thursday, 13 June, 2024 - 17:00 to 18:00
Speaker:
Tobias Nipkow (Technische Universität München)
Venue:
Live-streamed at MR14 Centre for Mathematical Sciences
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
Seminar series:
Formalisation of mathematics with interactive theorem provers
