Пренексные нормальные формы исчисления предикатов.

[Reef]

Здравствуйте! Прошу Вас помочь с решением следующей задачи.
Привести формулу к ПНФ:

$$F = \forall x ( P(x) \equiv \exists x R(x)) \to \forall y Q(y) $$

исключив логические связки эквивалентности и импликации получил:

$$F = \neg ( \forall x ( ( \neg P(x) \vee \exists x R(x)) \wedge (P(x) \vee \neg \exists x R(x)))) \vee \forall yQ(y) $$

продвинув знак отрицания до атома получил:

$$F = \exists x ((P(x) \wedge \forall x ( \neg R(x))) \vee ( \neg P(x) \wedge \exists x R(x))) \vee \forall y Q(y) $$

(Оффтоп)

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

[Sonic86]

Reef в сообщении #735247 писал(а):

нужно переименовать связанные переменные

Грубо говоря, в формуле не должно быть двух кванторов по одинаковым переменным. Посмотрите на исходную формулу и определите, есть ли такое (и лучше сделайте замену сразу там)

Reef в сообщении #735247 писал(а):

Прошу Вас проверить мною уже "нацарапанное"

по-моему, верно (Хотя 2-я формула избыточна).

Reef в сообщении #735247 писал(а):

вынести квантаторы

У Вас в аксиомах (если не ошибаюсь, а может и нет) должно быть правило вноса-выноса квантора в случае вида $Q\wedge (Kx)P(x)$ или $Q\vee (Kx)P(x)$, где $Q$ не зависит от $x$ - посмотрите или догадайтесь. Этого будет достаточно.

Reef в сообщении #735247 писал(а):

удалить квантификции

Как удаляется квантор всеобщности в ПНФ? А как удаляется квантор существования?

[Reef]

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

$$ F = \forall x (P(x) \equiv \exists z R(z)) \to \forall y Q(y)$$

затем я получу с учетом замены:

$$ F = \exists x (( P(x) \wedge \forall z (\neg R(z))) \vee ( \neg P(x) \wedge \exists z R(z))) \vee \forall y Q(y) $$

далее произвожу внос-вынос квантора, а именно:

$$F = \exists x ( \forall z (P(x) \wedge ( \neg R(z))) \vee \exists z ( \neg P(x) \wedge R(z))) \vee \forall y Q(y)$$

теперь, если я все сделал правильно, необходимо выполнить еще замену, чтобы не было кванторов по одинаковой переменной или тут возможно иное преобразование?

(Оффтоп)

Вторая формула действительно избыточна, старался показать ход действий.
Я судя по всему ввел Вас в заблуждение, простите меня, в исходнике написано так "удаление квантификаций, область действия которых не содержит вхождений квантифицируемых переменных."

[Sonic86]

Reef в сообщении #735429 писал(а):

Т.к. в формуле не должно быть двух кванторов по одинаковой переменной, то исходное выражение примет вид:

$$ F = \forall x (P(x) \equiv \exists z R(z)) \to \forall y Q(y)$$

Ага, замену кванторов сделали правильно.

Reef в сообщении #735429 писал(а):

затем я получу с учетом замены:

$$ F = \exists x (( P(x) \wedge \forall z (\neg R(z))) \vee ( \neg P(x) \wedge \exists z R(z))) \vee \forall y Q(y) $$

У Вас еще остался квантор $(\forall y)$, его тоже надо вынести.

Reef в сообщении #735429 писал(а):

далее произвожу внос-вынос квантора, а именно:

$$F = \exists x ( \forall z (P(x) \wedge ( \neg R(z))) \vee \exists z ( \neg P(x) \wedge R(z))) \vee \forall y Q(y)$$

Это преобразование формулы, конечно, эквивалентное, но оно не нужно - оно не ведет к ПНФ, если его оставить, то потом Вам явно (либо неявно) нужно его отменять. вру... Здесь теперь можно переименовать одну из переменных $z$ в $u$ например, и выполнять вынос кванторов дальше.

Reef в сообщении #735429 писал(а):

Я судя по всему ввел Вас в заблуждение, простите меня,

не ввели

Reef в сообщении #735429 писал(а):

в исходнике написано так "удаление квантификаций, область действия которых не содержит вхождений квантифицируемых переменных."

либо я чего-то не понял, либо это неверно. По определению, пренексная нормальная форма данной формулы $F$ - это эквивалентная ей формула вида $(K_1x_1)...(K_nx_n)P(x_1,...,x_n)$, $K_j$ - кванторы (проверьте меня, что я правильно написал определение, в книжке форма называется предваренной нормальной формой. Если у Вас другое определение, то забудьте, все, что я написал). В процессе приведения к ПНФ мы наоборот "вытаскиваем" кванторы изнутри формулы влево, включая в область их действия те части формулы, которые от переменных могут не зависеть.

З.Ы. Слушайте, а зачем Вы $X\equiv B$ переписываете через $\vee$ и $\wedge$ - оно Вам надо? Только буковок больше становится и проблем тоже... Или у Вас в задании явно написано, что нужно предикат внутри выразить только через $\neg, \vee, \wedge$?

[Reef]

В задании написано привести формулу к ПНФ и все, а вот в теории первым пунктом алгоритма приведения звучит "Исключить логические связки эквивалентности и импликации. Многократно (пока это возможно) применяется следующее правило: найти самое левое вхождение связок $\equiv$ или $\to$ и сделать замены:$F \equiv \Phi = (\neg F \vee \Phi) \wedge (F \vee \neg \Phi); F \to \Phi = \neg F \vee \Phi .$"

также определение ПНФ - "Говорят, что формула F исчисления предикатов находится в ПНФ тогда и только тогда, когда ее можно представить в форме $\zeta _1 x _1 \zeta _2 x_2 ... \zeta _r x _r M$, где каждый $\zeta _i x _i , i = 1, 2, ..., r$, есть либо $\forall x _i$, либо $\exists x _i$ и М – бескванторная формула. Иногда $\zeta _1 x _1 \zeta _2 x_2 ... \zeta _r x _r $ называют префиксом, а М – матрицей формулы F."

о вынесении $\forall y Q(y)$ (формулы в методичке написаны коряво) я пологаю что Вы имели ввиду следующее:

$$F = \exists x \forall y ((P(x) \wedge \forall z (\neg R(z))) \vee (\neg P(x) \wedge \exists z R(z)) \vee Q(y))$$

[Reef]

Прошу прошения, но не могу найти кнопку редактирования сообщения (пропала), по этому продолжу в новом...

В конце концов я совсем запутался и в результате своих "мытарств" совсем не уверен, а получилось у меня вот такое:

$$F = \exists x \forall y \forall z \exists u (P(x) \wedge \neg R(z) \wedge \neg P(x) \wedge R(u) \vee Q(y))$$

Но на общий вид ПНФ походит сильно, наверное. :)
Проверьте пожалуйста...

А тут мне вообще непонятно:

Sonic86 в сообщении #735526 писал(а):

З.Ы. Слушайте, а зачем Вы переписываете через и - оно Вам надо? Только буковок больше становится и проблем тоже... Или у Вас в задании явно написано, что нужно предикат внутри выразить только через ?

А как Вы предлагаете???

[Sonic86]

Reef в сообщении #735565 писал(а):

также определение ПНФ - "Говорят, что формула F исчисления предикатов находится в ПНФ тогда и только тогда, когда ее можно представить в форме $\zeta _1 x _1 \zeta _2 x_2 ... \zeta _r x _r M$, где каждый $\zeta _i x _i , i = 1, 2, ..., r$, есть либо $\forall x _i$, либо $\exists x _i$ и М – бескванторная формула. Иногда $\zeta _1 x _1 \zeta _2 x_2 ... \zeta _r x _r $ называют префиксом, а М – матрицей формулы F."

Значит определения у нас одинаковые.

Reef в сообщении #735565 писал(а):

В задании написано привести формулу к ПНФ и все, а вот в теории первым пунктом алгоритма приведения звучит "Исключить логические связки эквивалентности и импликации. Многократно (пока это возможно) применяется следующее правило: найти самое левое вхождение связок $\equiv$ или $\to$ и сделать замены:$F \equiv \Phi = (\neg F \vee \Phi) \wedge (F \vee \neg \Phi); F \to \Phi = \neg F \vee \Phi .$"

Ааа, тогда фигово...

Reef в сообщении #735979 писал(а):

А как Вы предлагаете???

Сейчас проверил - не получается, как я хотел (не буду ложные формулы писать). Значит придется переписывать через связки. У нас при выражении связки $\equiv$ через $\vee, \wedge, \neg$ появляется опять 2 квантора по одинаковым переменных - надо попробовать опять назвать переменные по-разному.

Reef в сообщении #735979 писал(а):

В конце концов я совсем запутался и в результате своих "мытарств" совсем не уверен, а получилось у меня вот такое:

$$F = \exists x \forall y \forall z \exists u (P(x) \wedge \neg R(z) \wedge \neg P(x) \wedge R(u) \vee Q(y))$$

ПНФ, выглядит так, но боюсь, что это неверно, поскольку $P(x) \wedge\neg P(x) = 0$ и тогда вся формула упрощалась бы до $(\forall y)Q(y)$, что явно неверно. Возможно, Вы просто где-то скобки потеряли по дороге.

Reef в сообщении #735565 писал(а):

о вынесении $\forall y Q(y)$ (формулы в методичке написаны коряво) я пологаю что Вы имели ввиду следующее:

$$F = \exists x \forall y ((P(x) \wedge \forall z (\neg R(z))) \vee (\neg P(x) \wedge \exists z R(z)) \vee Q(y))$$

Да. И в таком случае остается привести к ПНФ подформулу $(P(x) \wedge \forall z (\neg R(z))) \vee (\neg P(x) \wedge \exists z R(z))$

(Оффтоп)

Reef в сообщении #735979 писал(а):

Прошу прошения, но не могу найти кнопку редактирования сообщения (пропала), по этому продолжу в новом...

Редактирование через час пропадает во избежание троллинга...

[Reef]

Sonic86 в сообщении #736002 писал(а):

Да. И в таком случае остается привести к ПНФ подформулу

имеете ввиду вот так:

$$\forall z ( \neg R(z) \wedge P(x)) \vee \exists z ( R(z) \wedge \neg P(x))$$

затем переименовать:

$$\forall z ( \neg R(z) \wedge P(x)) \vee \exists u ( R(u) \wedge \neg P(x))$$

, если так то получится :

$$\forall z \exists u (( \neg R(z) \wedge P(x)) \vee ( R(u) \wedge \neg P(x)))$$

далее вся формула целиком:

$$$$\exists x \forall y(\forall z \exists u (( \neg R(z) \wedge P(x)) \vee ( R(u) \wedge \neg P(x))) \vee Q(y))$$

поправьте пожалуйста...

[Sonic86]

Reef в сообщении #736021 писал(а):

, если так то получится :

$$\forall z \exists z (( \neg R(z) \wedge P(x)) \vee ( R(u) \wedge \neg P(x)))$$

поправьте пожалуйста...

очепятка:надо $\exists u$ вместо $\exists z$.
И еще квантор существования $\exists u$ должен стоять вне $\forall z$. Понятно, почему?

[Reef]

Опечатку исправил. В остальном не понятно. Вы имеете ввиду: $\exists u \forall z$, т.е. местами поменять?

[Sonic86]

Reef в сообщении #736042 писал(а):

Опечатку исправил. В остальном не понятно

Сделаю подробно через замену:

$$\forall z ( \neg R(z) \wedge P(x)) \vee \exists u ( R(u) \wedge \neg P(x))$$

Замечу, что область действия квантора $\forall z$ - левая часть формулы. Обозначая левую часть за $H(x)$, получаем
($\text{подстановка}^{-1}\circ\text{вынос квантора}\circ\text{подстановка}$):

$$\forall z ( \neg R(z) \wedge P(x)) \vee \exists u ( R(u) \wedge \neg P(x))$$

$$H(x) \vee \exists u ( R(u) \wedge \neg P(x))$$

$$\exists u (H(x) \vee (R(u) \wedge \neg P(x)))$$

$$\exists u (\forall z ( \neg R(z) \wedge P(x)) \vee (R(u) \wedge \neg P(x)))$$

[Reef]

тогда получается что ко всему я сделал ошибку и в самом начале, с учетом рекомендаций получается:

$$\forall y (\exists x( \exists u (\forall z (( \neg R(z) \wedge P(x)) \vee ( R(u) \wedge \neg P(x))))) \vee Q(y))$$