LIPIcs.ITP.2024.1.pdf
- Filesize: 461 kB
- 4 pages
Document
Alpha-Beta Pruning Verified (Invited Talk)
Author
Tobias Nipkow 
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.ITP.2024.1
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.
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)
0PDF Downloads
References
- 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.
- 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.
- John P. Fishburn. Another optimization of alpha-beta search. SIGART Newsl., 84:37-38, 1983. URL: https://doi.org/10.1145/1056623.1056628.
- 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.
- J. Hughes. Why Functional Programming Matters. The Computer Journal, 32(2):98-107, 1989. URL: https://doi.org/10.1093/comjnl/32.2.98.
- 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.
- 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.
-
Gr. C. Moisil. Recherches sur l'algèbre de la logique. Annales scientifiques de l'Université de Jassy, 122:1-118, 1936.
- Tobias Nipkow. Alpha-beta pruning. Archive of Formal Proofs, June 2024. , Formal proof development. URL: https://isa-afp.org/entries/Alpha_Beta_Pruning.html.
- Tobias Nipkow, editor. Functional Data Structures and Algorithms. A Proof Assistant Approach. ACM Books. self-published, 2024. URL: https://functional-algorithms-verified.org/.
- Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
-
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.