Nuprl - The Towers of Hanoi - a thorough treatment

HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
HanoiTowersNuprl Section: HanoiTowers - Towers of Hanoi: a thorough treatment. The purpose of these notes is to exhibit the application of formal proof-oriented methods to a familiar non-trivial problem. A variety of informal explanations and executable solutions may be easily found on the WEB by searching for "towers of hanoi". We formulate various aspects of the problem domain and prove various key claims about them.

Here are the main contents, both extant and planned:

The Towers of Hanoi Problem

Standard Solution

Standard Solution Explicitly

A Non-Standard Recursive Solution

Standard Solution is Optimal

Deriving Simpler Output Data (in preparation)

Deriving an Iterative Method (in preparation)

Automatic Extraction of a Solution (in preparation)

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

HanoiTowers Sections NuprlLIB Doc

The Towers of Hanoi Problem

Standard Solution

Standard Solution Explicitly

A Non-Standard Recursive Solution

Standard Solution is Optimal

Deriving Simpler Output Data	(in preparation)

Deriving an Iterative Method	(in preparation)

Automatic Extraction of a Solution	(in preparation)