A Mizar Mode for HOL

John Harrison.

Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'96, Springer LNCS 1125, pp. 203-220, 1996.

Abstract:

The HOL theorem prover is implemented in the LCF style, meaning that all inference is ultimately reduced to a collection of very simple (forward) primitive inference rules. By programming it is possible to build alternative means of proving theorems on top, while preserving security. Existing HOL proofs styles are, however, very different from those used in textbooks. Here we describe the addition of another proof style, inspired by Mizar. We believe the resulting system combines some of the best features of both HOL and Mizar.

DVI (Times font) or PostScript (Times font) or PDF (Times font)

DVI (CM font) or PostScript (CM font) or PDF (CM font)

The Times versions are recommended for printing, but the Computer Modern ones sometimes look better on previewers.

Bibtex entry:

@INPROCEEDINGS{harrison-mizar,
        author          = "John Harrison",
        title           = "A Mizar Mode for {HOL}",
        pages           = "203--220",
        editor          = "Joakim von Wright and Jim Grundy and John Harrison",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           9th International Conference, TPHOLs'96",
        series          = "Lecture Notes in Computer Science",
        volume          = 1125,
        address         = "Turku, Finland",
        date            = "26--30 August 1996",
        year            = 1996,
        publisher       = "Springer-Verlag"}