18.3. Метод резолюцій у логіці предикатів
Завдання встановлення нездійсненності безлічі пропозицій у 356 огіїки предикатів найчастіше вирішується за допомогою методу резолюцій. Попередньо одержують безліч диз'юнктів так, як було описано раніше. На відміну від логіки висловлювань, для отримання резольвенту необхідна уніфікація. Це не що інше, як отримання окремих випадків формул. Далі будують дерево спростування, як у логіці висловлювань.
Нездійсненна в окремому випадку формула не може бути здійсненна в інших випадках, так як формулазамкнута, а замкнута формула або хибна, або істинна. На цьому й ґрунтується використання методу резолюції в логіці предикатів.
Наприклад, для висновку за модусом «Barbara» при використанні формалізації [8]:
Отримуємо для висновку ААА за першою фігурою силогізму кон'юнкцію посилок та заперечення укладання: що відповідає
безлічі диз'юнктів та дереву спростування (рис. 120).
Мал. 120. Дерево спростування для модусу «Barbara»
На рис. 120 "а" - це константа, що вийшла після введення функції Сколема при запереченні укладання модусу "Barbara".
Для модусу «Darapti» (третя фігура силогізму) диз'юнкти та дерево спростування мають вигляд (рис. 121):
Мал. 121. Дерево спростування для модусу «Darapti»
Спростування не досягається, хоча модус правильний. Аналогічно не досягається спростування і для модусів Felapton і Fesapo. Виявляється, це недолік формалізації, а чи не методу резолюцій. У той самий час формалізація В.А. Смирнова [1]:
позбавлена цього недоліку. Так, для модусу "Felapton" (рис. 122):
Мал. 122. Дерево спростування для модусу «Felapton»
та моделі В.А. Смирнова
Безпосередньою перевіркою можнапереконатися в тому, що при цій формалізації метод резолюції «працює» для всіх 19 правильних основних і 5 додаткових модусів [1] і не працює для решти 232 неправильних.
На методі резолюцій заснована мова логічного програмування ПРОЛОГ.
18.4. Принцип логічного програмування
У ряді логічних завдань [29] з'ясовують, чи слід логічно деяка формула F з множини Ф0.
В інших завданнях встановлюють значення елемента x (якщо воно існує!), При якому дана формула F, що містить як один з аргументів x, випливає з Ф0, тобто. спочатку встановлюють, чи формула xF(x) з Ф0, а потім, при позитивній відповіді на це питання, визначається відповідне значення x.
Розглянемо приклад [29].
Нехай вантажний робіт (пр) розташовується на автоматичному візку (ат). Візок знаходиться на складі (скл). Потрібно відповісти на питання, де знаходиться вантажний робот.
Формалізуємо завдання, ввівши предикат:
"Бути в певному місці": Б (z, x) - "z знаходиться в x", тоді:
.
Перша формула висловлює той факт, що в якому місці не знаходився візок, в цьому ж місці знаходиться вантажний робот. Друга формула – що візок знаходиться на складі.
Необхідно довести теорему:
Рішення: отримуємо заперечення припущення: .
Отримаємо безліч диз'юнктів і застосуємо метод резолюцій:
,
Мал. 123. Дерево спростування для завдання про роботу
Таким чином, припущення випливає з гіпотез (рис. 123).
Після побудови дерева спростування для отримання відповіді на поставлене питання будуютьмодифіковане дерево докази:
1. До кожної пропозиції, що випливає з заперечення пропозиції, додаються (в сенсі диз'юнкції) її заперечення.
2. Виконуються ті самі резолюції, що і при побудові дерева спростування.
У корені модифікованого дерева докази виходить окремий випадок припущення, який і використовується як відповідь.
Мал. 124. Модифіковане дерево доказу
для завдання про роботу
Таким чином, вантажний робот знаходиться на складі.
У процесі отримання відповіді виникають тавтології (типу: ).
Проте, т.к. Тавтологію можна відкинути, не змінюючи здійсненності або нездійсненності будь-якої множини (кон'юнкція з одиницею), що містить крім тавтології інші формули, зазначені припущення випливають з аксіом.
Таким чином, модифіковане дерево спростування є графом доказу, що формула, розташована в його корені, логічно випливає з аксіом.
Описаний процес отримання відповіді можна застосовувати при автоматичному побудові простих програм для ЕОМ.
Нехай задані відносини R(x,y) між x і y деяким безліччю аксіом, а також елементарні функції, що визначаються іншою множиною аксіом. Потрібно написати програму, яка за заданими вхідними значеннями видає на виході значення y, що задовольняє значення R(x, y). При написанні можна використовувати задані елементарні функції.
Необхідну програму можна побудувати за допомогою процесу отримання відповіді, після того як буде доведено, що припущення
