Перевірка правильності міркування методом Девіса й Патнема

За допомогою методу Девіса й Патнема перевіряється суперечність формули, поданої у вигляді множини диз’юнктів. Розглянемо задачу (2) (стор. 38). За відомим твердженням (п.2 теореми 1) формула BÚDÚH є логічним наслідком формул A®B, C®D, G®H, AÚCÚG, якщо формула

F = (A®B)Ù(C®D)Ù(G®H)Ù(AÚCÚG)ÙØ(BÚDÚH)

є суперечністю.

    Щоб застосувати метод Девіса й Патнема для розв’язання цієї задачі, необхідно спочатку привести подану формулу до КНФ, а потім побудувати множину диз’юнктів за цією КНФ.

    Перетворимо формулу

(A®B)Ù(C®D)Ù(G®H)Ù(AÚCÚG)ÙØ(BÚDÚH)

у КНФ частинами:

1) (A®B) = ØAÚB;

2) (C®D) = ØCÚD;

3) (G®H) = ØGÚH;

4) Ø(BÚDÚH) = ØВÙØDÙØH.

Отже, маємо множину диз’юнктів: S={ØAÚB, ØCÚD, ØGÚH, AÚCÚG, ØВ, ØD, ØH}, до якої вже можна застосувати метод Девіса й Патнема. Далі ми будемо розглядати диз’юнкти як множини літер.

Перше правило (правило тавтології) не застосовне (множина S не містить тавтологічних диз’юнктів), тому використовуємо друге правило. Спочатку виберемо у множині S одиничний диз’юнкт (нехай це буде диз’юнкт {ØH}), потім викреслюємо з множини S усі диз’юнкти, що містять літеру ØH. У даному випадку такий диз’юнкт тільки один. Маємо множину S₁={ØAÚB, ØCÚD, ØGÚH, AÚCÚG, ØВ, ØD}. Множина S₁ не порожня, отже, тепер треба вилучити з диз’юнктів, що входять в S₁, усі входження літери H. Таке входження тільки одне. Після вилучення маємо множину S₂={ØAÚB, ØCÚD, ØG, AÚCÚG, ØВ, ØD}. Множина S₂ не містить порожнього диз’юнкту, отже, застосовуємо до неї метод Девіса й Патнема, оскільки S суперечна тоді й тільки тоді, коли суперечна S₂. Правило тавтології не застосовне до S₂. За правилом 2 (з диз’юнктом {ØB}), вилучивши з S₂ диз’юнкт {ØB}, побудуємо множину S₃={ØAÚB, ØCÚD, ØG, AÚCÚG, ØD}, яка не є порожньою. Маємо вилучити з диз’юнктів множини S₃ усі входження літери, контрарної до літери ØB, тобто літери В. Маємо множину S₄={ØA, ØCÚD, ØG, AÚCÚG, ØD}. Ця множина не містить порожнього диз’юнкту, отже, до неї застосовуємо метод Девіса й Патнема. Шукаємо перше правило, що застосовне до S₄. Це правило однолітерних диз’юнктів. За цим правилом (з диз’юнктом {ØA}) маємо множину S₅={ØCÚD, ØG, AÚCÚG, ØD}. Множина S₅ не порожня, тому вилучаємо з диз’юнктів цієї множини усі входження літери A. Маємо множину S₆={ØCÚD, ØG, CÚG, ØD}. Оскільки S₆ не містить порожнього диз’юнкту, застосовуємо до неї метод Девіса й Патнема. За правилом 2 (з диз’юнктом {ØD}) маємо множину S₇={ØCÚD, ØG, CÚG}. Оскільки S₇ не порожня, вилучаємо з диз’юнктів цієї множини усі входження літери D. Маємо множину S₈={ØC, ØG, CÚG}. Оскільки S₈ не містить порожнього диз’юнкту, перевіряємо її суперечність. За правилом 2 (з диз’юнктом {ØС}) маємо множину S₉={ØG, CÚG}. Оскільки ця множина не порожня, вилучаємо входження літери С з диз’юнктів цієї множини. Маємо множину S₁₀={ØG, G}. Оскільки S₁₀ не містить порожнього диз’юнкту, перевіряємо її суперечність. За правилом 2 (з диз’юнктом {ØG}) маємо множину S₁₁={G}. Оскільки ця множина не порожня, вилучаємо входження літери G з єдиного диз’юнкту {G}, що міститься у S₁₁. Маємо множину S₁₂={c}, яка є суперечною, бо містить порожній диз’юнкт. Отже, й початкова множина диз’юнктів S суперечна.

Таким чином, формула

(A®B)Ù(C®D)Ù(G®H)Ù(AÚCÚG)ÙØ(BÚDÚH)

є суперечною, тому формула BÚDÚH є логічним наслідком формул A®B, C®D, G®H, AÚCÚG. Отже, задане міркування є логічно правильним.

 

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

Поделиться: