Підстановка а називається уніфікатором для множини виразів {M,, ...,..., MLi

якщо^м'“"^'-'^Ч°

Уніфікатор ст для множини виразів {M,, ..., М„] називається найбЬіьш загальним уніфікатором, якщо для будь-якого уніфікатора 0 цієї множини існує така підстановка X,

щоОявлятиме собоюкомпозицію п/дстановокаІ X.

Композицією Постановок° “ щ| -.V*.)¹1 “ ІЩ Щрі на

зивається підстановка^{,,Ux'- - - '^- Ш |4 ^* з якої викресленівсі ?,A/x,, якщо^"'>^,'*^й^^т“’^и“^хв **" - -^1-

Тепер можна сформулювати загальне правило резолюцій.

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

Існують формальні алгоритми, які дозволяють отримувати найбільш загальний уніфікатор [121, 272, 320]. Але у більшості випадків достатньо деяких неформальних простих правил, подІбних до тих, що були сформульовані в [172].

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

P(*)v~Q{b,c\

Q(b, c)v~X (b,C)

є резольвовані, I резольвента записується як^я^ ^v ~ ^ <>' *

P(a)v~Q(b,c\

2 0(c,c)v~*(b,c) p|_3Hf константи не зіставляються одна з одною, тому

фрази

не є резольвованими.

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

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

Ш0ЩШШШ

резольвується, при цьому змінна x зіставляється з константою о, змінна у — з константою Ь. У резольвенті^^'^'^змІннІ замінені на константи, з якими вони зіставлялися.

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

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

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

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

---

Системи штуїиою інтелекту. С^юи llM

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

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

Приклад 7.1.

Нехай дано такий набір фраз: вовк Тсть м'ясо,

тварини, якІТдять м'ясо, ехижаками.

Потрібно довести, що: вовк є хижаком.

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

ТодІ маємо базу знань:

GfiN,M)

~G(x,M)vQ (x)

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

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

~G(W,M) (7.11)

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

Приклад 7.2:

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

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

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

Необхідно довести, що:

Володимир єнащадком Олега.

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

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

(7.tt)

---

(7.U)(7.14)

(7Л5)

SlKK)

syc.0)

-Jfr>)vA4*.W ~N(x,'y) v-H0>. *) vMCr. x)

~ШР) (7.16)

Крон 2. Застосовуємо резолюцію до (7.16) I (7.15); при цьомухзІставляється з V, a z

-jO:

S(KX)

S(K,0)

~Sfay)vN(x,y)

~ЩйШ ^v '$Щ Ш ****• *>

-N(V.O)

-N(K,y)v-NU>.0) (7.17)

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

твердження

~J(K.r)v~A4K.0) (7.18)

Крок4. Застосовуємо резолюціюдо (7.14) і (7.18);додається твердження -S(Ky)v~S0>.O) (7.19)

Крон 5. Застосовуємо резолюціюдо (7.19) і (7.12); у зіставляється з K:

-SlK.O) (7.20)

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

Приклад 7.3.

Повернемосядо бази знань, що складається з фраз:

Ус! студенти люблять відвідувати лекції.

ДеякІстудентилюблять морозиво.

Іванов є студент, але не любить морозива.

Ми ввелитакі предикати та предметнІ константи:

L(x У) — *любить у.

S(x) — x є студентом.

А — предметна константа; яка означає "відвідування лекцій";

/ — предметна константа, яка відповідає Іванову;

Q — предметна константа, яка означає морозиво.

База знань має вигляд:

^' S (x) v L (x, А)

S(c)

L(c,0

S(1)

~L(I,Q). Спробуємо довести, що деякі люди, якІ люблять морозиво, люблять і відвідувати лекції. Остання фраза запишеться у вигляді 3xv /1 fo Д) & і /x, 0). її заперечення має вигляд

Системи штучного іііів,тскту Суром RM

Vx: (~ L (x, A) v ~ L (x, 0). Позбувшися квантора узагальнення, отримуємо фразу ~ L (x, A)v~ L(KQ).

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

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

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

Для даноїмножини диз'юнктівSI початкового диз'юнкта лІнІй-

I ним шиееденням диз'юнкта С_п називається [129,272] послідовність

Co, Cl,.,., С_м, де

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

t 2) будь-який боковий диз'юнкт В, або належить S, або є C) для ^< деякого У </•

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

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

---

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

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

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

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

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

6. Мова Пролог і логічне програмування

Розглянемо відповідність між численням предикатів і Прологом [26]. Як ми вже бачили, деякі фрази виглядають точно так, як фрази Прологу, а інші дещо інакше.

Зокрема, запитання Прологу:

?-ЛІ,Л2,........ ...,An означає точно те саме, що й неповна хорнІвська фраза:

:-A\A2, .J\n.

Система виведення Прологу базується на засобах аналізу хорнІвських фр_аз Конкретна стратегія, яку використовує ця мова, є формою аналізу постійного входу. Коли застосовується дана стратегія, вибір, що з чим аналізувати, проводиться за таким принципом.

Починаємо з цільового твердження та аналізуємо його разом з однією з аксІом. Отриману фразу знову аналізуємо з однією з аксіом і т. д. Ми завжди аналізуємо лише щойно отриману фразу разом з однією з первинних хорнІвських фраз. У Пролозі щойно отриману фразу можна розглядати як послідовність цІлей, що мають бути досягнуті. Все починається із запитання і закінчується (бажано) пустою фразою. На кожному кроці побудови виведення ми знаходимо фразу, початок якої збігається з однією з цілей зв'язуємо потрібні змінні, обираємо мету, яка збігається, І додаємо зміст зв'язаної фрази до набору цілей, що мають бути досягнуті.

Наприклад, вЩ:

;- мати (Іван, X), мати (X, T). та

мати (U, У):-батько (U, V), жінка (V). переходимо до

:- батько (Іван, X), жінка (X), мати (X, У).

Насправді стратегія доведення у Пролозі ще більш обмежена, ніж просто аналіз лінійного входу, В цьому прикладі ми вирішили звести перший літерал у цільовому пункті, але могли вибрати й інший.

В арго також наголосити, як Пролог вишукує альтернативні фрази для досягнення тІєї самої мети. В основному Пролог використовує стратегію пошуку "в глибину" частіше нІж "в ширину". Тобто, вІн оперує лише з од-імсю альтернативою одночасно, вважаючи цей вибір вІрним, доки fte буде доведено зворотне. Для кожної мети він вибирає фрази в затвердженій no-l Імдовності I звертається до наступних лише після доведення невірності попередніх. Альтернативною до цІєТ стратегії e стратегія пошуку "в ширину", до якої Пролог звертається пізніше. Вона має перевагу в тому, що за-оезпечує перебір yclx варіантів, у той часян пошук "в глибину" може легко зупинитись у глухому куті. 3 Іншого боку пошук "в глибину" дозволяє перевіряти варіанти до кінця I є простішим в оперуванні, до того ж займає менше ресурсів комп'ютера.

---

I, нарешті, кІлька'слІв про те, в яких випадках у Пролозі відповідність двох фраз може відрізнятись від класичного аналізу. Більшість варіантів Прологу дозволить вам досягнути такої мети: рівність (X, X).

? —рівність ff(Y), Y).

---

Смотрите также файлы

• Рынок финансовых услуг (1).doc

• n9.doc

• ПЕРВЫЕ ДНИ ПОСЛЕ ОПЕРАЦИИ.doc

• ЛФК при заболеваниях сосудов.doc

• ЛФК при беременности.doc