Binary decision diagrams as a HOL Derived Rule

John Harrison.

Proceedings of the 1994 International Workshop on Higher Order Logic theorem proving and its applications, Valletta, Malta. Springer LNCS 859, pp. 254-268, 1994.

NB! This paper is superseded in its main theme by a newer version

Abstract:

Exhaustive testing of boolean terms has long been held to be impractical for nontrivial problems, since the problem of tautology-checking is NP-complete. Nevertheless research on Ordered Binary Decision Diagrams, which was given a great impetus by Bryant's pioneering work, shows that for a wide variety of realistic circuit problems, exhaustive analysis is tractable. In this paper we seek to explore how these datastructures can be used in making an efficient HOL derived rule, and illustrate our work with some examples both from hardware verification and pure logic.

PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-hol94,
        crossref        = "hol94",
        author          = "John Harrison",
        title           = "Binary Decision Diagrams as a {HOL} Derived Rule",
        pages           = "254--268"}

@PROCEEDINGS{hol94,
        editor          = "Thomas F. Melham and Juanito Camilleri",
        booktitle       = "Higher Order Logic Theorem Proving and Its
                           Applications: Proceedings of the 7th
                           International Workshop",
        series          = "Lecture Notes in Computer Science",
        volume          = 859,
        address         = "Valletta, Malta",
        date            = "19--22 September 1994",
        year            = 1994,
        publisher       = "Springer-Verlag"}