Prime implicants of first order formulas via transversal clauses

Knowledge compilation techniques are usually applied for prepositional knowledge bases. In this article, an extension of the notion of prime implicants of aknowledge base using first order formulas in Skolem conjunctive normal form is suggested. The method of transversal clauses used earlier for computing prime implicants of a propositional formula in conjuctive normal form is adopted to the first order case via substitutions. Partial correctness of the algorithm is proved. The algorithm is adopted heuristically for computing approximate prime implicants.