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

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

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

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

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

Множина диз’юнктів Dl, D2,… Dn називається невиконуваною, якщо формула тотожно хибна.

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

Методом резолюцій називається послідовне отримання бінарних резольвент із заданих диз’юнктів та з усіх тих, що утворюються. [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 замість змінної х позначають Одночасно можна виконати кілька замін. їх групують у підстановку. Наприклад, перший частинний випадок отримано у результаті підстановки другий – , третій . У загальному випадку де всі – різні змінні, – терми. Застосування підстановки до літерала позначають Р0. Послідовне виконання двох підстановок та дає третю .

Множина літералів {L1, L2,… Ln} називається уніфікованою, якщо існує така підстановка , що Підстановка називається уніфікатором множини літералів {Li}. Уніфікатор множини формул називається найзагальнішим, якщо для кожного уніфікатора цієї множини існує підстановка, що .

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

Рекомендуємо почитати:

Поновлення бібліотечних фондів на сучасному етапі
За законом України бібліотеки мають пріоритетне право на придбання книг, документів, інших носіїв інформації відповідно до профілю комплектування їх фондів. Це право забезпечується одержанн ...

Типологія уроків літератури з мультимедійною підтримкою
Специфіка підготовки уроку - презентації безумовно визначається типом уроку. У нашій практиці використовуються: Уроки-лекції Інформаційно-комунікаційні технології на цьому типі уроку роблят ...

Ступені роботи над текстовими задачами
Розв'язати математичну задачу – це значить знайти таку послідовність загальних положень математики (означень, аксіом, теорем, правил, законів, формул), використовуючи які до умов задачі чи ...