A New Algorithm for Computing Theory Prime Implicates Compilations

We present a new algorithm (called TPI /BDD) for computing the theory prime implicates compilation of a knowledge base S. In contrast to many compilation algorithms, TPI /BDD does not require the prime implicates of S to be generated. Since their number can easily be exponential in the size of S, TPI/BDD can save a lot of computing. Thanks to TPI/BDD, we can now conceive of compiling knowledge bases impossible to before.