Introduction

It is not usually possible, nor indeed desirable, to present a proof in complete detail. Partly this is due to the limited number of pages available to any author publishing in a journal or conference proceedings. More significantly, however, it is due to the fact that to present any nontrivial argument in complete detail - right down to the level of the basic axioms and inference rules of the logic - would render it unreadable.

At what level of detail should a proof be presented? If an author presents a proof in too fine a detail it will be difficult to read, and hence unconvincing. Including too little detail will also make a proof unconvincing. Judging the right level of detail for a proof is one of the things that distinguishes a good author. Good authors know their audience - what they find obvious, and what they will find interesting - and present their proofs accordingly. However, since not all readers are the same, even the best author cannot present a proof in a way that is optimal for its whole audience.

Perhaps the solution is to take the problem out of the hands of authors, and to let readers decide for themselves how much detail they need to see in proof. Of course, this is not possible with proofs presented on paper, but the increasing popularity of electronic publishing may soon make such considerations less important. This paper describes a structured format for presenting proofs which, with the aid of computer support, allows proofs to be viewed at various levels of detail.


A Browsable Format for Proof Presentation: Introduction / Jim Grundy