converting predicate logic to clause form

Question

Lets say we have a statement in predicate logic which we have to convert to clause form to apply unification:

$ \forall x, P1(x) \vee P2(x) \Rightarrow P3(x) $

or,

$ \exists x,\neg( P1(x) \vee P2(x)) \vee P3(x) $

or,

$ \exists x,(\neg P1(x) \wedge \neg P2(x)) \vee P3(x) $

How to go from here? Does it divide into two separate statements, like so-

$ \neg P1(x) \vee P3(x) $

$ \neg P2(x) \vee P3(x) $

?

Answer 1

First Skolemize. In other words, replace all existential quantified statements with appropriate terms. In your example, this means you just replace variables with constants and drop all existential quantifiers. You can also drop all universal quantifiers once you've Skolemized since you'll have them implicitly.

Second, apply the INDO method. In other words, remove all Implications by transforming them into disjunctions, remove all Negations of anything which isn't a literal via De Morgan/Petrus Hispanus laws, then Distribute everything, and finally get rid of the Operators (if you need to convert to sets).