Преобразование логической формулы

[magneton_bora]

Здравствуйте.

Помогите, пожалуйста, разобраться.

Имеется следующее задание:
Преобразовать формулу, данную ниже, в форму, которая пригодна для процедур вывода.
Использовать правило Modus Ponens.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$

Ход решения.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$

Дадим всем переменным при кванторах уникальные имена.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists z W(z,x))$

Перенесем все кванторы в одну сторону.

$\forall x \forall y \exists z(P(y) \Rightarrow U(x,y)) \Rightarrow (W(z,x))$

Квантор существования заменим уникальной сколемовской функцией.

$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Опустим кванторы общности.

$(P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Выполним преобразования.

$(\neg P(y) \vee U(x,y)) \Rightarrow W(F(z),x)$

$\neg (\neg P(y) \vee U(x,y)) \vee W(F(z),x)$

$P(y) \wedge \neg U(x,y) \vee W(F(z),x)$

$\neg U(x,y) \wedge P(y) \vee W(F(z),x)$

Я сделал данные преобразования. И теперь вопросы.

1. Мне не ясно что значит "форма пригодная для процедур вывода"? Это форма Хорна или что?
2. Что значит использовать правило Modus Ponens в данном контексте?
3. Верное ли решение?

Заранее спасибо.

[Sonic86]

magneton_bora в сообщении #713131 писал(а):

$\forall x \forall y \exists z(P(y) \Rightarrow U(x,y)) \Rightarrow (W(z,x))$

Квантор существования заменим уникальной сколемовской функцией.

$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Надо писать не $F(z)$, а $F(x)$.
В остальном вроде верно.

magneton_bora в сообщении #713131 писал(а):

Мне не ясно что значит "форма пригодная для процедур вывода"? Это форма Хорна или что?

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

magneton_bora в сообщении #713131 писал(а):

Что значит использовать правило Modus Ponens в данном контексте?

Может быть задание неполно?

[magneton_bora]

Цитата:

Надо писать не $F(z)$, а $F(x)$.

Хорошо, а почему?

Цитата:

Может быть задание неполно?

Исходное задание звучит следующим образом.
Transform the formula, given below, into a form that is appropriate for inference procedures applying the Modus Ponens inference rule.
Вот и пишу, потому что не могу понять что тут имеется в виду под "applying the Modus Ponens inference rule".

[Sonic86]

magneton_bora в сообщении #713144 писал(а):

Хорошо, а почему?

Ну хотя бы так. Вы эквивалентно преобразуете замкнутую формулу

magneton_bora в сообщении #713131 писал(а):

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$

в формулу со свободной переменной $z$

magneton_bora в сообщении #713131 писал(а):

$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Некорректно же. Посмотрите процедуру сколемизации, если хочется смысл понять - возьмите конкретный пример (например, для любого эпсилон, существует эн зависящее от эпсилон... - двух кванторов и одного предиката хватит)

magneton_bora в сообщении #713144 писал(а):

Transform the formula, given below, into a form that is appropriate for inference procedures applying the Modus Ponens inference rule.

Вот я Inglish плохо знаю, но понял так: привести формулу к форме, пригодную к процедуре вывода, использующей [только] Modus Ponens (т.е. правил вывода с кванторами нету). Отсюда действительно следует, что нам надо избавиться от кванторов. Если сомневаетесь, можете уточнить здесь: topic10065-375.html