An Algorithm for Dual Transformation in First-Order Logic

The transformation between conjunctive and disjunctive canonical forms is useful in domains such as theorem proving, function minimization, and knowledge representation. In this paper, we present a concurrent algorithm for this transformation, suitable for first-order logic theories. The proposed algorithm use the holographic relation between these normal forms in order to avoid the generation of noncondensed and subsumed (dual) clauses. We also stress the facts that, in first-order logic, this transformation is asymmetric and that disjunctive normal form, in some special cases, may be not unique, depending on choices about which subsumptions are allowed or not. The algorithm, which is part of a theorem-proving knowledge representation project, has been implemented and tested.