Привести формулу к предварённой нормальной форме

[Nemodny]

Привести $(\forall xQ(x,y))\to (\exists yQ(x,y)\vee \exists xR(x,y))$ к предварённой нормальной форме.
Мое решение:
$\neg(\forall xQ(x,y)) \vee \exists yQ(x,y)\vee \exists xR(x,y)$
$\exists x \neg Q(x,y) \vee \exists yQ(x,y)\vee \exists xR(x,y)$
$\exists x(\neg Q(x,y) \vee R(x,y)) \vee \exists y Q(x,y)$

Как дальше непонятно.

[gefest_md]

Nemodny в сообщении #1096886 писал(а):

$\neg(\forall xQ(x,y)) \vee \exists yQ(x,y)\vee \exists xR(x,y)$
$\exists x \neg Q(x,y) \vee \exists yQ(x,y)\vee \exists xR(x,y)$
...
Как дальше непонятно.

$\exists xA(x)\sim\exists aA(a)$. Поэтому после второй строки можно переименовывать связанные переменные.

[Nemodny]

Т.е. делается замена как то так:

$\exists x\neg Q(x,y) \vee \exists x Q(x,x) \vee \exists x R(x,y)$
$\exists x (\neg Q(x,y) \vee Q(x,x) \vee R(x,y))$

[gefest_md]

Nemodny в сообщении #1097086 писал(а):

Т.е. делается замена как то так:

$\exists x\neg Q(x,y) \vee \exists x Q(x,x) \vee \exists x R(x,y)$
$\exists x (\neg Q(x,y) \vee Q(x,x) \vee R(x,y))$

Нет, не так. Ведь $\exists yQ(x,y)\not\sim\exists xQ(x,x)$ (не равносильно ... связали $x$ который был свободен). Но можно $\exists yQ(x,y)\sim\exists bQ(x,b)$.

[Nemodny]

Переименовал связанные переменные. $x \sim t$, $y \sim b$

$\exists x \neg Q(x,y) \vee \exists b Q(x,b) \vee \exists x R(x,y)$
$\exists t \neg Q(t,y) \vee Q(x,b) \vee \exists t R(t,y)$
$\exists t \exists b(\neg Q(t,y) \vee Q(x,b) \vee R(t,y))$

[gefest_md]

Правильно (во второй строке пропустили квантор $\exists b$).

Nemodny в сообщении #1097175 писал(а):

Переименовал связанные переменные. $x \sim t$, $y \sim b$

$\sim$ (или $\leftrightarrow$) - связки, поэтому справа и слева от них должны стоять только формулы.