1
$\begingroup$

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) $

?

$\endgroup$
1
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Thanks for the INDO tip. So it appears that my conclusion is correct. $\endgroup$ – goelakash Nov 25 '15 at 7:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.