To Table of Contents No.2


A Browsable Format for Proof Presentation

Jim Grundy

Åbo Akademi University
Department of Computer Science
Lemminkäisenkatu 14A
20520 Turku
Finland

Abstract

The paper describes a format for presenting proofs called structured calculational proof. The format resembles calculational proof, a style of reasoning popular among computer scientists, but extended with structuring facilities. A prototype tool has been developed which allows readers to interactively browse proofs presented in this format via the world wide web. The ability to browse a proof increases its readability, and hence its value as a proof. Computers have been used for some time to both construct and check mathematical proofs, but using them to enhance the readability of proofs is a relatively novel application.

Keywords:
calculational proof, proof browsing, proof presentation
CR Classification:
F.4.1, I.7.2

NOTE: This paper is intended to illustrate how the web can be used to support browsable proofs. The formatting in the paper requires some advanced HTML features, to read it you will require a browser that supports HTML Level 3.2. You may also need to stretch your browser window wider than normal for the proofs to format correctly. If you are reading the paper via too slow a link, it will be inconvenient to browse the proofs it contains. To avoid this problem, you can down-load a local copy of the paper.



A Browsable Format for Proof Presentation / Jim Grundy