1. Будь-який терм зіставляється сам з собою. Наприклад, дві фрази

P(a)v~Q(b, с),

Q(b, c)v~R(b, с) є резольвовані, і резольвента записується як Р (a)v ~ R (b, с).

2. Різні константи не зіставляються одна з одною, тому фрази

Р (a) v ~ Q (Ь, с),

Q(c, с) v-Д (6, с) не є резольвованими.

3. Змінна може бути замінена константою або іншим термом. Так, фрази

P(a)v~Q(a, b\ Q(x₉y)v~R(x,y) резольвується, при цьому змінна х зіставляється з константою а, змінна у — з константою b. У резольвенті Р (a) v ~ R (а, Ь) змінні замінені на кон­станти, з якими вони зіставлялися.

Якщо в процесі виведення утворилися фрази Р (а) та ~ Р (а), їх резолю­цією є пустий диз'юнкт (тотожна хибність, позначається П). Саме виве­дення пустого диз'юнкта і означає суперечливість теорії.

Тепер можна сформулювати алгоритм автоматичного доведення тео­рем на основі методу резолюцій. Нагадаємо, що йдеться про перевірку іс­тинності будь-якого твердження в рамках існуючої системи знань.

Застосовується метод доведення "від супротивного". При перевірці утворюється деяка пробна теорія, що утворюється шляхом додавання за­перечення нового твердження до вже існуючих (сама база знань при цьо­му вважається несуперечливою). Послідовно застосовується правило резо­люції, і утворені резольвенти додаються до пробної теорії. Якщо при цьому врешті утворюється пуста фраза, то твердження, яке перевіряється, істинне.

Фундаментальною властивістю методу резолюцій є його повнота. Від­повідна теорема формулюється так [129]: множина диз'юнктів S супере­члива тоді і тільки тоді, коли з неї можна вивести пустий диз'юнкт.

Як уже зазначалося, логіка предикатів першого порядку не є розв'яз­ною. Тому для множини диз'юнктів, яка не є суперечливою, процедура, що ґрунтується на методі резолюцій, може працювати нескінченно довго.

Наведемо ще приклади застосування методу резолюції.

Приклад 7.1.

Нехай дано такий набір фраз:

вовк їсть м 'ясо,

тварини, які їдять м 'ясо, є хижаками.

Потрібно довести, що:

вовк є хижаком.

Введемо предикати G (х, у), який означає "х їсть у" і Q (х), який означає "х є хижаком". Далі введемо предметні константи: W— вовк; М— м'ясо.

Тоді маємо базу знань: G (W, М)

~ G (х, М) v Q (хУ

Потрібно довести формулу Q (fV).

Крок 1. Утворюємо пробну теорію та додаємо до неї заперечення:

9. (7.10)

G(W,M)

~ G (x,M)v Q(x)

-em

Крок 2. Застосовуємо резолюцію до (7.9) та (7.10); при цьому констан­та W зіставляється зі змінною х:

G(W,M)

~ G(x,M)v Q (х)

-всю

~G(W,My

Крок 3. Внаслідок резолюції (7.8) і (7.11) утворюється пуста фраза. Це означає суперечливість пробної теорії та істинність твердження, яке перевіряється.

Приклад 7.2:

Нехай дана база знань, що складається з фраз: Володимир є сином Костянтина, Костянтин є сином Олега та правил:

Якщо х є сином у, то х є нащадком у,

Якщо х є нащадком у, а у є нащадком z, то х є нащадком z.

Необхідно довести, що: Володимир є нащадком Олега.

Введемо предметні константи V— Володимир, К— Костянтин, О — Олег і предикати: S (х, у) — х є сином у; N (х, у) — х є нащадком у.

Крок 1. Утворюємо пробну теорію шляхом додавання заперечення твердження, що перевіряється:

S(V₉K) S(K₉0)

~S(x₉y)vN(x,y) ~N(x,y)v~N(y₉z)v N (х, z) ~N(V₉Oy

Крок 2. Застосовуємо резолюцію до (7.16) і (7.15); при цьому х зістав­ляється з V, a z — з О: S(V,K) S(K,0)

~S(x₉y)vN(x₉y)

~ N (х, у) v ~ N (у, z) v N (х, z)

~N(V,0)

~ N(K,y)v ~ N(y, О) (7.17)

Крок 3. Застосовуємо резолюцію до (7.14) і (7.17); в результаті до теорії додається твердження

~S(V₉y)v~N(y₉0) (7.18)

Крок 4. Застосовуємо резолюцію до (7.14) і (7.18); додається твердження ~S(V₉y)v~S(y₉0). (7.19)

Крок 5. Застосовуємо резолюцію до (7.19) і (7.12);^ зіставляється з К: ~S(K,0) (7.20)

Крок 6. У результаті резолюції (7.13) і (7.20) утворюється порожня фраза. Висновок: твердження, що перевіряється, є істинним. Приклад 7.3.

Повернемося до бази знань, що складається з фраз: Усі студенти люблять відвідувати лекції. Деякі студенти люблять морозиво. Іванов є студент, але не любить морозива.

Ми ввели такі предикати та предметні константи: L (х, у) — х любить у. S (х) — х є студентом.

А — предметна константа, яка означає "відвідування лекцій"; / — предметна константа, яка відповідає Іванову; Q — предметна константа, яка означає морозиво. База знань має вигляд:

- S (х) v L (х, А) S(c) L (с, Q) S(I)

Спробуємо довести, що деякі люди, які люблять морозиво, люблять і відвідувати лекції.

Остання фраза запишеться у вигляді Зх: (L (х, А) & L (х, Q)). Її запере­чення має вигляд Vx: L (х, A) v (х, Q)). Позбувшися квантора узагаль­нення, отримуємо фразу ~ L (х, A) v ~ L (х, Q).

Подальші резолюції здійснюються звичайним чином. Спробуйте вико­нати їх самостійно.

У літературі також вживаються такі терміни, як лінійна і вхідна резо­люції. Пояснимо їх застосування.

Метод резолюцій є перебірною процедурою. Якщо спробувати безпо­середньо застосовувати метод резолюцій у тому вигляді, в якому він був сформульований, то для великих баз знань він породжуватиме значну кількість безперспективних резолюцій і тому виявляється досить неефек­тивним. Для запобігання "експоненційного вибуху" були запропоновані ефективніші модифікації [129]: семантична резолюція, лок-резолюція, лінійна резолюція. Суть цих модифікацій полягає у введенні тих чи інших критеріїв, за якими відбираються диз'юнкти, що беруть участь у черговій резолюції. Зазначені модифікації в цілому не усувають бектрекінгового перебору, але дозволяють істотно скоротити цей перебір і роблять метод резолюцій цілком придатним для практичного застосування.

І Для даної множини диз'юнктів S і початкового диз'юнкта ліній­ним виведенням диз'юнкта С_п називається [129, 272] послідовність С₀, Сі, ..., С_п, де

1. для і = 0, 1, ...,п- 1 диз'юнкт С_і+\ являє собою резольвенту диз 'юнк- та Сі (який називається центральним диз'юнктом) і B_t (який нази­вається боковим диз 'юнктом), при цьому:

2. будь-який боковий диз 'юнкт В і або належить S, або є Cj для деякого

Лінійна резолюція є повною.

Важливим варіантом лінійної резолюції є так звана вхідна резолюція, Для якої за бокові диз'юнкти беруться тільки диз'юнкти з множини S. Вхід­на резолюція є простою та ефективною, і саме вона лежить в основі меха­нізму логічного виведення, що реалізовано в мові Пролог.

У загальному випадку вхідна резолюція не є повною. Але повнота вхідної резолюції гарантується, якщо обмежитися тільки хорнівськими диз'юнктами.

Нарешті, видається зручним такий неформальний опис лінійної, зокрема вхідної, резолюції [172].

Алгоритм доведення теорем на основі методу резолюцій повинен бути сфокусований на наслідках внесення до пробної теорії нових ре­зольвент. Це досягається за допомогою таких двох правил:

• у першій резолюції слід використовувати щойно додане запере­чення твердження, яке перевіряється;

• кожна наступна резолюція повинна використовувати попередній результат.