Structured Calculational Proof

Reference

Note: this version of the paper superceeds an earlier version published as a technical report by both The Australian National University (ANU) and the Turku Centre for Computer Science (TUCS).

ANU Technical Report

Ralph Back, Jim Grundy and Joakim von Wright. Structured Calculational Proof. Joint Computer Science Technical Report TR-CS-96-09. The Australian National University, Department of Computer Science, Canberra ACT 0200, Australia. November 1996.

TUCS Technical Report

Ralph Back, Jim Grundy and Joakim von Wright. Structured Calculational Proof. TUCS Technical Report 65. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. November 1996.

Abstract

We propose a new format for writing proofs, called structured calculational proof. The format resembles the calculational style already familiar to many computer scientists, but extends it to allow the hierarchical decomposition of larger proofs into smaller ones. Structured calculation is actually an alternative presentation of natural deduction, a 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 browsing proofs in electronic publications.

BibTeX

Here is a suitable BibTeX entry:

  @ARTICLE{Back:1997:SCP,
    author      = "Ralph Back and Jim Grundy and Joakim von Wright",
    title       = "Structured Calculational Proof",
    journal     = "Formal Aspects of Computing",
    year        = 1997,
    volume      = 9,
    number      = "5--6",
    pages       = "469--483"}

Where To Find it

If you are having trouble finding the journal in which this paper appears, then the following infomation might be of help.