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.
## 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"}