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.
There are two versions of this paper. The first was a printed version appearing in the proceeding of the symposium on Logic, Mathematics and the Computer. The second is an on-line version in the electronic journal Mathesis Universalis. The on-line version is the better of the two. The paper describes a format for presenting proofs that allows the proofs to be browsed interactively. The paper version merely describes what it would be like to be able to browse a proof interactively, whereas the on-line version contains proofs that can actually be browsed. The on-line version also contains an extended example that could not be presented in the paper version.
@ARTICLE{Grundy:1996:ABF,
author = "Jim Grundy",
title = "A Browsable Format for
Proof Presentation",
journal = "Mathesis Universalis",
year = 1996,
volume = 1,
number = 2,
month = "Spring"}
@INPROCEEDINGS{Grundy:1996:BFP,
author = "Jim Grundy",
title = "A Browsable Format for
Proof Presentation",
editor = "Christoffer Gefwert and
Pekka Orponen and
Jouko Sepp{\"a}nen",
booktitle = "Logic, Mathematics and
the Computer --- Foundations:
History, Philosophy and
Applications",
volume = "14",
series = "Symposium Series",
organization = "Finnish Artificial
Intelligence Society",
month = jun,
year = "1996",
address = "Helsinki, Finland",
pages = "171--178",
}
If you liked this paper, then you might also like the following papers which cite it:
If you are having trouble finding the journal or proceedings in which this paper appears, then the following information may be of help:
| Title: | Mathesis Universalis |
| Editor: | Witold Marciszewski |
| URL: | http://www.pip.com.pl/MathUniversalis/ |
| Volume: | 1 |
| Number: | 2 |
| ISSN: | 1426-3513 |
| Copyright: | 1996 |
| Publisher: | Philomath |
| Address: | Krochmalna 3 / 917 00-864 Warszawa POLAND |
| Title: |
Logiikka, matematiikka ja tietokone -
Perusteet: historiaa, filosofiaa ja sovelluksia [Logic, Mathematics and the Computer - Foundations: History, Philosophy and Applications] |
| Editors: | Christoffer Gefwert and Pekka Orponen and Jouko Seppänen |
| Series: | Symposiosarja [Symposium Series] |
| Volume: | 14 |
| ISSN: | 0785-8140 |
| Copyright: | 1996 |
| Publisher: |
Soumen Tekoälyseuran julkaisuja [Finnish Artificial Intelligence Society] PO Box 1201 02044 VTT FINLAND |
| ISBN: | 951-22-3094-1 |
Feedback & Queries:
Jim Grundy