I have a well formed proposition logic formula in disjuntive normal
form (DNF). The original formula uses only OR + AND.

Example: (a&b)|(c&d&e)|(f&g&h&i&j)|(k&l) ...

I am looking for a fast algorithm, that transforms big formulas (maybe
hundreds of clauses) into conjunctive normal form (CNF). It must be possible
to realize it in Java. A ready-for-action-solution in Java is favored.

Hi dave29-ga,

It's not a direct answer to your question (because it's written in
Eiffel rather than in Java), but you could take a look at

   Kniffel: First Order Predicate Logic Converter
   http://www.raboof.at/cgi-bin/kniffel_cgi

It's an online application which I find works well, and it's also an
open-source Eiffel application that you could translate to Java.

Regards,
eiffel-ga

It seems to me that the CNF is obvious but has a tremendous number of
clauses. Say the original DNF is
(a1&a2&...&an)or(b1&b2&...bm)or....(c1&c2&...cp)or... Then the CNF is
the "&" of all clauses of the form: ai or bj or ck or ... as the i's
vary from 1 to n and the j's vary from 1 to m, the k's vary from 1 to
p, etc. So the number of clauses to "&" in the CNF would be n*m*p*....