View Question
 Question
 Subject: Logic Category: Science > Math Asked by: dave29-ga List Price: \$14.50 Posted: 18 Jul 2006 08:21 PDT Expires: 17 Aug 2006 08:21 PDT Question ID: 747361
 ```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*....```