Conclusions and Related Work

The paper has advocated writing proofs in a structured calculational format together with interactive browsing, as a way to increase their readability. The example proof contained in the paper was, by necessity, too small to really benefit from browsing. At any rate, the proof was not browsable since it was presented on paper. However, the utility and readability of the proposed format and browsing technique has been demonstrated by using it to solve a significant and unbiased set of problems: The 1995 Finnish high-school general mathematics matriculation exam. Browsable solutions to these problems are available on the web for interested readers to assess

The most notable sources of inspiration for the proof format described in the paper are the calculational proof format popular among computer scientists (Gries and Schneider 1993), the window inference style of reasoning proposed by Robinson and Staples (Robinson and Staples 1993) and later generalised by Grundy (to appear), and natural deduction (Gentzen 1935). Other systems of proof presentation with similar aims to the one presented here include the `structured proof' notation of Lamport (1995, Rudnicki and Trybulec 1996) and the `block calculus' of Dahn and Wolf (1995). Both Lamport, and Dahn and Wolf discuss the idea of proof browsing, although without as concrete a proposal as was presented here.


A Browsable Format for Proof Presentation: Conclusions and Related Work / Jim Grundy