ANU: The Australian National University
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________

Recording HOL Proofs in a
Structured Browsable Format

Reference

Jim Grundy and Thomas Långbacka. Recording HOL Proofs in a Structured Browsable Format. In Johnson (ed). Algebraic Methodology and Software Technology: Proceedings of the 6th International Conference, AMAST'97, volume 1349 of Lecture Notes in Commputer Science, Sydney, December 1997. Springer-Verlag. pages 567-571.

Abstract

It is possible to discern two attitudes toward proof in the computer science community. Some regard a proof as a formal mathematical object, while the others view proof as a social process: a proof is an argument that convinces its reader. These views have been largely incompatible.

The goal of our work is to record proofs checked by the HOL theorem prover~\cite{Gor93b} in a readable format. Even experienced HOL users find it difficult to read proofs described using the HOL meta-language. Our idea is that such a record would constitute a convincing proof under both definitions by being both readable and machine checked.

We have attempted to address the readability problems of formal proofs by recording the steps and intermediate results of HOL proofs in a browsable format. This format hides unnecessary levels of detail in the proof from the reader, while allowing them to view as much of the proof as they feel is necessary to become convinced of its validity.

BibTeX

Here is a suitable BibTeX entry:

  @INPROCEEDINGS{Grundy:1997:RHP,
    author      = "Jim Grundy and Thomas L{\aa}ngbacka",
    title       = "Recording {HOL} Proofs in a
                   Structured Browsable Format",
    pages       = "567--571",
    editor      = "Michael Johnson",
    booktitle   = "Alebraic Methodology and
                   Software Technology:
                   6th International Conference,
                   AMAST'97",
    series      = "Lecture Notes in Computer Science",
    volume      = 1349,
    address     = "Sydney, Australia",
    month       = dec,
    year        = 1997,
    publisher   = "Springer-Verlag"}

Where To Find it

If you are having trouble finding the proceedings in which this paper appears, then the following information may be of help:

Title: Algebraic Methodology and Sofware Technology:
Proceedings of the 6th International Conference, AMAST97
Editor: Michael Johnson
Series: Lecture Notes in Computer Science
Volume: 1349
Copyright: 1997
Publisher: Springer-Verlag, Berlin
ISSN: 0302-9743
ISBN 3-540-63888-1
_____________________________________________________________________
[ANU] [FEIT] [DCS] [Jim Grundy] [Research] [Teaching] [Publications] [Software] [CV]
_____________________________________________________________________
Feedback & Queries: Jim Grundy
Date Last Modified: Thu 11 Nov 1999
Universal Ressource Locator: file:/home/jgrundy/www//Publications/amast97.html