An Optimized Transformation into Conjunctive (or Disjunctive) Normal Form

Abstract

Resolution based theorem proving systems require the conversion of predicate logic formulae into clausal normal form. One step of all procedures performing this transformation is the multiplication into conjunctive normal form. In general this is a critical step, since it can result in an exponential increase in the size of the original formula. In general the resulting clausal normal form even contains many redundant clauses. This paper presents a multiplication algorithm that avoids the generation of these redundant clauses. It is shown that the set of clauses generated by this algorithm is the set of prime implicants (in the sense of Quine) of the original formula. Especially in those cases where the usual multiplication algorithm produces a contradictory set of ground clauses the improved algorithm generates the empty clause.