Prime Implicates of First Order Formulas.
Manoj K. Raut, Arindama Singh · International journal of computer science and applications · 2004
This paper extends the notion of prime implicates to first order logic formulas without equality which are assumed to be in Skolem Conjunctive Normal Form. Using the extended notions of consensus and subsumption it is shown that the consensus-subsumption algorithm for computing prime implicates well known for propositional formulas can be conditionally lifted to first order formulas.