Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 1 Sep 1993 18:33:52 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA12958; Wed, 1 Sep 93 10:22:13 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from bilbo.radonc.washington.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA12954; Wed, 1 Sep 93 10:22:05 -0700 Received: by violin1.radonc.washington.edu (1.37.109.4/16.2) id AA13639; Wed, 1 Sep 93 10:24:18 -0700 Date: Wed, 1 Sep 93 10:24:18 -0700 From: Jon Jacky To: info-hol@dworshak.cs.uidaho.edu Subject: Re: HOL improvement: to better document your proof Message-ID: <"swan.cl.cam.:025150:930901173443"@cl.cam.ac.uk> I've been following this thread on proof presentation, for example... > From: John Harrison > > Konrad Slind writes: > > | I think an analysis of textbook-style proofs will show that the > | weighting between forward and backward steps in a proof is different > | than in a typical HOL proof. > > I think it's true that proofs in textbooks are generally forward at > low levels of granularity, although sometimes backward at a higher level... > > ... The question is: why are proofs in mathematics books generally > written forward-- is it just tradition or is there a good reason for it? > > If you look at some "epsilontics" proofs in analysis, lots of instantiations > for lemmas are plucked from the air and then by some magic, the > quantity we're interested in comes out less that epsilon. This sort > of thing seems easier to understand backwards. ... Coincidentally, I've just read a whole book on this subject that readers of this list might find interesting: "On the Shape of Mathematical Arguments" by A. J. M. van Gasteren. The book considers how to develop proofs and then present them for human readers. Van Gasteren proposes a presentation style that I've seen in used by others, for example Edward Cohen and Edsger Dijkstra. Van Gasteren discusses this forward vs. backward issue (which she cals bottom-up vs. top-down) on pps. 110 - 116. She argues that the top-down presentation is usually better. @book{vangasteren90, title = "On the Shape of Mathematical Arguments", author = "A. J. M. van Gasteren", publisher = "Springer-Verlag", year = "1990", series = "Lecture Notes in Computer Science", volume = "445"} Jonathan Jacky jon@radonc.washington.edu Radiation Oncology RC-08 voice: (206)-548-4117 University of Washington FAX: (206)-548-6218 Seattle, Washington 98195 USA