Презентація на тему:
Автоматичне доведення теорем і метод резолюцій

Тема №4 Автоматичне доведення теорем і метод резолюцій

Автоматизація дедуктивних логічних побудов Одна з постановок - автоматичне доведення теорем. Тут ми розглядаємо базу знань як логічну теорію, тобто як сукупність аксіом і правил виведення. Формули вважаємо правильно побудованими. Постановка задачі: дана теорія S. Потрібно встановити, чи є твердження q теоремою, тобто чи можна його логічно вивести з аксіом теорії після скінченного числа застосувань правил виведення.

Автоматичне доведення теорем і логічне програмування Механізм автоматичного доведення теорем лежить в основі логічного програмування (напр., Пролог) і прологівського механізму виконання програм. Основна ідея логічного програмування - програма розглядається як певна теорія, тобто як певний набір тверджень (аксіом і правил виведення); виконання програми є доведенням певної теореми (або перевіркою певного твердження).

Прологівський механізм: продовження Іншими словами, ціль прологівської програми - перевірка істинності певного твердження (доведення теореми). Процедурний аспект імплікації (Ковальскі) - вираз Q,S => P ( в Пролозі - P:-Q,S) можна проінтерпретувати наступним чином: щоб досягти мети P, треба спочатку досягти Q, а потім S. Основа прологівського механізму виконання програм - бектрекінг на основі зворотного логічного виведення. Найбільш відомий метод - метод резолюцій (Робінсон, 1965 р). Ербран, Маслов.

Простий приклад теорії Кіт їсть м’ясо. Якщо X їсть м’ясо, то X хижак. M(c). M(X) v H(X). Довести: кіт є хижак.

Метод резолюцій: основні визначення Атомарна формула (літерал) - предикат, який залежить від певної кількості аргументів - термів: констант, змінних і функторів (тобто функціональних символів від термів). Літерал негативний, якщо він стоїть під знаком заперечення; позитивний - якщо не стоїть. Диз’юнкт (фраза) - диз’юнкція певної кількості літералів. Пустий диз’юнкт □, який не містить літер. Якщо теорія містить □ (або з теорії можна вивести □), то вона суперечлива. Позначення: константи будемо позначати першими літерами латинського алфавіту (a,b,…); змінні - останніми (x,y,z).

Найважливіші терміни: продовження Контрарна пара. Підстановка. Уніфікатор. Композиція (добуток) підстановок. Найбільш загальний уніфікатор (НЗУ). Бінарна резолюція. Резолюція на основі НЗУ. Алгоритм знаходження НЗУ.

Метод резолюцій: попередній етап Метод резолюцій працює з формулами, записаними у вигляді набору фраз, що не містять кванторів (кожна фраза - безкванторна диз’юнкція атомарних формул). Є певна послідовність перетворень, яка дозволяє звести будь-яку формулу числення предикатів до такої форми.

Основні кроки зведення Усунення імплікацій та тотожностей. Втягнення заперечень всередину (зведення до вигляду, коли всі заперечення знаходяться тільки над літералами) – на основі законів де Моргана. Перейменування змінних (щоб не було випадкового співпадіння імен змінних в області дії кванторів). Зведення до пренексної нормальної форми: K1 … Kn M(x1, …, xn), де M - формула, яка містить тільки кон’юнкції та диз’юнкції атомарних формул і не містить кванторів, Ki - квантори. Усунення кванторів існування (сколемізація, введення констант і функцій Сколема). Усунення кванторів узагальнення. Зведення до кон’юнктивної нормальної форми. Розділення кон’юнкцій.

Сколемізація Якщо квантор існування не стоїть в області дії квантора узагальнення - константа Сколема: від x P(x) до P(c). В іншому випадку - функція Сколема: від y x: P(x,y) до P(h(y),y). Перетворення не еквівалентні, але можна довести наступне: Теорія А суперечлива тоді і тільки тоді, коли невиконувана її сколемівська форма SA.

Зведення до КНФ Від A (B&C) до (A B) &(A C).

Розділення кон’юнкцій від (A B)(D E) до A B. D E.

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

Приклад Від A B. B C. до A C.

Правило бінарної резолюції для предикатів Дві фрази містять контрарну пару, якщо одна містить деякий позитивний літерал, а інша - негативний з тим самим предикатним ім’ям, і ці літерали можуть бути уніфіковані, тобто існує уніфікатор (допустима підстановка σ, після застосування якої набори аргументів літералів стають однаковими). Допустимою є підстановка замість змінних (не замість констант!) термів, що не містять цих змінних. Резольвента фраз P C1, P C2), що містять контрарну пару (P, P ) утворюється як диз’юнкція цих фраз, з якої контрарна пара викреслюється, а до залишків застосовується уніфікатор σ : σ (C1) σ(C2).

Простий приклад резолюції для предикатів Q(x,y) P(x) Q(a,b) R(y) Підстановка σ= {a/x, b/y }. Тоді резольвента (результат резолюції): P(a) R(b). Резолюцією P та P є пустий диз’юнкт.

Підстановка: більш формальне визначення Нехай Х - алфавіт змінних і T(W,X) – алгебра термів над Х. Підстановкою називається відображення σ, що має вигляд σ:X->T(W,X). Підстановка часто позначається через {t1/x1, … ,tn/xn }

Уніфікатор Підстановка називається уніфікатором для множини термів { Q1, … Qn} тоді і тільки тоді, коли (Q1) = … = (Qn) . Кажуть, що множина термів уніфікується, якщо для неї існує уніфікатор.

Композиція (добуток) підстановок Нехай = {t1/x1, … , tn/xn } і = {r1/y1, … , rm/ym } . Добутком підстановок і називається підстановка, одержана з множини { (t1 ) / x1, … , (tn ) /xn, r1/y1, … , rm/ym } вилученням всіх елементів, що мають вигляд (tk) / xk , для яких (tk ) = xk , і всіх елементів, що мають вигляд rk /yk і таких, що yk належить {x1, … , xn}.

Композиція підстановок: приклад Нехай = {f(y)/x, z/y}, = {a/x, b/y, y/z). Тоді добуток = { f(b)/x), y/z}.

Найбільш загальний уніфікатор Уніфікатор множини термів {t1, … , tn} називається найбільш загальним уніфікатором (НЗУ), якщо для всякого уніфікатора цієї множини існує така підстановка , що = . Ознайомлення з конкретними алгоритмами пошуку НЗУ виноситься на самостійну роботу.

Склеювання Якщо дві або більше літер з однаковими предикатними символами в диз’юнкті С мають НЗУ , то (С) називається склеюванням С.

Загальне правило резолюцій Резольвентою диз’юнктів-посилок С1 і С2 називається одна з таких резольвент: бінарна резолюція С1 і С2; бінарна резолюція С1 і склеювання С2; бінарна резолюція С2 і склеювання С1; бінарна резолюція склеювання С1 і склеювання С2.

Алгоритм автоматичного доведення теорем на основі методу резолюцій Постановка задачі: дана теорія, або набір тверджень S. Треба перевірити істинність твердження q (точніше, чи є q логічним наслідком S). Сама теорія S при цьому має бути несуперечливою. Фактично - доведення від супротивного.

Алгоритм методу резолюцій: продовження Утворюється пробна теорія S’ шляхом додавання до S заперечення q: S’ := S { q}. Послідовно здійснюються резолюції, їх результати (резольвенти) додаються до пробної теорії. Якщо на певному кроці утворюється пустий диз’юнкт, то S’ суперечлива, і відповідно, твердження q істинне. Якщо чергову резолюцію здійснити неможливо - q хибне.

Повнота методу резолюцій Теорія S суперечлива тоді і тільки тоді, коли з неї можна вивести пустий диз’юнкт. Це означає, що якщо твердження істинне, то алгоритм рано чи пізно доведе, що воно є істинним. Числення предикатів є алгоритмічно нерозв’язним, і тому можуть бути твердження, для яких алгоритм працюватиме нескінченно довго.

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

Лінійна резолюція Лінійним виведенням з множини фраз S називається послідовність диз’юнктів (C1 , … ,Cn), де C1 S, а будь-який Ci+1 є резольвентою Ci (який називається центральним диз’юнктом) і деякого Вi , який називається боковим диз’юнктом. Боковий диз’юнкт Вi повинен задовольняти одній з двох умов: або Вi S, або Вi є деяким Ck , k < i.

Можливе лінійне виведення C[1] B[1] C[2] C[3] B[2] C[n-1] B[n-1] C[n]

Властивості лінійної резолюції Не виключає перебору, але суттєво підвищує його цілеспрямованість. Є повною.

Вхідна резолюція Вхідна резолюція - варіант лінійної резолюції, в якій хоча б один з диз’юнктів, які беруть участь у черговій резолюції, належить S. Вхідна резолюція, взагалі кажучи, не є повною. Але вона є повною для певного класу диз’юнктів - т.зв. фраз Хорна. Фраза Хорна - це диз’юнкт, який містить не більш ніж один позитивний літерал. В основі прологівського механізму лежить саме вхідна резолюція.