Stålmarck's algorithm as a HOL derived rule

John Harrison.

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

Abstract:

Stålmarck's algorithm is a patented technique for tautology-checking which has been used successfully for industrial-scale problems. Here we describe the algorithm and explore its implementation as a HOL derived rule.

DVI (Times font) or PostScript (Times font) or PostScript (CM font)

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

Bibtex entry:

@INPROCEEDINGS{harrison-stal,
        crossref        = "hol96",
        author          = "John Harrison",
        title           = "St{\aa}lmarck's algorithm as a {HOL} derived rule",
        pages           = "221--234"}


@PROCEEDINGS{hol96,
        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"}