2.6. Метод резолюций для исчисления предикатов

В случае исчисления предикатов резолютивный вывод касается бескванторных формул, но под литерой дизъюнкта надо понимать элементарную формулу, в которую в качестве аргу­ментов предикатного символа могут входить различные термы. Это усложняет ситуацию, поскольку один предикатный символ в зависимости от комбинации термов в его аргументах может давать разные истинностные значения. Но правило резолюций остается тем же: если есть дизъюнкты pV D_iи ¬pV D_j, то их заменяем резольвентой D_iV D_j. Здесьp– некоторая элементарная формула.

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

Унификация – процедура, позволяющая (при некоторых условиях) сохранять свойство про­тиворечивости, но при этом согласовывать аргументы у одинаковых предикатных символов.

2.7. Пример решения задачи на логический вывод методом резолюций

Область определения: люди.

1. Те, кто нарушает свои обещания, не заслуживают доверия. 2. Любители выпить очень общительны. 3. Человек, выполняющий свои обещания, честен. 4. Ни один трезвенник не ростовщик. 5. Тому, кто очень общителен, всегда можно верить.

Заключение:ни один ростовщик не бывает нечестен.

Этот вывод необходимо доказать методом резолюций, т.к. как он далеко не очевиден. Напомним, что для автоматизации подобных задач существует язык алгоритмического программирования – ПРОЛОГ.

В нашем случае, мы должны записать вывод в виде логики предикатов в НДФ, но в виде инверсии, т.е. построить доказательство методом от противного. Если в процессе дедуктивного вывода методом резолюций мы придем к противоречию (получим пустой дизъюнкт П), то наше предположение ложно и, следовательно, заключение является истинным, т.е. задача решена – мы доказали истинность заключения.

Решение:

Н – нарушает обещание

Д – доверие

Л – любители выпить

О – общительные

Ч – честен

Р – ростовщик

Нне Д преобразуя, получим не Нне Д (1)

ЛО преобразуя, получим не ЛО (2)

не НЧ преобразуя, получим НЧ (3)

не Лне Р преобразуя, получим Лне Р (4)

ОД преобразуя, получим не ОД (5)

Резолюция

РЧ преобразуя получим не PЧ (6)

Для доказательства от противного инвертируем формулу резолюции

Не (не P Ч) преобразуя получим P и не Ч (7)

Но (7) истинно, если истинны конъюнкты

P (8)

и не Ч (9)

Итак, формулы 1-5 и 8,9 – исходные формулы.

По правилу получения резольвент имеем:

Из 1 и 3 получим резольвенту не Д Ч (10)

Из 1 и 5 получим резольвенту не Н не О (11)

Из 2 и 4 получим резольвенту О не Р (12)

Из 2 и 5 получим резольвенту не Л Д (13)

Из 2 и 5 получим резольвенту не Н не Р (14)

Из 3 и 9 получим резольвенту Н (15)

Из 14 и 8 получим резольвенту не Н (16)

Из 15 и 16 получим резольвенту П (пустой дизъюнкт)

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

Существует и другой, более простой метод проведения логического вывода с помощью таблицы истинности. Проиллюстрируем его с помощью табл.2.

Таблица 2

Логический вывод с помощью таблицы истинности

Н	Д	Л	О	Ч	Р	если Н то не Д	если Л то О	если не Н то Ч	если не Л то не Р	если О то Д	если Р то Ч
0	0	0	0	0	0	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА
0	0	0	0	0	1	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА	ЛОЖЬ
0	0	0	0	1	0	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА
0	0	0	1	0	0	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ЛОЖЬ	ИСТИНА
0	0	1	0	0	0	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА
0	1	0	0	0	0	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА
1	0	0	0	0	0	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА
0	0	0	0	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА
0	0	0	1	0	1	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ЛОЖЬ	ЛОЖЬ
0	0	1	0	0	1	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА	ИСТИНА	ЛОЖЬ
0	1	0	0	0	1	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА	ЛОЖЬ
1	0	0	0	0	1	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА	ЛОЖЬ
0	0	0	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА
0	0	1	0	1	1	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА
0	1	0	0	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА
1	0	0	0	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА
0	0	1	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА
0	1	0	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА	ИСТИНА
1	0	0	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ЛОЖЬ	ИСТИНА
0	1	1	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА
1	0	1	1	1	1	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ЛОЖЬ	ИСТИНА
1	1	1	1	1	1	ЛОЖЬ	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА	ИСТИНА

В данной таблице можно выделить (выделено цветом) две зоны: первая соответствует наборам значений одноместных предикатов {Н Д Л О Ч Р}, а вторая – значениям соответствующих логических выражений. Заключение является верным, если во второй зоне таблицы найдется строка, все ячейки которой содержат значение «ИСТИННО». В таблице две подобных строки, следовательно, заключение доказано.

Этот метод является эвристическими и нагляден при относительно небольшом наборе входных переменных.

Задание.

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

Теория вопроса (кратко)

Постановка задачи (по заданию преподавателя)

Процесс решения (подробно)

Заключение (четкий ответ на вопрос: как удалось получить решение и каково оно)

Ссылки на литературу (конкретно)