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

Європейський  Університет

 

 

 

 

 Реферат  на тему:”Метод резолюції ”

 

 

 

 

 

 

Підготував  студенит 2-го курсу

Бізнес-Коледжу 

Остапюк Олександр

 

 

 

 

 

 

 

 

Рівне 2013   

 

 

1. Основні виробники. 

Інструментарій для створення  експертних систем реального часу вперше випустила фірма Lisp Machine Inc в 1985 році. Цей продукт призначався для  символьних ЕОМ Symbolics і носив назву Picon. Його успіх привів до того, що група провідних його розробників утворила фірму Gensym, яка, значно розвинувши ідеї, закладені в Picon, випустила в 1988 році інструментальне засіб під назвою G2. На даний момент працює його третя версія і підготовлена четверта.

Ще наприкінці 1970-х років  стала чітко проглядатися тенденція  до використання в дослідженнях в області штучного інтелекту "формальних" методів, тобто заснованих на апараті математичної логіки. Ці методи протиставлялися більш інтуїтивним і менш формалізованим евристичним методам, скажімо, таким, які були використані в системі MYCIN. Для того щоб стало ясно, що все це значить, треба познайомити вас з логічними мовами, а потім показати, як співвідносяться їх властивості з тими методами міркувань, які повинні підтримувати типові експертні системи.

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

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

При реалізації автоматичного формування суджень, як правило, прагнуть до максимально можливого однаковості та стандартизації у поданні формул, але в той же час в літературі часто доводиться стикатися з найрізноманітнішими системами позначень, що відносяться до логіки. Основними синтаксичними схемами подання виразів є Кон'юнктивна нормальна форма (conjunctive normal form-CNF), повна фразова форма (full clausal form) і фраза Хорна (Horn clause), остання є підмножиною повної фразовой форми.

 

2. Історія виникнення і  розвитку мови ПРОЛОГ.

 

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

У жовтні 1981 року Японське міністерство міжнародної торгівлі і промисловості оголосило про створення дослідницької організації - Інституту по розробці методів створення комп'ютерів нового покоління (Institute for New Generation Computer Technology Research Center). Метою даного проекту було створення систем обробки інформації, що базуються на знаннях. Передбачалося, що ці системи будуть забезпечувати простоту управління за рахунок можливості спілкування з користувачами за допомогою природної мови. Ці системи повинні були самонавчатися, використовувати накопичуються в пам'яті знання для вирішення різного роду завдань, надавати користувачам експертні консультації, причому від користувача не потрібно бути фахівцем в інформатиці. Передбачалося, що людина зможе використовувати ЕОМ п'ятого покоління так само легко, як будь-які побутові електроприлади типу телевізора, магнітофона і пилососа. Незабаром слідом за японським стартували американський та європейський проекти.

Поява таких систем могло  б змінити технології за рахунок  використання баз знань та експертних систем. Основна суть якісного переходу до п'ятого покоління ЕОМ полягала в переході від обробки даних до обробки знань. Японці сподівалися, що їм вдасться не підлаштовувати мислення людини під принципи функціонування комп'ютерів, а наблизити роботу комп'ютера до того, як мислить людина, відійшовши при цьому від фон неймановской архітектури комп'ютерів. У 1991 році передбачалося створити перший прототип комп'ютерів п'ятого покоління.

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

В якості основної методології  розробки програмних засобів для  проекту ЕОМ п'ятого покоління було обрано логічне програмування, яскравим представником якого є мова Пролог. Здається, що і в даний час Пролог залишається найбільш популярною мовою штучного інтелекту в Японії і Європі (США, традиційно, більш поширений іншу мову штучного інтелекту - мова функціонального програмування Лісп).

Назва мови "Пролог" походить від слів Логічне програмування (PROgrammation en LOGique у французькому варіанті і PROgramming in LOGic - в англійській).

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

В історії виникнення і  розвитку мови Пролог можна виділити наступні етапи.

У 1965 році в роботі "A machine oriented logic based on the resolution principle", опублікованій в 12 номері журналу "Journal of the ACM", Дж Робінсон представив метод автоматичного пошуку докази теорем в численні предикатів першого порядку, який отримав назву "принцип резолюції". Насправді, ідея даного методу була запропонована Ербраном в 1931 році, коли ще не було комп'ютерів. Робінсон модифікував цей метод так, що він став придатним для автоматичного, комп'ютерного використання, і, крім того, розробив ефективний алгоритм уніфікації, що становить базис його методу.

У 1973 році "група штучного інтелекту" на чолі з Аланом Колмерое створила в Марсельському університеті програму, призначену для доведення теорем. Ця програма використовувалася при побудові систем обробки текстів на природній мові. Програма докази теорем отримала назву Prolog (від Programmation en Logique). Вона і стала прообразом Прологу. Ходять легенди, що автором цієї назви була дружина Алана Колмерое. Програма була написана на Фортрані і працювала досить повільно.

Велике значення для розвитку логічного програмування мала робота Роберта Ковальського "Логіка предикатів як мова програмування" (Kowalski R. Predicate Logic as Programming Language. IFIP Congress, 1974), в якій він показав, що для того щоб досягти ефективності, потрібно обмежитися використанням безлічі Хорновськими диз'юнктів. До речі, відомо, що Ковальський і Колмерое працювали разом протягом одного літа.

У 1976 р. Ковальський разом  з його колегою Маартеном ван  Емден запропонував два підходи до прочитання текстів логічних програм: процедурний і декларативний. Про ці підходах мова піде у третій лекції.

У 1977 році в Единбурзі Уоррен і Перейра створили дуже ефективний компілятор мови Пролог для ЕОМ DEC-10, який послужив прототипом для багатьох наступних реалізацій Прологу. Що цікаво, компілятор був написаний на самому Пролозі. Ця реалізація Прологу, відома як "едінбурзька версія", фактично стала першим і єдиним стандартом мови. Алгоритм, використаний при його реалізації, послужив прототипом для багатьох наступних реалізацій мови. Як правило, якщо сучасна Пролог-система і не підтримує Единбурзький Пролог, то до її складу входить підсистема, яка переводить прологовскую програму в "Единбурзький" вигляд. Є, звичайно, стандарт ISO / IEC 13211 - 1:1995, але його підтримують далеко не всі Прологсістеми.

У 1980 році Кларк і Маккейб  у Великобританії розробили версію Прологу для персональних ЕОМ.

У 1981 році стартував вищезгаданий проект Інституту по розробці методів  створення комп'ютерів нового покоління.

На сьогодні існує досить багато реалізацій Прологу. Найбільш відомі з них наступні: BinProlog, AMZI-Prolog, Arity Prolog, CProlog, Micro Prolog, МПролог, Prolog-2, Quintus Prolog, SICTUS Prolog, Silogic Knowledge Workbench, Strawberry Prolog, SWI Prolog, UNSW Prolog і т. д.

У нашій країні були розроблені такі версії Прологу як Пролог-Д (Сергій Григор'єв), Акторний Пролог (Олексій Морозов), а також Фленг (А. Манцівода, В'ячеслав Петухін).

Стерлінг і Шапіро в книзі "Мистецтво програмування мовою Пролог" пишуть: "Зрілість мови означає, що він більше не є доопределяют і уточнюємо науковою концепцією, а стає реальним об'єктом з усіма притаманними йому вадами і чеснотами. Настав час визнати, що хоча Пролог і не досяг високих цілей логічного програмування, але, тим не менш, є потужним, продуктивним і практично придатним формалізмом програмування ".

 

3. Обчислення висловлень.

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

Нижче приведені всі синтаксичні  правила, які використовуються для  конструювання правильно побудованих  формул (ППФ) в обчисленні висловлювань.

(S. U) ЕсліU є атомом, то в є ППФ.

(S ¬) Якщо U є ППФ, те-U також є ППФ.

(S. v) Якщо U і ф є ППФ,  то (U u ф) також є ППФ. 

У цих правилах малі літери грецького алфавіту (наприклад, U і ф) представляють пропозіціональние змінні, тобто НЕ атомарні формули, а будь-яке просте або складене висловлювання. Пропозіціональние константи є частиною мови висловлювань, який використовується для програми обчислення пропозиційних змінних до конкретної проблеми.

Вираз-U читається як "не U", а (U v ф) читається як диз'юнкція "U або ф (або обидва)". Можна ввести інші логічні константи - "л" (сполучення), "D" (імплікація, або обумовленість), "=" (еквівалентність, або рівнозначність), які, по суті, є скороченнями комбінації трьох наведених вище констант. .

(U ^ ф) Еквівалентно ¬  (¬ U v ф). Читається "U і ф".

(U  ф) Еквівалентно (¬ U v ф). Читається "U імплікує ф".

(U == ф) Еквівалентно (U  ф) ^ (ф  U). Читається "U еквівалентно ф".

У кон'юнктивній нормальній формі обчислення висловлювань константи "імплікація" і "еквівалентність" замінюються константами "заперечення" і "диз'юнкція", а потім заперечення  складного висловлювання розкривається  за допомогою формул Де Моргана:

¬ (U ^ ф) перетворюється в (¬ Uv ¬ ф), ¬ (U v ф) перетворюється в (-U ^ ф), ¬ ¬ U перетвориться в U.

Останній етап перетворень - внесення диз'юнкцій всередину дужок: (Ј v (U ^ ф))) замінюється ((ЈvU \ (U) ^ (Јvф)).

Прийнято скорочувати  вкладеність дужкових форм, відкидаючи в нормальній кон'юнктивній формі  знаки операцій v і л. Нижче представлений  приклад перетворення виразу, що містить імплікацію двох дужкових форм, в нормальну кон'юнктивні форму.

¬ (pvq)  (-P ^ Aq) Вихідне вираз.

¬ ¬ (pvg) v (-p ^ - q) Виключення ~.

(Pvq) v (-p ^ - q) Введення - всередину  дужок. 

(¬ pv (pvq)) v (¬ pv (pvq)) Занесення v всередину дужок.

{{-P, р, q}, {¬ q, р, q}} Відкидання А і v у кон'юнктивній нормальній формі.

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

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

перетвориться в дві фрази:

p, q <¬ q.

в яких позитивні літерали згруповані ліворуч від знаку  стрілки, а негативні справа.

Більш строго, фраза є виразом вигляду

в якому p1 ..., рт q1 ,..., qn є атомарними формулами, причому т => 0 і п => 0. Атоми в множині р1 ,..., рт подають висновки, об'єднані операторами диз'юнкції, а атоми в множині q1 ..., qn - умови, об'єднані операторами кон'юнкції.

3.1 Обчислення предикатів

Обчислення висловлень має  певні обмеження. Воно не дозволяє оперувати  з узагальненими твердженнями на кшталт "Всі люди смертні". Звичайно, можна позначити таке твердження деякої пропозіціональной константою р, а інший константою q позначити твердження "Сократ - людина". Але з (р л q) не можна вивести затвердження "Сократ смертний".

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

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