ANU Computer Science Technical Reports
TR-CS-96-09
Ralph Back, Jim Grundy, and Joakim von Wright.
Structured calculational proof.
November 1996.
This paper is also available as Turku Centre for Computer Science TUCS
Technical Report No 65.
[POSTSCRIPT (86390 bytes)] [PDF (120426 bytes)]
Abstract: We propose a new format for writing proofs,
which we call structured calculational proof. The format is similar to
the calculational style of proof already familiar to many computer
scientists, but extends it by allowing large proofs to be hierarchically
decomposed into smaller ones. In fact, structured calculational proof can be
seen as an alternative presentation of natural deduction. Natural deduction
is a well established style of reasoning which uses hierarchical
decomposition to great effect, but which is traditionally expressed in a
notation that is inconvenient for writing calculational proofs. The
hierarchical nature of structured calculational proofs can be used for proof
browsing. We comment on how browsing can increase the value of a proof, and
discuss the possibilities offered by electronic publishing for the
presentation and dissemination of papers containing browsable proofs.
Technical Reports <Technical-DOT-Reports-AT-cs-DOT-anu.edu.au>
Last modified: Tue May 31 12:55:59 EST 2011