A Symbolic Finite-State Approach For Automated Proving of Theorems in Combinatorial Game Theory

By Thotsaporn "Aek" Thanatipanonda and Doron Zeilberger

.pdf     .ps        .tex files  
[Appeared in Journal of Difference Equations and Its Applications 15 (2009), 111 - 118]
Written: Aug. 29, 2007.

This is my sweet revenge against Jeff Erickson's snide remarks, that I have already got mad at, but it is better to get even. My brilliant student Thotsaporn "Aek" Thanatipanonda, and I taught our computer how to prove some conjectures made by that same Erickson, way back when he was at grad school. Not only that, it can make much more elaborate conjectures and then prove them, all without human touch!

In hindsight, we are very thankful to Jeff for his snide remarks, since this lead me to look up his work and discover his early paper on Toads and Frogs, that is admittedly a beautiful piece of work, as far as humans go. But humans can only go so far, so our present paper is a dramatic illustration of computer-generated-mathematics and the "ansatz ansatz".

Important: This article is accompanied by Maple package ToadsAndFrogs that automatically conjectures and then automatically proves explicit expressions for values of certain families of Toads and Frogs game-positions.

Sample Input and Output

  • For the values of positions (f[1]) consisting of a1 Toads followed by one Blank followed by a2 Toads followed by one Frog, as well as for the values of positions (f[2]) consisting of a1 Toads followed by one Frog followed by one Blank (what we call in the paper class A11),
    the input produces the output .
  • For the values of positions (f[1]) consisting of a1 Toads followed by one Blank followed by a2 Toads followed by one Blank followed by a3 Toads followed by one Frog, as well as for the values of positions (f[2]) consisting of a1 Toads followed by one Blank followed by a2 Toads followed by one Frog followed by one Blank (f[2]) as well as as for the values of positions (f[3]) consisting of a1 Toads followed by one Frog followed by two Blanks, (what we call in the paper class A21),
    the input produces the output .
  • For the class of positions of the form Ta1BTa2BTa3B Ta4F (f[1]),
    as well as the class of positions Ta1BTa2BTa3FB (f[2]),
    as well as the class of positions Ta1BTa2FBB (f[3]),
    as well as the class of positions Ta1FBBB (f[4]),
    (what we call in the paper class A31) the input produces the output .
  • For the class A41, the input produces the output .
  • For the class A51, the input produces the output .
  • For the class A12, the input produces the output .
  • For the class A22, the input produces the output .
  • For the class A32, the input produces the output . (This contains, amongsts many other results, the proof of Jeff Erickson's conjecture mentioned in the paper).
Added Sept. 26, 2007: I am going to talk about it at a special session, organized by Moa Apagodu and Akalu Tefera, on 4:30pm (local time), Jan. 8, 2008, at the AMS annual meeting to be held in San Diego. Here is the abstract

Doron Zeilberger's List of Papers

Doron Zeilberger's Home Page