Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем


НазваАвтоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем
Дата конвертації06.02.2013
Розмір445 b.
ТипПрезентации


Тема №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), де C1S, а будь-який Ci+1 є резольвентою Ci (який називається центральним диз’юнктом) і деякого Вi , який називається боковим диз’юнктом. Боковий диз’юнкт Вi повинен задовольняти одній з двох умов: або ВiS, або Вi є деяким Ck , k < i.





Властивості лінійної резолюції

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

  • Є повною.



Вхідна резолюція

  • Вхідна резолюція - варіант лінійної резолюції, в якій хоча б один з диз’юнктів, які беруть участь у черговій резолюції, належить S.

  • Вхідна резолюція, взагалі кажучи, не є повною. Але вона є повною для певного класу диз’юнктів - т.зв. фраз Хорна.

  • Фраза Хорна - це диз’юнкт, який містить не більш ніж один позитивний літерал.

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



Схожі:

Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconАвтоматизація обліку в бутіках Автоматизація обліку в бутіках
Програмний комплекс налаштовується для будь-якої схеми торгівлі: одна каса на відділ одна каса на декілька відділів самообслуговування...
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconРозминка
Під час підготовки в текстовому редакторі реферату чи наукової статті в документ іноді потрібно вставляти формули, рівняння, формулювання...
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconФормула Герона. Формули радіусів вписаного й описаного кіл трикутника. Геометрія. 9 клас
Ще одна формула площі трикутника, для доведення якої можна використати тригонометричні функції, була наведена давньогрецьким математиком...
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconРоботу з поточною періодикою
Автоматичне встановлення дат очікуваного та реального приходу видання в бібліотеку
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconВідсоткове відношення Немає науки, не пов'язаної з математикою
Л. Ейлер Ми знаємо, що одна друга це половина, одна третя третина, одна четверта четвертина, три четвертих три четверті
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconРізні способи доведення теореми Піфагора

Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconАвтоматизація аптек Автоматизація аптек

Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconАвтоматизація фінансової логістики на підприємстві

Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconЕвклід, математик що жив у Давній Греції в 3 ст до н е. роботи Рафаеля
Загальноприйнятого визначення математики немає. Початково вона використовувалася для підрахунку, вимірювання, а також для вивчення...
Автоматизація дедуктивних логічних побудов Одна з постановок автоматичне доведення теорем iconТабличний процесор підтримує використання таких логічних функцій: И, или, не, если


Додайте кнопку на своєму сайті:
dok.znaimo.com.ua


База даних захищена авторським правом ©dok.znaimo.com.ua 2013
звернутися до адміністрації
dok.znaimo.com.ua
Головна сторінка