Page 42 - 6109

Літерали L та ~L є протилежними. Кажуть, що дві фрази містять
контрарну пару атомарних формул (або просто контрарну пару), якщо одна з
них включає деяку атомарну формулу без заперечення, а інша – ту саму
формулу під знаком заперечення.
На основі цього правило резолюцій можна подати, як:
Дві фрази, що містять контрарну пару, можуть бути резольвовані одна з
іншою, і результатом резолюції (резольвентою) є диз'юнкція літералів, які
залишаються в обох фразах після викреслення контрарної пари. Тобто із
диз’юнктів XF та ~XG виводимо диз’юнкт FG.
Слід відмітити, що правило резолюцій завжди зберігає істинність. Це
означає, що якщо (XF)=1 та (~XG)=1 для деякої інтерпретації , то і
(FG)=1.
Правило резолюцій необов’язково застосовувати до крайніх лівих
диз’юнктів. Оскільки, ми не розрізняємо диз’юнкти, що відрізняються
порядком запису літералів.
Нехай S – множина диз’юнктів. Виводом з S називається послідовність
диз’юнктів D 1, D 2, …,D n така, що кожний диз’юнкт цієї послідовності належить
S або слідує їх попередніх за правилом резолюцій. Диз’юнкт D виводиться з S,

якщо існує вивід S, останнім диз’юнктом якого є D.
Наприклад, S={~X  Y  Z, ~Y  U, X} D 1 =…., D 5 = Z  U. Диз’юнкт Z  U
виводиться з S.
Застосування методу резолюцій базується на наступному твердженні:
Множина диз’юнктів логіки висловлювань S невиконувана тоді і тільки тоді,
коли з виводимо пустий диз’юнкт.
Для доведення того, що формула G є логічним наслідком формул F 1,…,
F n метод резолюцій застосовується наступним чином. Спочатку складається
множина формул T = {F 1,…,F n, ~G}. Потім кожна з цих формул приводиться до
кон’юктивної нормальної форми і в отриманих формулах викреслюються знаки
кон’юнкції. Отримується множина диз’юнктів S, та здійснюється вивід пустого
диз’юнкту з S. Якщо пустий диз’юнкт виводиться з S, то формула G є логічним
наслідком формул F 1,…,F n. Якщо вивести з S неможливо, то формула G не є
логічним наслідком формул F 1,…,F n.
Нехай з S виводимо . Припустимо протилежне  множина S виконувана,
тобто існує інтепритація , при якій всі дизюнкти істинні. Виводимість із S
означає, що існує послідовність D 1, D 2, …, D n = , кожний дизюнкт якої
належить S або отримується з попередніх за методом резолюцій. Якщо D j
належить та за припущенням (D j)=1, якщо отримується з попередніх то також

(D j)=1 (правило зберігає істинність) при j = n ( )=1  що протиречить.
Наприклад, довести, що формула G=Z, є логічним наслідком формул
(приклад 1)
F 1=~X  Y  X  Z,
F 2 = ~Y  Z
Оскільки в логіці предикатів, в диз’юнктах можуть бути змінні, то
попереднє правило резолюцій вже не підходить. Дійсно, множина диз’юнктів
S={P(x), ~P(x)} не виконувана (передбачається що змінна зв’язана квантором

42