Построение ПНФ

[Praytic]

Можете проверить, правильно ли я преобразую формулу к предваренной нормальной форме?
$ \varphi = \neg\forall{y}(\exists{x}P(x, y)\rightarrow \forall{u}(R(y, u) \rightarrow \neg\forall{z}(P(z, u) \vee \neg R(z, y)))) $
$ \varphi = \exists{y}\neg(\forall{x}\neg P(x, y) \vee \forall{u}(\neg R(y, u) \vee \exists{z}(\neg P(z, u) \wedge R(z, y)))) $
$ \varphi = \exists{y}\exists{x}\exists{u}\neg(\neg P(x, y) \vee (\neg R(y, u) \vee \exists{z}(\neg P(z, u) \wedge R(z, y)))) $
$ \varphi = \exists{y}\exists{x}\exists{u}(P(x, y) \wedge (R(y, u) \wedge \forall{z}(P(z, u) \vee \neg R(z, y)))) $
$ \varphi = \exists{y}\exists{x}\exists{u}\forall{z}(P(x, y) \wedge (R(y, u) \wedge(P(z, u) \vee \neg R(z, y)))) $
Не знаю точно, когда можно выносить кванторы за скобку...

[arseniiv]

Praytic в сообщении #1076889 писал(а):

Не знаю точно, когда можно выносить кванторы за скобку...

Алгоритм разве не описан в деталях?

[Praytic]

arseniiv в сообщении #1076921 писал(а):

Praytic в сообщении #1076889 писал(а):

Не знаю точно, когда можно выносить кванторы за скобку...

Алгоритм разве не описан в деталях?

Но это только мои догадки. У меня верные преобразования?