Методи перевірки ТОТОЖНОЇ ХИБНОсті й тОТОЖНОЇ ІСТИННості формул логіки висловлень

Різноманітні задачі у математиці та у інших галузях можуть бути сформульовані як задачі встановлення того, чи випливає деяке твердження з заданої сукупності інших тверджень, тобто як задачі перевірки правильності міркування. Якщо твердження у міркуванні є висловленнями, то задачу перевірки правильності такого міркування можна звести до задачі перевірки логічного слідування формули логіки висловлень, що є перекладом твердження-висновку заданого міркування, з формул, що є перекладами висловлень-посилок цього міркування. Теорема 1, що сформульована вище, дає можливість замінити перевірку логічного слідування формули F з формул F₁,…,F_n перевіркою тавтологічності (або суперечності) формули, побудованої з F₁,…,F_n, F спеціальним чином. Для установлення тавтологічності (суперечності) деякої формули P логіки висловлень можна використати таблиці істинності й перевіряти істинносні значення формули P при кожній інтерпретації. Ми розглянемо інші методи перевірки тавтологічності та суперечності, які ґрунтуються на поданні формул у спеціальному вигляді, а саме у вигляді тієї чи іншої нормальної форми. Для подання формули у нормальній формі виконуються перетворення даної формули, які зберігають її істинносне значення при кожній інтерпретації.

 

Метод перевірки суперечності й тавтологічності формул шляхом зведення до диз’юнктивної та кон’юнктивної нормальної форми

    Тавтологічність формули можна перевірити шляхом зведення її до кнф. Наприклад, (P®Q) Ù ØQ ® ØP = (ØPÚQ) ÙØQ ® ØP = Ø((ØPÚQ) ÙØQ) ÚØP = Ø(ØPÚQ)ÚQÚØP = (PÙØQ) Ú Q ÚØP = (PÚ Q ÚØP) Ù(ØQÚ Q ÚØP) = 1 Ù1 = 1. Отже, формула (P®Q) Ù ØQ ® ØP є тавтологією.

    Суперечність формули можна довести шляхом перетворення її у днф. Наприклад, (P®Q)ÙØQÙP = (ØPÚQ)ÙØQÙP = (ØPÙØQÙP)Ú(QÙØQÙP) = 0Ú0 = 0. Отже, формула є суперечною.

 

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

1. До якої нормальної форми (кнф чи днф) треба звести формулу, щоб перевірити, чи є вона тотожно істинною?

2. До якої нормальної форми (кнф чи днф) треба звести формулу, щоб перевірити, чи є вона тотожно хибною?

Метод Девіса й Патнема

Метод Девіса й Патнема дає можливість перевіряти суперечність множини диз’юнктів. Він базується на чотирьох правилах.

    1. Правило тавтології. З множини диз’юнктів S вилучити усі тавтологічні диз’юнкти, якщо такі містяться у S. Позначимо множину диз’юнктів, що утворюється у результаті такого вилучення, через S¢. Якщо S¢=Æ, то дати відповідь «S несуперечна» та завершити роботу, інакше перевірити суперечність S¢.

Зазначимо, що множина S суперечна тоді й тільки тоді, коли S¢ суперечна. Отже, однократне застосування правила тавтології до множини диз’юнктів S, що містить тавтологічні диз’юнкти, або дає відповідь на питання про суперечність S (якщо S¢=Æ, то S – несуперечна), або зводить задачу про суперечність S до задачі про суперечність множини диз’юнктів S¢, яка містить менше диз’юнктів, ніж S.

    2. Правило однолітерних диз’юнктів. Якщо в S існує одиничний диз’юнкт {L}, то спочатку побудувати множину S¢, вилучаючи з S ті диз’юнкти, що містять літеру L. Якщо S¢=Æ, то дати відповідь «множина S несуперечна» й завершити роботу. Якщо S¢¹Æ, то побудувати множину S², вилучаючи з диз’юнктів множини S¢ усі входження літери ØL. Якщо S² містить порожній диз’юнкт, то дати відповідь «множина S суперечна» та завершити роботу, інакше перевірити суперечність S².

Зазначимо, що множина S суперечна тоді й тільки тоді, коли S² суперечна. Таким чином, однократне застосування правила однолітерних диз’юнктів до множини диз’юнктів, що містить одиничний диз’юнкт, або дає відповідь на питання про суперечність S (якщо S¢=Æ, то S – несуперечна, якщо cÎS², то S суперечна), або зводить задачу про суперечність S до задачі про суперечність множини диз’юнктів S², яка містить менше диз’юнктів, ніж S.

    3. Правило чистих літер. Назвемо літеру L, що входить у деякий диз’юнкт з S, чистою в S, якщо літера ØL не входить в жоден диз’юнкт з S. Якщо S містить літеру L, чисту в S, вилучити з S усі диз’юнкти, що містять L. Позначимо через S¢ множину диз’юнктів, що залишилися. Якщо S¢=Æ, то дати відповідь «S несуперечна» й завершити роботу, інакше перевірити суперечність S¢.

Зазначимо, що S суперечна тоді й тільки тоді, коли S¢ суперечна. Отже, однократне застосування правила чистих літер до множини диз’юнктів S, що містить чисту літеру, або дає відповідь на питання про суперечність S (якщо S¢=Æ, то S несуперечна), або зводить задачу про суперечність S до задачі про суперечність множини диз’юнктів S¢, яка містить менше диз’юнктів, ніж S.

    4. Правило розщеплення. Вибрати літеру L, що має входження у який-небудь диз’юнкт з S. Подати множину S у вигляді (A₁Ú L)Ù…Ù(A_mÚL)Ù(B₁ÚØL)Ù…Ù(B_nÚØL)ÙR, де m,nÎN⁺, A_i (iÎ{1,…,m}), B_j
(j Î {1,…,n}), R не містять літер L та ØL. Побудувати множини S₁ = A₁Ù…ÙA_mÙR та S₂ = B₁Ù…ÙB_nÙR. Перевірити суперечність S₁ та S₂.

Зазначимо, що S суперечна тоді й тільки тоді, коли S₁ й S₂ суперечні. Застосування правила розщеплення дає можливість звести задачу про суперечність множини диз’юнктів S до сукупності двох задач (про суперечність S₁ та про суперечність S₂), кожна з яких простіша, ніж задача про суперечність S.

    Метод Девіса й Патнема перевірки суперечності множини диз’юнктів S полягає у рекурсивному застосуванні до S правил 1-4 у зазначеному порядку.

    Розглянемо приклад. Перевіримо за допомогою методу Девіса й Патнема суперечність множини S = {ØPÚØQÚR, ØPÚQ, P, ØR, T}. За правилом 2 (з диз’юнктом {P}) маємо множину S₁ = {ØQÚR, Q, ØR, T}. За правилом 2 (з диз’юнктом {ØR}) маємо множину S₂ = {ØQ, Q, T}. За правилом 2 (з диз’юнктом {ØQ}) маємо множину S₃ = {c, T}, яка є суперечною, оскільки містить порожній диз’юнкт. Отже, початкова множина диз’юнктів S суперечна.

 

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

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 суперечна тоді й тільки тоді, коли існує вивід порожнього диз’юнкту c з S за допомогою правила резолюції.

Розглянемо приклад. Доведемо суперечність множини диз’юнктів S = {ØPÚQ, ØPÚØQÚR, P, ØR, T}, побудувавши вивід c з 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. c                                             резольвента 4 та 7.

Отже, маємо вивід ØPÚØQÚR, ØPÚQ, P, ØR, ØPÚR, R, c порожнього диз’юнкту з 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,…,. Необмежене використання правила резолюції при виведенні може призвести до породження великої кількості надлишкових (зайвих) резольвент, тобто таких диз’юнктів, що, наприклад, не входять до виводу c. Розглянемо деякі шляхи вирішення проблеми надлишкових резольвент при застосуванні метода резолюцій.

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

Диз’юнкт С називається п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 є суперечною, оскільки методом резолюцій можна побудувати вивід c з S. Дійсно:

(1) PÚQ

(2) PÚØQ

(3) ØPÚQ

(4) ØPÚØQ

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

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

(7) c          резольвента (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¹. Неважко бачити, що продовжуючи пошук вхідною резолюцією, можна побудувати лише тавтології та наддиз’юнкти тих резольвент, які одержані раніше. Отже, вхідного виведення c з S не існує.

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

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

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

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

1. Що таке резольвента двох диз’юнктів?

2. Що таке вивід порожнього диз’юнкту з множини диз’юнктів?

3. Що таке піддиз’юнкт (наддиз’юнкт) диз’юнкту?

4. Які існують засоби обмеження перебору при перевірці суперечності множини диз’юнктів методом резолюцій?

 

⇐ Предыдущая12345678910Следующая ⇒

Поделиться: