Binary decision diagrams as a HOL Derived Rule

The Computer Journal, vol. 38, pp. 162-170, 1995.

Abstract:

Binary Decision Diagrams (BDDs) are a representation for Boolean formulas which makes many operations, in particular tautology-checking, surprisingly efficient in important practical cases. In contrast to such custom decision procedures, the HOL theorem prover expands all proofs out to a sequence of extremely simple primitive inferences. In this paper we describe how the BDD algorithm may be adapted to comply with such strictures, helping us to understand the strengths and limitations of the HOL approach.

PostScript

Bibtex entry:

@ARTICLE{harrison-cj95,
        author          = "John Harrison",
        title           = "Binary Decision Diagrams as a {HOL} Derived Rule",
        journal         = "The Computer Journal",
        year            = 1995,
        volume          = "38",
        pages           = "162--170"}