Document Open Access Logo

Alpha-Beta Pruning Verified (Invited Talk)

Author Tobias Nipkow

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2024.1.pdf
  • Filesize: 461 kB
  • 4 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Algorithmic game theory
Keywords
  • Verification
  • Algorithmic Game Theory
  • Isabelle

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Tobias Nipkow. Alpha-Beta Pruning Verified (Invited Talk). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.1

Author Details

Tobias Nipkow
  • Department of Computer Science, Technical University of Munich, Germany

References

  1. Richard S. Bird and John Hughes. The alpha-beta algorithm: An exercise in program transformation. Information Processing Letters, 24(1):53-57, 1987. URL: https://doi.org/10.1016/0020-0190(87)90198-0.
  2. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of Haskell programs. In Martin Odersky and Philip Wadler, editors, International Conference on Functional Programming (ICFP '00), pages 268-279. ACM, 2000. URL: https://doi.org/10.1145/351240.351266.
  3. John P. Fishburn. Another optimization of alpha-beta search. SIGART Newsl., 84:37-38, 1983. URL: https://doi.org/10.1145/1056623.1056628.
  4. Matthew L. Ginsberg and Alan Jaffray. Alpha-beta pruning under partial orders. In Richard J. Nowakowski, editor, More Games of No Chance, volume 42 of MSRI Publications, pages 37-48. Cambridge University Press, 2002. URL: http://library.msri.org/books/Book42/files/ginsberg.pdf.
  5. J. Hughes. Why Functional Programming Matters. The Computer Journal, 32(2):98-107, 1989. URL: https://doi.org/10.1093/comjnl/32.2.98.
  6. Donald E. Knuth and Ronald W. Moore. An analysis of alpha-beta pruning. Artif. Intell., 6(4):293-326, 1975. URL: https://doi.org/10.1016/0004-3702(75)90019-3.
  7. Junkang Li, Bruno Zanuttini, Tristan Cazenave, and Véronique Ventos. Generalisation of alpha-beta search for AND-OR graphs with partially ordered values. In Luc De Raedt, editor, International Joint Conference on Artificial Intelligence, IJCAI 2022, pages 4769-4775. ijcai.org, 2022. URL: https://doi.org/10.24963/ijcai.2022/661.
  8. Gr. C. Moisil. Recherches sur l'algèbre de la logique. Annales scientifiques de l'Université de Jassy, 122:1-118, 1936. Google Scholar
  9. Tobias Nipkow. Alpha-beta pruning. Archive of Formal Proofs, June 2024. , Formal proof development. URL: https://isa-afp.org/entries/Alpha_Beta_Pruning.html.
  10. Tobias Nipkow, editor. Functional Data Structures and Algorithms. A Proof Assistant Approach. ACM Books. self-published, 2024. URL: https://functional-algorithms-verified.org/.
  11. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
  12. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact