1.4. Метод резолюцій

Основна ідея методу резолюцій, який розглядається у логіці висловлень, зберігається і у логіці предикатів. Нагадаємо основні означення і факти.

Бінарною резольвентою R(D_l, D₂) двох диз’юнктів D_l і D₂ називається диз’юнкція літералів, що залишається після видалення пари контрарних.

Наприклад, якщо D_l = р₁, D₂= , то R(D₁,D₂) = q. Тут резольвента є висновком, який отримується за правилом modus ponens з посилок р та . Аналогічно резольвента D₁= і D₂= ілюструє правило силогізму: R(D₁,D₂) = . Отже, правило резолюції, яке відкрив Дж. Робінсон (1965 p.), є сильнішим з усіх схем логічного висновку, якими користується людина. Це випливає з теореми, яка справедлива у самому загальному випадку.

Теорема. Якщо для диз’юнктів D_l і D₂ існує резольвента R(D₁,D₂), то вона є логічним наслідком цих диз’юнктів: D_l, D₂ R(D₁,D₂).

Множина диз’юнктів D_l,D₂,...D_n називається невиконуваною, якщо формула тотожно хибна.

Якщо можна встановити, що деяка формула F хибна, то можна відповісти, чи є логічне слідування А₁, А₂, …, А_n B, оскільки для цього потрібно дослідити, чи буде формула хибною.

Методом резолюцій називається послідовне отримання бінарних резольвент із заданих диз’юнктів та з усіх тих, що утворюються. [2, ст.30]

Застосовуючи метод резолюцій, можна отримати резольвенту, у якій не залишиться жодного літерала. Кажуть, що отримали порожній диз’юнкт □.

Теорема (про повноту методу резолюцій) Множина диз’юнктів S не виконувана тоді і тільки тоді, коли у результаті застосування методу резолюцій до множини S отримується порожній диз’юнкт □.

Є багато різних процедур для реалізації методу резолюцій: локрезолюція, метод насичення рівня, стратегія викреслювання тощо.

У логіці предикатів для дослідження невиконуваності множини диз’юнктів потрібно провести додаткову процедуру уніфікації формул. Тут літералом є елементарна формула, терми якої можуть містити змінні, сталі або вирази із функціональних символів і термів. P(x,f(y),b), приклади літералів.

Підстановкою у літерали термів замість змінних можна отримати різні частинні випадки (приклади) літерала. Наприклад, частинними випадком першого літерала можуть бути P(z,f(a),b), P(g(z),f(c),b), P(с,f(a),b). Останній частинний випадок називається атомом, бо не містить змінних. Підстановку терма t замість змінної х позначають Одночасно можна виконати кілька замін. їх групують у підстановку. Наприклад, перший частинний випадок отримано у результаті підстановки другий - , третій . У загальному випадку де всі - різні змінні, - терми. Застосування підстановки до літерала позначають Р₀. Послідовне виконання двох підстановок та дає третю .

Множина літералів {L₁,L₂,...L_n} називається уніфікованою, якщо існує така підстановка , що Підстановка називається уніфікатором множини літералів {L_i}. Уніфікатор множини формул називається найзагальнішим, якщо для кожного уніфікатора цієї множини існує підстановка , що .

Існує алгоритм уніфікації, який починає роботу з порожньої підстановки і крок за кроком знаходить множину неузгодженості в літералах і будує найзагальніший уніфікатор, якщо він є. Наприклад, для літералів L₁=P(x,f(y),b) та L₂=P(a,f(b),b) перша множина неузгодженості W₁={x,a). Щоб ліквідувати неузгодженість, робимо підстановку =P{a,f(y),b), =P(a,f(b),b). Друга множина неузгодженості W₂={y,b}. Після підстановки у новоутворені літерали отримаємо однакові літерали. Отже, є найзагальнішим уніфікатором. Кожен елемент множини неузгодженості повинен бути термом або літералом. Якщо множина неузгодженості не містить змінних, то така множина літералів не уніфікується. [2, ст. 32]

Нехай деякий диз’юнкт D містить літерали для яких існує спільний уніфікатор. Тоді замість к літералів залишають один і така процедура називається склейкою.

Нехай є два диз’юнкти і і всі змінні у них різні. Диз’юнкт , містить літерал , а диз’юнкт містить літерал , причому існує уніфікатор такий, що . Бінарною резольвентою і у логіці предикатів називається диз’юнкція літералів, які залишаються після викреслювання уніфікованих.

Перед побудовою резольвент спочатку виконують склейку у кожному диз’юнкті (якщо це можливо). У логіці предикатів теж справедлива теорема про повноту методу резолюцій. Наприклад, для перевірки логічного слідування ⊨ методом резолюцій потрібно:

1. Утворити формулу . При цьому у кожній посилці та висновку змінні перейменувати, позначивши усі різними буквами, оскільки вони можуть мати різний зміст.

2. Знайти сколемівську стандартну форму цієї формули і записати її матрицю у кон’юнктивній нормальній формі ;

3. До множини диз’юнктів застосувати метод резолюцій провівши, за необхідності, уніфікацію літералів. Якщо у результаті побудови всіх можливих резольвент отримується порожній диз’юнкт □, то множина диз’юнктів невиконувана, формули і тотожно хибні, отже, є логічне слідування.