Alpha-Beta Pruning Verified

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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. We have formalized and verified 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.

Original languageEnglish
Title of host publication15th International Conference on Interactive Theorem Proving, ITP 2024
EditorsYves Bertot, Temur Kutsia, Michael Norrish
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959773379
DOIs
StatePublished - Sep 2024
Event15th International Conference on Interactive Theorem Proving, ITP 2024 - Tbilisi, Georgia
Duration: 9 Sep 202414 Sep 2024

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume309
ISSN (Print)1868-8969

Conference

Conference15th International Conference on Interactive Theorem Proving, ITP 2024
Country/TerritoryGeorgia
CityTbilisi
Period9/09/2414/09/24

Keywords

  • Algorithmic Game Theory
  • Isabelle
  • Verification

Fingerprint

Dive into the research topics of 'Alpha-Beta Pruning Verified'. Together they form a unique fingerprint.

Cite this