Контрольні питання

1. Для розв’язання якої задачі застосовується метод Девіса й Патнема?

2. Яка літера називається чистою у множині диз’юнктів?

3. На яких правилах перетворення множини диз’юнктів ґрунтується метод Девіса й Патнема?

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

Правило резолюції. Нехай С₁, С₂ – диз’юнкти й С₁=D₁L, С₂=D₂L, де D₁, D₂ – диз’юнкції літер, можливо, порожні, L, L – контрарні літери. Будемо говорити, що диз’юнкт C=D₁D₂ утворюється за допомогою правила резолюції з диз’юнктів С₁ та С₂. Диз’юнкт С називається резольвентою диз’юнктів С₁ та С₂.

Розглянемо приклад. Застосуємо правило резолюції до диз’юнктів С₁ = RQ та С₂ = QP й побудуємо їх резольвенту. Оскільки С₁ та С₂ містять відповідно літери Q та Q, що складають контрарну пару літер, до них застосовне правило резолюції. Маємо резольвенту С = RP диз’юнктів С₁ та С₂.

Теорема 2. Нехай С₁, С₂ – диз’юнкти, С – резольвента С₁ та С₂. Тоді С є логічним наслідком С₁ та С₂.

Будемо говорити, що порожній диз’юнкт c виводиться з множини диз’юнктів S (або існує вивід диз’юнкту c з множини диз’юнктів S) за допомогою правила резолюції, якщо існує така скінченна послідовність диз’юнктів С₁,…,С_k, що С_k= c й кожен диз’юнкт С_i даної послідовності (1ik) є або диз’юнктом з множини S, або резольвентою таких диз’юнктів C_n, C_m даної послідовності, що n<і та m<i. Послідовність С₁,…,С_k, що задовольняє наведені умови, назвемо виводом порожнього диз’юнкту з множини диз’юнктів S за допомогою правила резолюції.

За допомогою правила резолюції можна доводити суперечність формул логіки висловлень. Основою для цього є така теорема.

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

Розглянемо приклад. Доведемо суперечність множини диз’юнктів S = {PQ, PQR, P, R, T, побудувавши вивід  з S за допомогою правила резолюції.

1. PQR диз’юнкт в S

2. PQ диз’юнкт в S

3. P диз’юнкт в S

4. R диз’юнкт в S

5. T диз’юнкт в S

6. PR резольвента 1 та 2

7. R резольвента 3 та 6

8.  резольвента 4 та 7.

Отже, маємо вивід PQR, PQ, P, R, PR, R,  порожнього диз’юнкту з S за допомогою правила резолюції, а це означає, що множина S суперечна.

Засоби обмеження перебору при застосуванні правила резолюції. Для доведення суперечності множини диз’юнктів S за допомогою правила резолюції достатньо знайти вивід порожнього диз’юнкту з S. Для доведення несуперечності множини диз’юнктів S за допомогою правила резолюції треба переконатися, що не існує виводу порожнього диз’юнкту з множини S. Перевірка суперечності множини диз’юнктів S методом резолюцій, тобто пошук виведення з S порожнього диз’юнкту за допомогою правила резолюції, може бути організована за таким планом. Спочатку будуємо усі резольвенти усіх пар диз’юнктів з S, поповнюємо множину диз’юнктів, включаючи у неї побудовані резольвенти, знову будуємо резольвенти й повторюємо описаний процес доти, поки не буде побудовано порожній диз’юнкт або виникають нові резольвенти (тобто такі, що не збігаються з побудованими раніше). Це означає, що послідовно породжуються множини S⁰, S¹, S²,…, де S⁰=S, Sⁿ={R: R є резольвента C₁ та C₂, C₁(S⁰…S^n-1), C₂S^n-1}, n=1,2,…,. Необмежене використання правила резолюції при виведенні може призвести до породження великої кількості надлишкових (зайвих) резольвент, тобто таких диз’юнктів, що, наприклад, не входять до виводу . Розглянемо деякі шляхи вирішення проблеми надлишкових резольвент при застосуванні метода резолюцій.

Стратегія викреслювання. Ця стратегія виникла як узагальнення правила тавтології Девіса й Патнема. Визначимо деякі допоміжні поняття.

Диз’юнкт С називається пiддиз’юнктом D (або таким, що поглинає D), якщо CD (нагадаємо, що вирази “множина літер” та “диз’юнкт” вважаються синонімами). Диз’юнкт D називається наддиз’юнктом С.

Зазначимо, що коли D збігається з С, то D є наддиз’юнктом С.

Нехай, наприклад, C=QR, D=QPR (тобто C={Q,R}, D={Q,P,R}). Оскільки {Q,R}{Q,P,R}, тобто СD, то C є піддиз’юнктом D, або С поглинає D, а D є наддиз’юнктом С.

Стратегія викреслювання полягає у вилученні з множини диз’юнктів усіх тавтологій та диз’юнктів, що є наддиз’юнктами інших диз’юнктів. Розглянемо один з різновидів стратегії викреслювання, який є повним у тому розумінні, що при його застосуванні до множини диз’юнктів S вивід порожнього диз’юнкту існує тоді й тільки тоді, коли множина S суперечна. Нехай побудована множина (S⁰…S^n-1). Обчислюємо резольвенти, вибираючи по порядку диз’юнкт C₁ з множини (S⁰…S^n-1) й диз’юнкт C₂ з множини S^n-1. Якщо С₁,С₂S^n-1, то С₁ має передувати С₂. Якщо резольвента R диз’юнктів С₁ та С₂ існує, то вона включається у множину Sⁿ у тому випадку, коли R не є тавтологією й не поглинається деяким раніше побудованим диз’юнктом.

Стратегія вхідної резолюції. Дана стратегія базується на обмеженні використання правила резолюції: хоча б одна з двох посилок правила при побудові резольвенти має бути диз’юнктом з висхідної множини диз’юнктів. Назвемо таке правило виводу вхідною резолюцією, а виведення, у якому будь-яке застосування правила резолюції є вхідною резолюцією, – вхідним виведенням.

Розглянемо приклад, який показує, що стратегія вхідної резолюції не є повною. Нехай S={PQ,PQ,PQ,PQ}. Множина S є суперечною, оскільки методом резолюцій можна побудувати вивід  з S. Дійсно:

(1) PQ

(2) PQ

(3) PQ

(4) PQ

(5) Р резольвента (1) та (2)

(6) P резольвента (3) та (4)

(7)  резольвента (5) та (6)

Застосуємо до S стратегію вхідної резолюції. Резольвенти, що є тавтологіями та наддиз’юнктами, викреслюються й у виведенні не показані. Праворуч від резольвент вказані номери диз’юнктів-посилок.

(1) PQ

(2) PQ

(3) PQ

(4) PQ

(5) Р (1), (2)

(6) Q (1), (3)

(7) Q (2), (4)

(8) Р (3), (4)

Диз’юнкти (5)–(8) – це диз’юнкти множини S¹. Неважко бачити, що продовжуючи пошук вхідною резолюцією, можна побудувати лише тавтології та наддиз’юнкти тих резольвент, які одержані раніше. Отже, вхідного виведення  з S не існує.

Стратегія одиничної резолюції. Дана стратегія базується на такому обмеженні використання правила резолюції: хоча б одна з двох посилок правила при побудові резольвенти має бути одиничним диз’юнктом. Назвемо таке правило виводу одиничною резолюцією, а виведення, у якому будь-яке застосування правила резолюції є одиничною резолюцією, – одиничним виведенням. Зв’язок між стратегіями одиничної та вхідної резолюції зрозумілий з такої теореми.

Теорема 4. Для даної множини диз’юнктів S одиничне виведення  існує тоді й тільки тоді, коли існує вхідне виведення .

Як показано вище, стратегія вхідної резолюції не є повною, отже, згідно з наведеною теоремою, стратегія одиничної резолюції теж не є повною.