Метод резолюції

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

Нехай р представляє твердження "Сократ - це людина", aq - твердження "Сократ смертний". Нехай наша теорія має вигляд

Т = {{¬ р, q}, {р}}.

Таким чином, стверджується, що якщо Сократ людина, то Сократ смертний, і що Сократ - людина. {17} виводиться з теорії Т за один крок резолюції, еквівалентній правилом modus ponens. .

Вирази {¬ р, q} і {р} "стикаються" на парі доповнюють літералів р і  ¬ р, а {q} є резольвенту. Таким чином, теорія алогічний увазі д, що записується у формі Т |-q. Тепер можна додати нову фразу {q} - резольвенту - в теорію Т і отримати таким чином теорію

Т '= {{¬ ip, q}, {p}, {q}}.

Звичайно, в більшості  випадків для доказу потрібно безліч кроків. Покладемо, наприклад, що теорія Т має вигляд

У цій теорії р і q зберігають колишній сенс, а г представляє твердження "Сократ - бог". Для того щоб показати, що Т | - ¬ r, будуть потрібні два кроки резолюції:

{¬ q, p}, {Р} / {q}

{¬ q,-r}, {q} / {-r}

Зверніть увагу, що на першому  кроці використовуються дві фрази  з вихідної безлічі Т, а на другому-резольвента {q}, додана до Т. Крім того, слід зазначити, що доказ може бути виконане і по-іншому, наприклад:

{¬ p, q}, {¬ q, ¬ r} / {¬ p, ¬ r},

{¬ p, ¬ r}, {p} / {¬ r}

При такому способі докази до Т додається інша резольвента. У зв'язку зі сказаним виникає ряд проблем.

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

Безліч Т може підтримувати і ті правила, які не мають нічого спільного з доказом цільової формули. Як же заздалегідь дізнатися, які правила приведуть нас до мети?

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

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

Припустимо, перед нами стоїть завдання вивести {q} з деякого безлічі фраз

Т = {...,{ ¬ p, q },...}.

Створюється враження, що це безліч потрібно перетворити, відшукуючи фрази, що включають q в якості літерала, а потім спробувати усунути інші літерали, якщо такі знайдуться. Але фраза {q} не "стикається" з такою фразою, як, наприклад, {-р, q}, оскільки пара, що складається з однакових літералів q, не є взаємно доповнює.

Якщо q є метою, то метод  спростування резолюції реалізується додаванням негативної формули мети до безлічі Т, а потім потрібно показати, що формула

Т '= Т U {¬ q}

є несумісною. Вважаючи, що безліч Т несуперечливо, приходимо до висновку, що Т 'може бути суперечливим внаслідок Т | - q.

Розглянемо це питання  більш докладно. Спочатку до існуючого  безлічі фраз додається заперечення перевіряється фрази {-q}. Потім робиться спроба резольвіровать {-q} з іншого фразою в Т. При цьому існують тільки три можливі ситуації.

У Т не існує фрази, що містить q. У цьому випадку довести шукане неможливо.

Безліч Т містить {q}. У цьому випадку доказ виконується негайно, оскільки з {¬ q} і {q} можна вивести порожню фразу, що означає несумісності (наявність протиріччя).

Безліч Т містить фразу {..., q, ...}. Резольвірованіе цієї фрази з {¬ q} формує нову фразу, яка містить інші літерали, причому для доказу протиріччя всі вони повинні бути видалені в процесі резольвірованія.

Ці залишилися літерали можна розглядати в якості підцілей, які повинні бути дозволені, якщо потрібно досягти головної мети. Описана стратегія отримала назву низхідною (або зворотного) і дуже нагадує формулювання підцілей в системі MYCIN.

Як приклад покладемо, що безліч Т, як і раніше, має вигляд {{¬ p, q}, {¬ q, ¬ r}, {p}}. Ми намагаємося показати, що Т | - ¬ r. Для цього доведемо, що фраза {r} є наслідком існуючого безлічі Т, для чого додамо до цього безлічі заперечення фрази ¬ r. Пошук суперечності відбувається наступним чином:

[{¬ q, ¬ r}, {r }]/{¬ q}

[{¬ p, q}, {¬ q }]/{¬ q}

[{¬ p}, {p }]/{}

Цей метод доведення теорем отримав назву "спростування резолюції", оскільки, по-перше, він використовує правило висновку резолюцій, а по-друге, слід стратегії "від протилежного" (стратегії спростування).

Тепер повернемось до нашого прикладу PROLOG-програми, представленому в лістингу 1. На рис. 1 показано дерево докази затвердження above (a, с). Дерево будується зверху вниз, і кожна гілка пов'язує дві "батьківські фрази", в яких містяться доповнюють літерали, з фразою, яка утворюється в результаті застосування правила резолюції. До всіх цілям, записаним праворуч від значка ":-", неявно застосовується заперечення. У лівій частині дерева представлені формули цілей, а в правій - фрази, взяті з бази даних.

Коренем дерева є пуста  фраза {}. Це означає, що пошук доказу був успішним. Додавання негативної фрази: - above (а, с) до вихідного безлічі (теорії) призвело до суперечності. Таким чином, можна стверджувати, що фраза above (а, с) є логічним наслідком із цієї теорії.

Зверніть увагу на роль операції уніфікації в цьому доказі. Мета above (а, с) уніфікується з головним фразою above (X, Y) за допомогою підстановки {Х / а, Y / c}, де вираз Х / а можна інтерпретувати як "X отримує значення а". Потім ця підстановка застосовується до хвостової частини фрази

on (Z, Y), above (X, Z),

з чого випливає формулювання підцілей

on (Z, с), above (a, Z).

Наступна підцілі on (Z, с) уніфікується з on (b, c) підстановкою {Z / b}. Ця підстановка потім застосовується і до решти підцілі, яка таким чином перетворюється на above (а, b), і так до тих пір, поки не утвориться пуста фраза.

 

Рис. 1. Дерево докази методом  спростування резолюцій 

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

 

4. Висновок 

Тема штучного інтелекту  завжди була в інформатиці "країною  поганців", населеної масою "неправильних" проблем, що не піддаються вирішенню традиційними способами. Ця область привернула увагу насамперед різнобічних фахівців, яких не злякало її відкрите, позбавлене будь-якої організації простір, - людей, яких вабить завдання дізнатися, як ми мислимо. Такі дослідники, як Марвін Мінський (Marvin Minsky), Джон Мак-Карті (John McCarthy), Герберт Саймон (Herbert Simon), Пат Хейес (Pat Hayes), Дональд Мічі (Donald Michie) і Бернард Мельтцера (Bernard Meltzer), стали першопрохідцями для тих, хто слідував за ними по дорозі, що пролягає через інформатику, психологію і математичну логіку.

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

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

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

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

 

Список літератури:

1. О.М. Адаменко, А.М. Кучуків.  Логічне програмування та Visual Prolog

СПб.: БХВ-Петербург, 2003.

2. Братко І. Алгоритми  штучного інтелекту мовою PROLOG. М.: «Вільямс», 2004.

3. Джексон П. Введення  в експертні системи.-Москва, С. Петербург, Київ: Вид. будинок "Вільямс", 2002

4. Дж. Доорс, А. Рейблейн, С. Вадер. Пролог - мова програмування  майбутнього. М.: Фінанси і статистика, 1990

5. Дюбуа Д., Прад А. Теорія  можливостей. Додатки до 

представлення знань. -М.: Радіо і зв'язок, 1995

6. Корнєєв В.В., Гарєв А.Ф., Васюшін СВ., Райх В.В. Бази даних. 

Інтелектуальна обробка  інформації. - М.: Изд-во "Нолидж",

2000

7. Мендельсон Е. Введення  в математичну логіку. М., 1976

8. Нечаєв В.В., Панченко  В.М., Свиридов О.П. Дослідження операцій

і теорія систем. Основи статистичної динаміки знань. Навчальний

посібник.-М.: МІРЕА, 2000

9. Новиков П. С. Елементи  математичної логіки. М., 1959

10. Попов Е.В. Експертні  системи реального часу. В: Відкриті 

системи, N2 (10), 1995

11. Хоггер К. Введення  в логічне програмування М.: Мир, 1988

12. Черч А. Введення в  математичну логіку, т. I. М. 1960