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

Нижче наведені синтаксичні  правила обчислення предикатів першого  порядку.

Будь-який символ (константа  або змінна) є термо. Якщо 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. Узагальнення резолюції.

Правило виводу  Звичайна форма  Кон'юнктивна нормальна форма  

Modus ponens  (U  ф, U) / Ф  {¬ U, Ф}, {U} / {ф}  

Modus fallens  (U  ф. ¬ ф) /-U  {¬ U, ф },{-, ф} / {-U}  

Зчеплення  (U  ф, ф  Ј) (U  Ј)  {¬ U, ф}, {¬ ф, Ј} / {¬ U, Ј}  

Злиття  (U  ф, ¬ U  ф) / ф  {U, ф}, {¬ U, ф} / {ф}  

Reductio  (U, ¬ U) / |  {¬ U}, {U} / {}  

Протиріччя в правилі, яке зазвичай позначається значком 1, дає в результаті порожню фразу-{}. Це означає, що передумови несумісні. Якщо вважати, що передумови описують деякий стан предметної області, то такий набір передумов не може бути реально забезпечений в ній, тобто такий стан неможливо.

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

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

Наприклад, вирази БЕЖІТ_БИСТРЕЕ_ЧЕМ (Х, равлик) і БЕЖІТ_БИСТРЕЕ _ЧЕМ (черепаха, Y) перетворюються на ідентичні при  підстановці {Х / черепаха, Y / равлик}. Така підстановка називається уніфікатором. Наша мета - відшукати найбільш загальну підстановку такого роду.

3.4 Пошук докази в системі резолюцій