Принцип резолюції в обчисленні висловлювань та логіки предикатів і його модифікації

Зміст.
Введення ... ... ... ... ... ... ... ... ... ... ... ... .... ... ... ... ... ... ... ... ... ... ... ... ... .3
1. Основні виробники ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... .. 5
2. Історія виникнення і розвитку мови ПРОЛОГ ... ... .... ... ... ... .6
3. Обчислення висловлювань ... ... ... ... ... ... ... ... ... ... ... ... ... .... ... ... ... 9
3.1. Обчислення предикатів ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... .11
3.2. Програмування на Пролозі ... ... ... ... ... ... ... ... ... ... ... ... ... 14
3.3. Принцип резолюцій ... ... ... ... ... ... ... ... ... ... ... ... ... ... .. ... ... ... ... 16
3.4. Пошук докази в системі резолюцій ... ... ... ... ... ... .... ... .. 18 Висновок ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... .22
Список літератури ... ... ... .. ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... .. ... 24

Введення.
Програмні засоби, що базуються на технології та методи штучного інтелекту, набули значного поширення у світі. Їх важливість, і, в першу чергу, експертних систем і нейронних мереж, полягає в тому, що дані технології істотно розширюють коло практично значущих завдань, які можна вирішувати на комп'ютерах, і їх рішення приносить значний економічний ефект. У той же час, технологія експертних систем є найважливішим засобом у вирішенні глобальних проблем традиційного програмування: тривалість і, отже, висока вартість розробки додатків; висока вартість супроводу складних систем; повторна використовуванність програм і т.п. Крім того, об'єднання технологій експертних систем і нейронних мереж з технологією традиційного програмування додає нові якості до комерційних продуктів за рахунок забезпечення динамічної модифікації додатків користувачем, а не програмістом, більшої "прозорості" додатки (наприклад, знання зберігаються обмеженою природною мовою, що не вимагає коментарів до них, спрощує навчання та супровід), кращих графічних засобів, користувальницького інтерфейсу і взаємодії.
На думку фахівців, в недалекій перспективі експертні системи будуть відігравати провідну роль у всіх фазах проектування, розробки, виробництва, розподілу, продажу, підтримки і надання послуг. Їх технологія, отримавши комерційне поширення, забезпечить революційний прорив в інтеграції додатків з готових інтелектуально-взаємодіючих модулів.
Серед спеціалізованих систем, заснованих на знаннях, найбільш значущі експертні системи реального часу, або динамічні експертні системи. На їх частку припадає 70 відсотків цього ринку.
Значимість інструментальних засобів реального часу визначається не стільки їх бурхливим комерційним успіхом (хоча і це гідно ретельного аналізу), але, в першу чергу, тим, що тільки за допомогою подібних засобів створюються стратегічно значущі програми в таких галузях, як управління безперервними виробничими процесами в хімії , фармакології, виробництві цементу, продуктів харчування тощо, аерокосмічні дослідження, транспортування і переробка нафти і газу, управління атомними і тепловими електростанціями, фінансові операції, зв'язок та багато інших.
Класи завдань, що вирішуються експертними системами реального часу, такі: моніторинг у реальному масштабі часу, системи управління верхнього рівня, системи виявлення несправностей, діагностика, складання розкладів, планування, оптимізація, системи-порадники оператора, системи проектування.
Комерційні успіхи до експертних систем і нейронних мереж прийшли не відразу. Протягом ряду років (з 1960-х років) успіхи стосувалися в основному дослідних розробок, які демонстрували придатність систем штучного інтелекту для практичного використання. Починаючи приблизно з 1985 (а в масовому масштабі, ймовірно, з 1988-1990 років), в першу чергу, експертні системи, а в останні два роки і нейронні мережі стали активно використовуватися в реальних додатках.

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). Перший інтерпретується як "усі", а другий - "дехто" (або "дещо").
Нижче наведені синтаксичні правила обчислення предикатів першого порядку.
Будь-який символ (константа або змінна) є термо. Якщо rk є символом k-місній функції і а1 ..., <xk є термами, то Гk (a1. .., ak) є термо.
(S 40
Якщо Tk є символом k-місцевого предиката
і а1 ..., ak є термами,
то U (а1 ..., ak) є правильно побудованої формулою (ППФ).
(S. -) і (S. v)
Правила запозичуються з обчислення висловлюванні.
(S. V) Якщо U є ППФ та% є змінною,
то (будь-Х) U є ППФ.
Для позначення використовуються наступні символи:
U - довільний предикат;
Г - довільна функція;
a - довільний терм;
X - довільна змінна.
Дійсні імена, символи функцій та предикатів є елементами мови першого порядку.
Використання квантора існування дозволяє перетворити терми з квантором спільності відповідно до визначення
(EX) U визначено як - (будь-X)-U.
Вираз (Eх) (ФІЛОСОФ (Х)) читається як "Дехто є філософом", а вираз (будь-Х) (ФІЛОСОФ (Х)) читається як "Будь-який є філософом". Вираз ФІЛОСОФ (Х) є правильно побудовану формулу, але це не пропозиція, оскільки область інтерпретації для змінної X не визначена будь-яким квантором. Формули, в яких всі згадані змінні мають певні області інтерпретації, називаються замкненими формулами.
Як і в обчисленні висловлювань, у численні предикатів існує нормальна форма подання виразів, але для побудови такої нормальної форми використовується розширений набір правил синтаксичних перетворень. Нижче наведена послідовність застосування таких правил. Для приведення будь-якої вирази до нормальної форми слід виконати наступні операції.
(1) Виключити оператори еквівалентності, а потім імплікації.
(2) Використовуючи правила Де Моргана і правила заміщення (EX) U на - (будь-X)-U (а отже, і (будь-X) U на - (EX)-U), виконати приведення заперечення.
(3) Виконати приведення змінних. При цьому слід враховувати особливості визначення області інтерпретації змінних кванторами. Наприклад, у виразі (E Х) (ФІЛОСОФ (Х)) & (E Х) (АТЛЕТ (Х)) змінні можуть мати різні інтерпретації в одній і тій же області. Тому винесення квантора за дужки - (E Х) (ФІЛОСОФ (Х ))&.( АТЛЕТ (Х)) - дасть вираз, яке не випливає з вихідної формули.
(4) Виключити квантори існування. Квантори існування, які з'являються поза області інтерпретації будь-якого квантора спільності, можна замінити довільним ім'ям (його називають константою Сколема), в той час як екзистенційні змінні, які можуть існувати усередині області інтерпретації одного або більше кванторів спільності, можуть бути замінені функціями Сколема. Функція Сколема-це функція з довільним ім'ям, яка має такий зміст: "значення даної змінної є деяка функція від значень, привласнених універсальним змінним, в області інтерпретації яких вона лежить".
(5) Перетворення в префіксной форму. На цей крок всі залишилися квантори (залишаться тільки квантори спільності) переносяться "в голову" вираження і таким чином виявляються зліва в списку квантифікованій змінних. За ними йде матриця, в якій відсутні квантори.
(6) Рознести оператори диз'юнкції і кон'юнкції.
(7) Відкинути квантори спільності. Тепер всі вільні змінні є неявно універсально квантифікованій змінними. Екзистенціальні змінні стануть або константами, або функціями універсальних змінних.
(8) Як і раніше, відкинути оператори кон'юнкція, залишивши безліч фраз.
(9) Знову перейменувати змінні, щоб одні й ті ж імена не зустрічалися в різних фразах.
Обчислення предикатів у спрощеному вигляді. Там вираз виду
at (робот, комнатаА)
означає, що робот знаходиться в кімнаті А. Терми робот і комнатаА в цьому виразі представляли собою константи, які описували певні реальні об'єкти. Але що буде означати вислів виду
at (X, комнатаА),
в якому х є змінною? Чи означає воно, що щось знаходиться в кімнаті А? Якщо це так, то говорять, що змінна має екзистенційну підстановку (імпорт). А може бути, вираз означає, що всі об'єкти знаходяться в кімнаті А? У такому випадку змінна має універсальну підстановку. Таким чином, відсутність набору чітких правил не дозволяє однозначно інтерпретувати наведену формулу.
Перераховані в цьому розділі правила обчислення предикатів забезпечують однозначну інтерпретацію виразів, що містять змінні.
Зокрема, фраза
at (X, комнатаА) <-at (X, ящік1) інтерпретується як
"Для всіх XX знаходиться в кімнаті А, якщо X знаходиться в ящику 1". У цій фразі змінна має універсальну підстановку. Аналогічно, фраза
at (X, комнатаА) <-інтерпретується як "для всіх XX знаходиться в кімнаті А". А от фраза
<- At (X, комнатаА) інтерпретується як "для всіх XX не знаходиться в кімнаті А".
Іншими словами, це не той випадок, коли деякий об'єкт X знаходиться в кімнаті А і, отже, змінна має екзистенційну підстановку.
Тепер можна перетворити фразова форму, в якій позитивні літерали згруповані ліворуч від знаку стрілки, а негативні - праворуч. Якщо фраза у формі
P1, ..., Рт <- q1, ... qn містить змінні х1 ,..., Xk, то правильна інтерпретація має наступний вигляд:
для всіх x1, ..., хk
p1 або ... або pm є істинним, якщо q1 і ... і qn є істинними.
Якщо п = 0, тобто відсутній хоча б одна умова, то вираз буде інтерпретуватися наступним чином:
для всіх x1, ..., xk
p1 або ... або рт є істинним.
Якщо т = 0, тобто відсутні терми висновку, то вираз буде інтерпретуватися наступним чином:
для всіх x1, ..., xk
не має значення, що q1 і ... і qn є істинними.
Якщо ж т = п = 0, то ми маємо справу з порожньою фразою, яка завжди інтерпретується як помилкова.
3.2 Програмування на Пролозі.
При програмуванні на Пролозі зусилля програміста повинні бути спрямовані на опис логічної моделі фрагмента предметної області розв'язуваної задачі в термінах об'єктів предметної області, їх властивостей і відносин між собою, а не деталей програмної реалізації. Фактично Пролог являє собою не стільки мова для програмування, скільки мова для опису даних і логіки їх обробки. Програма на Пролозі не є такою у класичному розумінні, оскільки не містить явних керуючих конструкцій типу умовних операторів, операторів циклу і т.д. Вона являє собою модель фрагмента предметної області, про який йде мова в задачі. І рішення задачі записується не в термінах комп'ютера, а в термінах предметної області розв'язуваної задачі, в дусі модного зараз об'єктно програмування.
Пролог дуже добре підходить для опису взаємин між об'єктами. Тому Пролог називають реляційною мовою. Причому "Реляційність" Прологу значно могутніша й розвинена, ніж "Реляційність" мов, що використовуються для обробки баз даних. Часто Пролог використовується для створення систем управління базами даних, де застосовуються дуже складні запити, які досить легко записати на Пролозі.
У Пролозі дуже компактно, у порівнянні з імперативними мовами, описуються багато алгоритмів. За статистикою, рядок вихідного тексту програми мовою Пролог відповідає чотирнадцяти рядкам вихідного тексту програми на імперативному мовою, вирішальному ту ж задачу. Пролог-програму, як правило, дуже легко писати, розуміти й налагоджувати. Це призводить до того, що час розробки програми мовою Пролог у багатьох випадках на порядок швидше, ніж на імперативних мовах. У Пролозі легко описувати й обробляти складні структури даних.
Прологу притаманний ряд механізмів, якими не володіють традиційні мови програмування: зіставлення зі зразком, висновок з пошуком і поверненням. Ще одна істотна відмінність полягає в тому, що для зберігання даних у Пролозі використовуються списки, а не масиви. У мові відсутні оператори присвоювання і безумовного переходу, покажчики. Природним і часто єдиним методом програмування є рекурсія. Тому часто виявляється, що люди, які мають досвід роботи на процедурних мовах, повільніше освоюють декларативні мови, ніж ті, хто ніколи раніше програмуванням не займався, тому що Пролог вимагає іншого стилю мислення, відмови від стереотипів імперативного програмування.
Фрази Хорна (Horn clause) представляють собою підмножина фраз, які містять лише один позитивний літерал. У загальному вигляді фраза Хорна представляється виразом
У мові PROLOG ця ж фраза записується в такому вигляді:
р: - q1 ,..., qn. Така фраза інтерпретується наступним чином:
"Для всіх значень змінних у фразі p істинно, якщо правдиві q1 і ... і qn",
тобто пара символів ": -" читається як "якщо", а коми читаються як "і".
PROLOG - це не зовсім звичайну мову програмування, в якому програма складається в основному з логічних формул, а процес виконання програми представляє собою доказ теореми певного виду.
Фраза у формі
р: - q1, ..., qn.
може розглядатися в якості процедури. Така процедура передбачає наступний порядок виконання операцій.
(1) Літерал мети зіставляється з літералом р (уніфікується з р), який називається головою фрази.
(2) Хвіст фрази ql, ..., qn конкретизується підстановкою значень змінних (або уніфікаторов), сформованих в результаті цього зіставлення.
(3) конкретизовані терми хвостовій частині утворюють потім безліч підцілей, які можуть бути використані іншими процедурами.
Таким чином, зіставлення (або уніфікація) грає ту ж роль, що й передача параметрів функції в інших, більш звичних мовах програмування.
Наприклад, розглянемо набір фраз мови PROLOG, представлених у лістингу 1. Припустимо, що a, b і з - якісь блоки в світі блоків. Дві перші фрази стверджують, що а знаходиться на (on) b, ab знаходиться на (on) с. Третя фраза стверджує, що X знаходиться вище (above) Y, якщо X знаходиться на (on) Y. Четверта фраза стверджує, що X знаходиться вище (above) Y, якщо існує якийсь інший блок Z, розміщений на (on) Y, і X знаходиться вище (above) Y.
Лістинг 1. Проста програма на мові PROLOG, що визначає ставлення
on (на)
on (а, b).
on (b, с).
above (X, Y): - on (X, Y).
above (X, Y): - on (Z, Y),
above (X, Z).
Очевидно, що від програми потрібно вивести мета above (а, с) з цієї множини фраз. Процес формулювання вираження мети включає обробку двох процедур above і використання двох фраз on. У мові PROLOG використовується "інтерпретація фраз Хорна для вирішення проблем" Фундаментальний метод докази теорем, на якому базується PROLOG, називається спростуванням резолюцій (resolution refutation).
3.3 Принцип резолюцій
Ми намагаємося спростити синтаксис обчислення таким чином, щоб зменшити кількість правил впливу, необхідне для доведення теорем. Замість дюжини або більше правил, які використовуються при доказі теорем вручну, системи автоматичного докази для фразових форм використовують єдине правило висновку - принцип резолюцій, - вперше описане Робінсоном ([Robinson, 1965]).
Розглянемо наступний приклад з обчислення висловлювань. Надалі прописними літерами Р, Q, R, ... будуть позначатися окремі фрази, а малими грецькими U, ф і Ј - пропозіціональние змінні, як і раніше.
Якщо U і ф представляють дві довільні фрази, які можна представити у кон'юнктивній нормальній формі, і
U = {U1, ..., Ui, ...., Um},
і
ф = {ф1 ..., фi ....., Фn}, і
Ui, = ¬ фi при 1 [i [mm, 1 [j [n,
то нову фразу Ј можна вивести з об'єднання U 'і ф', де
U '= U ¬ {Ui} і ф' = ф ¬ {ф,}.
Фраза Ј = U 'і ф' називається резольвенти кроку резолюції, а U й ф є батьківськими фразами. Іноді кажуть, що U і ф "стикаються" на парі доповнюють літералів Ui, і фj.
Потужність резолюції забезпечується тим, що в ній підсумовується безліч інших правил. Це стане очевидно після того, як звичайні правила будуть представлені у кон'юнктивній нормальній формі.
У лівій колонці табл. 1 перераховані найменування правил виведення, в середній показано, як вони виглядають в звичайних позначеннях, а в правій колонці - у фразовой формі. У кожного запису вираження у верхній частині представляють схему передумов, а вирази в нижній частині - схему висновків. З цієї таблиці видно, що кожне з цитованих вище п'яти правил є одним з примірників резолюції:
Таблиця 1. Узагальнення резолюції.
Протиріччя в правилі, яке зазвичай позначається значком 1, дає в результаті порожню фразу-{}. Це означає, що передумови несумісні. Якщо вважати, що передумови описують деякий стан предметної області, то такий набір передумов не може бути реально забезпечений в ній, тобто такий стан неможливо.
Головне, що компонент автоматичного доведення теорем, який є основним компонентом більшості систем штучного інтелекту і, зокрема, мов програмування штучного інтелекту, таких як PROLOG, є системою, спростування резолюцій. Для того щоб довести, що р випливає з деякого опису стану (або теорії) Т, потрібно покласти-р і спробувати довести, що з цього припущення випливає твердження, що суперечить Т. Якщо це вдасться зробити, то тим самим підтверджується затвердження р, а в Інакше воно спростовується.
У численні предикатів використання резолюцій вимагає додаткових зусиль, оскільки в цьому обчисленні присутні змінні. Основна операція зіставлення у доказі теорем за допомогою резолюцій називається уніфікацією. При зіставленні доповнюють літералів відшукується така підстановка змінних, яка перетворює обидва вирази в ідентичні.
Наприклад, вирази БЕЖІТ_БИСТРЕЕ_ЧЕМ (Х, равлик) і БЕЖІТ_БИСТРЕЕ _ЧЕМ (черепаха, Y) перетворюються на ідентичні при підстановці {Х / черепаха, Y / равлик}. Така підстановка називається уніфікатором. Наша мета - відшукати найбільш загальну підстановку такого роду.
3.4 Пошук докази в системі резолюцій
Резолюція є правило висновку, за допомогою якого можна вивести нову ППФ (правильно побудовану формулу) зі старої. Проте в приведеному вище описі логічної системи нічого не говориться про те, як виконати доказ. Звернемо основну увагу на стратегічні аспекти докази теорем.
Нехай р представляє твердження "Сократ - це людина", 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