Animating Proofs

Abstract

Visualizing the proof of an algorithm is different from visualizing the algorithm itself, as is done by various systems described in Chapter 23. Visualization of a proof is an algorithm animation that goes one step further: It can be composed of an algorithm animation extended by a proof-dialog that exhibits in a temporal fashion and with visual means the correctness of the algorithm. In this chapter we describe a framework that defines three primary components for a proof visualization system: (1) the definition of the abstract operations necessary for a proof of correctness visualization, (2) the design of operations for the proof process or dialog, and (3) the correspondence between the proof visualization and the algorithm visualization. A detailed description of this system can be found in [Glo92b].