Goodies for simplifying conjunctive or disjunctive normal forms....

I'm in need of a goodie or other set of code which can simplify expressions of the conjunctive or disjunctive
normal form variety.  In less technical terms, these'd be the set of expressions which, in Smalltalk, or other
programming languages with Boolean objects, evaluate to true or false:  Expressions made up of AND, OR,
NOT, the comparison relations (<,>,<=, etc), equality and inequality.  CNFs have just ANDs and NOTs
in them, as well as the comparisons.  DNFs have just ORs and NOTs in 'em as well as the comparisons.
Both consist of only binary ANDs or ORs, respectively.

Anyway, this is the kind of thing that might appear in a compiler and used to simplify these expressions
before optimization or as part of it.

Ideally I'd like the expressions to be represented as abstract syntax trees or their equivalents, such
as those produced by TGEN, but I'll settle for anything as long as it's complete.  (One can do the
same with string rewrite rules, but it's inherently slower.)

My fallback is to find something similiar in LISP and rewrite it.  There ought to be lots of those things
around.  I'll also work from Eiffel or Java.

Thanks.  If you know of some significant part of a published goodie that might have this kind
of thing, let me know, too.  I checked the UIUC Archive but, at least using the obvious search
terms, I got no hits.  I'm planning to hunt through its source codes next.

  --Jan