Приведение к ПНФ и ССФ (проверить решение)

[WtCrow]

Я пытаюсь разобраться с приведением к ПНФ и ССФ.
Буду благодарен, если кто-нибудь проверит правильность действий.
Исходное выражение:
$\forall x(\neg A(x)\to\exists x(\neg C(x)))\to\forall x(C(x)\to A(x))$
Заменяем импликацию в скобках
$\forall x(A(x) \vee \exists x(\neg C(x)))\to\forall x(\neg C(x) \vee A(x))$
Заменяем последнюю импликацию
$\neg(\forall x(A(x) \vee \exists x(\neg C(x))))\vee\forall x(\neg C(x) \vee A(x))$

Избавляемся от отрицания над квантором всеобщности $\forall x(A(x) \vee \exists x(\neg C(x)))$
$\exists x(\neg (A(x) \vee \exists x (\neg C(x))))\vee\forall x(\neg C(x) \vee A(x)) $
$\exists x(\neg A(x) \wedge \neg\exists x (\neg C(x)))\vee\forall x(\neg C(x) \vee A(x)) $
Убираем отрицание над квантором существования $\exists x (\neg C(x))$
$\exists x(\neg A(x) \wedge \forall x (C(x)))\vee\forall x(\neg C(x) \vee A(x)) $

Заменяем $\forall x(C(x))$ на $\forall y(C(y))$
и $\forall x(\neg C(x) \vee A(x))$ на $\forall z(\neg C(z) \vee A(z))$

Получаем:
$\exists x(\neg A(x) \wedge \forall y (C(y)))\vee\forall z(\neg C(z) \vee A(z)) $
Теперь мы можем вынести за скобки все кванторы
$\exists x \forall y\forall z ((\neg A(x) \wedge C(y))\vee\neg C(z) \vee A(z)) $

Приводим к КНФ:
$\exists x \forall y\forall z ((\neg A(x)\vee\neg C(z) \vee A(z)) \wedge (C(y)\vee\neg C(z) \vee A(z))) $
На сколько я понимаю, это ПНФ.

Для получения ССФ нужно заменить $x$ на константу $a$ и отбросить кванторы всеобщности $\forall y\forall z$
Таким образом, ССФ будет иметь вид:
$(\neg A(a)\vee\neg C(z) \vee A(z)) \wedge (C(y)\vee\neg C(z) \vee A(z)) $

Все ли правильно или где-то есть ошибки?

[george66]

Префиксная нормальная форма, кажется, правильная. А что такое ССФ? Эрбрановская?

[WtCrow]

george66 в сообщении #1395320 писал(а):

Префиксная нормальная форма, кажется, правильная. А что такое ССФ? Эрбрановская?

ПНФ - предваренная (она же префиксная) нормальная форма
ССФ - сколемовская (иногда встречается как скулемовская) стандартная форма

[george66]

Не помню, честно говоря. Эрбрановскую ещё помню.

[WtCrow]

Почитал еще и, кажется, кванторы всеобщности отбрасывать не нужно, т. е. ССФ будет иметь вид:
$\forall y\forall z((\neg A(a)\vee\neg C(z) \vee A(z)) \wedge (C(y)\vee\neg C(z) \vee A(z))) $

[george66]

WtCrow в сообщении #1395445 писал(а):

Почитал еще и, кажется, кванторы всеобщности отбрасывать не нужно, т. е. ССФ будет иметь вид:
$\forall y\forall z((\neg A(a)\vee\neg C(z) \vee A(z)) \wedge (C(y)\vee\neg C(z) \vee A(z))) $

Наверное, да, поскольку в эрбрановской (двойственной) нормальной форме остаются только кванторы существования. А где почитали?

[WtCrow]

Цитата:

А где почитали?

Лекции в интернете (ссылка)

[george66]

Ну, судя по описанию, сделано правильно. Но я такого, честно говоря, не учил.

[arseniiv]

Если нужно больше голосов, я тоже думаю, что по крайней мере конечные результаты выглядят верно. В выкладки не вчитывался.

Единственно, в некоторых курсах внешние кванторы всеобщности могут всё же выкидываться (хотя я таких вроде не видел; но по этой части я тоже особо не смотрел где что, а по другим поводам такое выкидывание бывает допустимо). Это на случай маловероятных неожиданностей.