Hello, I have the following formula that I need to turn into a normal form required for the resolution rule. I understand that this comes from the sum of the ORs as in:
(V1 lor V2) land (V3 or V4))
forall x forall y [P(x,y) Rightarrow exists z [Q(y,z] land lnot R (x, z)]] lor forall Q (x, y, z)
So, I use Skolem to substitute exist z for a constant A, then remove the universal quantizers and follow the rules of the general logic for which I arrived:
bigl ( lnot P (x, y) lor Q (y, A) lor Q (x, y, z) bigl) land bigl ( lnot P (x, y) lor R (x , A) or Q (x, y, z) bigl)
Is it correct? Or did I make a mistake somewhere?