The Heine-Borel challenge problem. In honor of Woody Bledsoe

Woody Bledsoe's last challenge problem is the analogical transfer of the Heine-Borel theorem for real intervals to the two-dimensional case. This could not be solved by the up-to-then-known techniques of analogical theorem proving. The Heine-Borel theorem is a widely known result in mathematics. It is usually stated in the field of real numbers R-1, and similar versions are also true in R-2, in topology, and in metric spaces. This article shows how analogy-driven proof plan construction is applicable to this genuinely mathematical problem. Our goal here was to use a source proof plan of HB1 (the Heine-Borel theorem in R-1) as a guide to automatically produce a proof plan of HB2 (the Heine-Borel theorem in R-2). We were able to accomplish our goal by generating the target proof plan of HB2 by reformulation and analogical replay.