Page 44 - 6109

належить S або виводиться з попередніх за правилом резолюцій або з
попереднього за правилом зклейки. Відповідно D виводиться із S, якщо існує
вивід із S посліднім дизюнктом якого є D.
Наприклад, (приклад 5)
S={~B(x)~C(x)T(f(x)), C(y)T(f(z)), B(a)}
D 1=~B(x)~C(x)T(f(x))
D 2= C(y)T(f(z))
D 3=~B(x)~T(f(x))T(f(z)) резолюція D 1 та D 2 з підстановкою y=x

D 4=~B(x)~T(f(x)) із D 3 за правилом зклейки
D 5= B(a)
D 6=~T(f(a)) резолюція D 4 та D 5 з підстановкою x=a.
Існують формальні алгоритми, які дозволяють отримувати найбільш
загальний уніфікатор. Але у більшості випадків достатньо деяких
неформальних простих правил.
1. Будь-який терм зіставляється сам з собою.
Наприклад, дві фрази Ρ(α)~Q(b, с) та Q(b, с)~R(b, с), є резольвовані, і
резольвента записується як Ρ(α)~R(b, с).
2. Різні константи не зіставляються одна з одною.
Тому фрази Ρ(α)~Q(b, с) та Q(c, с)~R(b, с) не є резольвованими.
3. Змінна може бути замінена константою або іншим термом.
Так, фрази Ρ(α)~Q(a, b) та Q(x, y)~R(x, y), резольвується, при цьому
змінна x зіставляється з константою а, змінна у – з константою b. У резольвенті
Ρ(α) ~R(а, b) змінні замінені на константи, з якими вони зіставлялися.
Якщо в процесі виведення утворилися фрази Ρ(а) та ~Ρ(а), їх резолюцією

є пустий диз'юнкт (тотожна хибність, позначається ). Саме виведення
пустого диз'юнкта і означає суперечливість теорії.
Наприклад,
F 1 = x[P(x)  y(C(y)  Z(x, y))]
F 2 = xy(P(x)  L(y)  ~Z(x, y))
G = x(C(x)  ~L(x))
Тепер можна сформулювати алгоритм автоматичного доведення теорем
на основі методу резолюцій. Нагадаємо, що йдеться про перевірку істинності
будь-якого твердження в рамках існуючої системи знань.
Застосовується метод доведення "від супротивного". При перевірці
утворюється деяка пробна теорія, що утворюється шляхом додавання за-
перечення нового твердження до вже існуючих (сама база знань при цьому
вважається несуперечливою). Послідовно застосовується правило резолюції, і
утворені резольвенти додаються до пробної теорії. Якщо при цьому врешті
утворюється пуста фраза, то твердження, яке перевіряється, істинне.
Фундаментальною властивістю методу резолюцій є його повнота. Як
уже зазначалося, логіка предикатів першого порядку не є розв'язною. Тому для
множини диз'юнктів, яка не є суперечливою, процедура, що ґрунтується на
методі резолюцій, може працювати нескінченно довго.
Приклад. Нехай дано такий набір фраз:

44