VPF::Правило резолюций - Форум программистов

Cheloveck

Дата 30.10.2010, 17:08 (ссылка)

(нет голосов)

Загрузка ...

Эксперт

Профиль
Группа: Завсегдатай
Сообщений: 1578
Регистрация: 26.7.2008
Где: Тула

Репутация: нет
Всего: 32

Пытаюсь разобраться с правилом резолюций. В принципе, всё понятно, кроме одного. Что делают с кванторами.
Вот стандартный пример:

Цитата

Человек - это живое существо;
Все живые существа смертны;
Сократ - человек.

Доказать: Сократ смертен.

Не трудно записать это в виде формул логики предикатов.

Код


∀x(Человек(x) ⊃ ЖивоеСущество(x)).
∀y(ЖивоеСущество(y) ⊃ Смертно(y)).

И цель

Код


Человек(Сократ).

доказывает, что Сократ смертен.

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

Цитата

2. Человек, читающий книги, - неглуп
Предикат: ∀Y(read(Y) ⊃ smart(Y))
Дизъюнктивная форма: ¬read(Y) ∧ smart(Y)

А на втором:

Цитата

Предикат: ∀x(Человек(x) ⊃ Живое_Существо(x)).
Дизъюнктивная форма: ¬(Человек(x) ∨ Живое_Существо(x))

Может кто-нибудь объяснить, каким волшебным образом получают дизъюнктивную форму из предикатной, и почему в двух примерах они на столько разные? Подскажите хотя бы ресурс, на котором об этом можно почитать. А то, везде есть примеры, а как это сделано - не написано.

Это сообщение отредактировал(а) Cheloveck - 30.10.2010, 17:12

--------------------

Cheloveck

Дата 30.10.2010, 21:05 (ссылка)

(нет голосов)

Загрузка ...

Эксперт

Профиль
Группа: Завсегдатай
Сообщений: 1578
Регистрация: 26.7.2008
Где: Тула

Репутация: нет
Всего: 32

--------------------

Cheloveck

Дата 30.10.2010, 21:24 (ссылка)

(нет голосов)

Загрузка ...

Эксперт

Профиль
Группа: Завсегдатай
Сообщений: 1578
Регистрация: 26.7.2008
Где: Тула

Репутация: нет
Всего: 32

Нашёл ещё один вариант, который, как мне кажется, верный
http://books.google.ru/books?id=jaoDX9-e_M...%22&f=false

Это сообщение отредактировал(а) Cheloveck - 30.10.2010, 21:25

--------------------

Cheloveck

Дата 30.10.2010, 23:56 (ссылка)

(нет голосов)

Загрузка ...

Эксперт

Профиль
Группа: Завсегдатай
Сообщений: 1578
Регистрация: 26.7.2008
Где: Тула

Репутация: нет
Всего: 32

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

Цитата

Атомарные предикаты:
P(x): x является человеком;
Q(x): x является живым существом;
R(x): x смертен.

Общезначимые утверждения (предикатная форма):
∀x(P(x) ⊃ Q(x));
∀y(Q(y) ⊃ R(y));
P(Сократ).

Общезначимые утверждения (дизъюнктивная форма):
¬P(x) ∨ Q(x);
¬Q(y) ∨ R(y);
P(Сократ).

Цель:
R(Сократ).

Конъюнкция всех дизъюнктов и отрицания цели:
(¬P(x) ∨ Q(x)) ∧ (¬Q(y) ∨ R(y)) ∧ P(Сократ) ∧ ¬R(Сократ).

Применение правила резолюций:
+-----------------+-----------------+
| Первый дизъюнкт | Второй дизъюнкт |
+-----------------+-----------------+
| ¬P(x) ∨ Q(x)    | ¬Q(y) ∨ R(y)    |
+-----------------+-----------------+
| Резольвента: ¬P(y) ∨ R(y)         |
+-----------------+-----------------+
| ¬P(y) ∨ R(y)    | P(Сократ)       |
+-----------------+-----------------+
| Резольвента: R(Сократ)            |
+-----------------+-----------------+
| R(Сократ)       | ¬R(Сократ)      |
+-----------------+-----------------+
| Пустая резольвента.               |
+-----------------------------------+

Из чего следует, что отрицание предположения не верно, а значит само предположение истина.

Это сообщение отредактировал(а) Cheloveck - 31.10.2010, 14:05

--------------------

1 Пользователей читают эту тему (1 Гостей и 0 Скрытых Пользователей)
0 Пользователей:
« Предыдущая тема \| Алгоритмы \| Следующая тема »