Головна

Методи пошуку рішень на основі числення предикатів

  1. I. Неекспериментальні методи
  2. II. Арени. Методи отримання.
  3. II. Основні методи збору соціологічної інформації, їх коротка характеристика.
  4. II. експериментальні методи
  5. II. МЕТОДИ ДЕРЖАВНОГО УПРАВЛІННЯ.
  6. IV. Використання даних управлінського обліку для аналізу і прийняття управлінських рішень.
  7. IV. Методи дослідження виконавчої та пізнавальної діяльності

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

У численні висловів основним об'єктом є змінне висловлювання (предикат), істинність або хибність якого залежить від значень назв змінних. Так, істинність предиката "x був фізиком" залежить від значення змінної x. Якщо x - П. Капіца, то предикат істинний, якщо x - М. Лермонтов, то він хибна. Мовою обчислення предикатів твердження x (P (x) Q (x)) читається так: "для будь-якого x якщо P (x), то має місце і Q (x)". Іноді його записують і так: x (P (x) Q (x)). Виділене підмножина тотожно істинних формул (або правильно побудованих формул - ППФ), істинність яких не залежить від істинності входять до них висловлювань, називається аксіомами.

У численні предикатів є безліч правил виведення. Як приклад наведемо класичне правило відділення, або modus ponens:

(A, A B) / B

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

Modus tollendo tollens: Якщо з A слід B і B помилково, то і A помилково.

Modus ponendo tollens: Якщо A і B не можуть одночасно бути істинними і A істинно, то B помилково.

Modus tollendo ponens: Якщо або A, або B є істинним і A неправдиве, то B істинно.

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

f1& F2& ... & Fn B

або нездійсненності (тотожно-хибності) формули

f1& F2& ... & Fn& B

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

Наведемо приклад диз'юнкт:

 x (P (x, c1) Q (x, c2)).

Нехай P - предикат поважати, c1 - Ключевський, Q - предикат знати, c2 - Історія. Тепер даний диз'юнкт відображає факт "кожен, хто знає історію, поважає Ключевського".

Наведемо ще один приклад диз'юнкт:

 x (P (x, c1) & P (x, c2)).

Нехай P - предикат знати, c1 - Фізика, c2 - Історія. Даний диз'юнкт відображає запит "хто знає фізику і історію одночасно".

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

Повернемося до принципу резолюції. Головна ідея цього правила виведення полягає в перевірці того, чи містить безліч диз'юнктів R порожній (помилковий) диз'юнкт. Зазвичай резолюція застосовується з прямим або зворотним методом міркування. Прямий метод з посилок A, A B виводить висновок B (правило modus ponens). Основний недолік прямого методу полягає в його не направлення: повторне застосування методу призводить до різкого зростання проміжних висновків, не пов'язаних з цільовим висновком. Зворотний висновок є спрямованим: з бажаного укладення B і тих же посилок він виводить нове подцелевое висновок A. Кожен крок виведення в цьому випадку пов'язаний завжди з спочатку поставленої мети. Істотний недолік методу резолюції полягає в формуванні на кожному кроці виведення безлічі резольвент - нових диз'юнктів, більшість з яких виявляється зайвими. У зв'язку з цим розроблені різні модифікації принципу резолюції, що використовують більш ефективні стратегії пошуку і різного роду обмеження на вид вихідних диз'юнктів. У цьому сенсі найбільш вдалою і популярною є система ПРОЛОГ, яка використовує спеціальні види диз'юнктів, званих диз'юнкт Хорна.

Процес доведення методом резолюції (від зворотного) складається з наступних етапів:

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

Розглянемо приклади застосування методів пошуку рішень на основі числення предикатів. Приклад "цікаве життя" запозичений з [2]. Отже, задані твердження 1-4 в лівому стовпчику таблиця 3.2 Потрібно відповісти на питання: "Чи існує людина, що живе цікавим життям?" У вигляді предикатів ці твердження записані в другому стовпці таблиці. Передбачається, що X (smart (X) = stupid (X)) і Y (wealthy (Y) = poor (Y)). У третьому стовпці таблиці записані диз'юнкт.

 Таблиця 3.2. Цікаве життя
 Твердження і висновок  предикати  Пропозиції (диз'юнкт)
 1. Всі небідні і розумні люди щасливі  X (poor (X) smart (X) happy (X)) poor (X) smart (X) & happy (X)
 2. Людина, яка читає книги, - недурний  Y (read (Y) smart (Y)) read (Y) & smart (Y)
 3. Джон вміє читати і є заможною людиною read (John) poor (John) 3a read (John) 3b poor (John)
 4. Щасливі люди живуть цікавим життям  Z (happy (Z) exciting (Z)) happy (Z) & exciting (Z)
 5. Висновок: Чи існує людина, що живе цікавим життям?  W (exciting (W)) exciting (W)
 6. Заперечення укладення  W (exciting (W)) exciting (W)

Заперечення укладення має вигляд (рядок 6): W (exciting (W))

Одне з можливих доказів (їх більше одного) дає наступну послідовність резольвент:

  1. happy (Z) резольвента 6 і 4
  2. poor (X) smart (X) резольвента 7 і 1
  3. poor (Y) read (Y) резольвента 8 і 2
  4. read (John) резольвента 9 і 3b
  5. NILрезольвента 10 і 3a

Символ NIL означає, що база даних виразів містить протиріччя і тому наше припущення, що не існує людина, що живе цікавим життям, невірно.

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

Серед інших стратегій (пошук в ширину (breadth-first), стратегія "безлічі підтримки", стратегія лінійної вхідний форми) стратегія "безлічі підтримки" показує відмінні результати при пошуку в великих просторах діз'юнктівних виразів [2]. Суть стратегії така. Для деякого набору вихідних діз'юнктівних виразів S можна вказати підмножину T, зване безліччю підтримки. Для реалізації цієї стратегії необхідно, щоб одна з резольвент в кожному спростування мала предка з безлічі підтримки. Можна довести, що якщо S - нездійсненний набір диз'юнктів, а S-T - здійсненний, то стратегія безлічі підтримки є повною в сенсі спростування. З іншими стратегіями для пошуку методом резолюції в великих просторах діз'юнктівних виразів читач може познайомитися в спеціальній літературі [2], [45], [46].

Дослідження, пов'язані з доказом теорем і розробкою алгоритмів спростування резолюції, призвели до розвитку мови логічного програмування PROLOG (Programming in Logic). PROLOG заснований на теорії предикатів першого порядку. Логічна програма - це набір специфікацій в рамках формальної логіки. Незважаючи на те, що в даний час питома вага мов LISP і PROLOG знизився і при вирішенні завдань ІІ все більше використовуються C, C ++ і Java, проте багато завдань і розробка нових методів вирішення завдань ІІ продовжують спиратися на мови LISP і PROLOG. Розглянемо одну з таких завдань - завдання планування послідовності дій та її рішення на основі теорії предикатів.

Завдання планування послідовності дій

Багато результати в області ІІ досягнуті при вирішенні "завдань для робота". Однією з таких простих в постановці і інтуїтивно зрозумілих завдань є завдання планування послідовності дій, або завдання побудови планів.

У наших міркуваннях будуть використані приклади традиційної робототехніки (сучасна робототехніка багато в чому грунтується на реактивному управлінні, а не на плануванні). Пункти плану визначають атомарні дії для робота. Однак при описі плану немає необхідності опускатися до мікрорівня і говорити про датчиках, крокових двигунах і т. П. Розглянемо ряд предикатів, необхідних для роботи планувальника зі світу блоків. Є певний робот, який є рухомий рукою, здатної брати і переміщати кубики. Рука робота може виконувати наступні завдання (U, V, W, X, Y, Z - змінні).

goto (X, Y, Z) перейти в розташування X, Y, Z

pickup (W) взяти блок W і тримати його

putdown (W) опустити блок W в деякій точці

stack (U, V) помістити блок U на верхню межу блоку V

unstack (U, V) прибрати блок U з верхньої межі блоку V

Стану світу описуються наступним безліччю предикатів і відносин між ними.

on (X, Y) блок X знаходиться на верхній межі блоку Y

clear (X) верхня межа блоку Х порожня

gripping (X) захоплення робота утримує блок Х

gripping () захоплення робота порожній

ontable (W) блок W знаходиться на столі


Мал. 3.8. Початкова та цільове стану завдання зі світу кубиків

Предметна область зі світу кубиків представлена ??на рис. 3.8 у вигляді початкового та цільового стану для вирішення завдання планування. Потрібно побудувати послідовність дій робота, провідну (при її реалізації) до досягнення цільового стану.

Стану світу кубиків представимо у вигляді предикатів. Початковий стан можна описати таким чином:

start = [handempty, ontable (b), ontable (c), on (a, b), clear (c), clear (a)]

де: handempty означає, що рука робота Роббі порожня.

Цільове стан записується так:

goal = [handempty, ontable (a), ontable (b), on (c, b), clear (a), clear (c)]

Тепер запишемо правила, що впливають на стан і призводять до нових станів.

(X) (pickup (X) (gripping (X) < (gripping () clear (X) ontable (X)))) (X) (putdown (X) ((gripping () ontable (X) clear (X) ) < gripping (X))) (X) (Y) (stack (X, Y) ((on (X, Y) gripping () clear (X)) < (clear (Y) gripping (X)))) (X) (Y) (unstack (X, Y) ((clear (Y) gripping (X)) < (on (X, Y) clear (X) gripping ()))

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

На початку 1970-х років в Стенфордському дослідницькому інституті (Stanford Research Institute Planning System) була створена система STRIPS для управління роботом. У STRIPS чотири оператори pickup, putdown, stack, unstack описуються трійками елементів. Перший елемент трійки - безліч передумов (П), яким задовольняє світ до застосування оператора. Другий елемент трійки - список доповнень (Д), які є результатом застосування оператора. Третій елемент трійки - список викреслювань (В), що складається з виразів, які видаляються з опису стану після застосування оператора.

Ведучи міркування для розглянутого прикладу від початкового стану, ми приходимо до пошуку в просторі станів. Необхідна послідовність дій (план досягнення мети) буде наступною:

unstack (A, B), putdown (A), pickup (C), stack (C, B)

Для великих графів (сотні станів) пошук слід проводити з використанням оціночних функцій. Більш докладно про роботи з планування, в тому числі сучасні публікації по адаптивному планування, можна прочитати в літературі [7], [47], [48], [49], [50].

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



Альфа-бета-процедура | Пошук рішень в системах продукцій

Методи пошуку рішень в просторі | Алгоритм найшвидшого спуску по дереву рішень | Алгоритм оціночних (штрафних) функцій | алгоритм минимакса |

© um.co.ua - учбові матеріали та реферати