Повна версія

Головна arrow Природознавство arrow ІНТЕЛЕКТУАЛЬНІ СИСТЕМИ

  • Увеличить шрифт
  • Уменьшить шрифт


<<   ЗМІСТ   >>

ЕВРИСТИКИ В УПРАВЛІННІ ВИСНОВКОМ

Взагалі кажучи, процес пошуку виведення константи Л з вихідних диз'юнктів за допомогою правил виведення R0,

Rl, R2 може виявитися неприйнятно трудомістким, навіть в розглянутому вище простому прикладі можна було б вказати достатню кількість альтернативних способів застосування правил виведення (наприклад, отримати резольвенти диз'юнктів 1 і 2, або 1 і 3).

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

  • 1) Стратегія переваги одночленним. Як неважко помітити, застосування правила резолюції до диз'юнкт А V До V • • • V K m -i і -> А ' V К [ V • • • V K 9n_i довжини тип відповідно дає резольвенту К " V • • • V K ^ -i V К" ' V • • • V До , "_ 1 довжини т + п-2. Довжина ця лише в тому випадку виявиться меншою довжини одного з вихідних диз'юнктів, коли інший диз'юнкт мав довжину 1, тобто був "одночленной". Виходячи з такого, взагалі кажучи, евристичного міркування отримання наслідків, більш простих ніж вихідні формули, стратегія переваги одночленним рекомендує першочергове застосування правила резолюції до одночленной.
  • 2) Виключення тавтологію і унікальних літер: в процесі виведення наслідків відкидаються диз'юнкт виду V -> А V В V • • • V Bk) ( "тавтології"). Якщо предикатний символ Р зустрічається у всіх диз'юнкт тільки з запереченням, або тільки без заперечення, то все що містять Р диз'юнкт відкидаються.

Стратегія переваги одночленним дає приклад стратегії упорядкування, принцип виключення тавтологію і унікальних літер - приклад стратегії очищення.

  • 3) Стратегія першочергового застосування правила склеювання: правило R1 застосовується лише після того, як були отримані всі можливі в поточній ситуації слідства із застосуванням правила R2.
  • 4) Стратегія використання подслучаев. Диз'юнкт D називається подслучаем диз'юнкт С, якщо існує така підстановка <7, що С має вигляд cr (D) V С '. Стратегія полягає в відкиданні всіх виникаючих при виведенні диз'юнктів С , для яких вже знайдений був раніше деякий їх подслучай (дана стратегія є стратегією очищення і гарантує отримання за кінцеве число кроків константи Л).
  • 5) Стратегія застосування несе безлічі диз'юнктів. Ця стратегія пов'язана з виділенням в вихідному безлічі диз'юнктів М такого, можливо більшого підмножини М ', про яке відомо, що воно реально (наприклад М' може бути утворено всіма аксіомами, у тому числі потрібно витягти заданий наслідок). При виведенні наслідків допускається лише таке застосування правила резолюції, коли хоча б один з несучих диз'юнктів належить несе безлічі. Останнє визначається наступним індуктивним чином:
    • а) Кожен елемент з ММ ' відноситься до несучого безлічі.
    • б) Якщо резольвента отримана за участю хоча б одного елемента несе безлічі, то вона входить в несе безліч.
    • в) Результати застосування правила R0 або R2 до елементу несе безлічі дають елемент несе безлічі.
  • 6) стратегія використання лінійних висновків. Лінійний висновок являє собою послідовність застосувань правила резолюції визначається діаграмою такого вигляду:

Тут кожне З { - або елемент вихідної множини диз'юнктів М, або є якийсь Dj при j ? {0,1, ..., г - 1}. Має місце твердження (Андерсон-Бледсоу), згідно з яким для отримання константи Л досить використовувати лише лінійні висновки (тут і далі ми розглядаємо лише зустрічаються в висновках правила R1, так як саме вони відповідальні за експоненціально наростаючу зі збільшенням глибини виведення трудомісткість пошуку докази, які не згадуючи про можливі застосування "одномісних і правил R0 і R2). Зауважимо, що саме по собі обмеження лінійності висновку не усуває деревовидної схеми пошуку лінійного виводу при переборі різних возможн стей для C ^ Cj, ..., С п .

  • 7) Спільне застосування стратегій використання подслучаев і злиття. Введемо спочатку допоміжні поняття злиття та літери злиття. Резольвента a (D [ ) V ••• V (r (D ' n ) V a (D ") V • • • V <т (?>") Двох диз'юнктів А V D V • • • V D' n і -ii4 V D " V • • • V називається злиттям цих диз'юнктів, якщо існують такі i 6 {1, ..., п} иг 6 {1, ..., т}, що a (D [) = a ( Dj). Формула (t (D [) при цьому називається літерою злиття. Андерсону і Бледсоу належить твердження про те, що при пошуку виведення константи Л досить обмежиться лише такими лінійними висновками, у яких кожне Ci (позначення ті ж, що в пункті 6 ) або належить вихідного безлічі диз'юнктів М, або є деяким Dj, j <г, отриманим при злитті двох діз'ю Ктов, причому літерою (уніфікуючих при застосуванні правила резолюції формулою А або - • А ') в Ci при отриманні Di є деяка літера злиття, а саме Di є подслучаем диз'юнкт Di-i. Незважаючи на суттєве обмеження у використанні формул Ci ) котрі належать до М (в порівнянні з пунктом 6), дане твердження практично не усуває ефект експоненціального наростання трудомісткості, так як достатня кількість альтернативних застосувань правил виведення на кожному кроці дає вже вихідне безліч М.
  • 8) Стратегія упорядкування літер. Можливе застосування при пошуку виведення константи Л іншого обмеження на вид лінійного виводу. В цьому випадку роздільною літерою в кожному D x є перша літера, тобто D i + i виникає з Di = Av DV • • -V D ' n і = Z ^ V- • -VZ ^ V-A'VjD ^ V * • V? ^ як

причому вказане тут впорядкування літер в диз'юнкт Д + i зберігається. Як і в пункті 7, передбачається, що кожне С * - або з початкової множини диз'юнктів М, або збігається з деяким Dj, j <г, що є диз'юнкт злиття. Повнота даної стратегії також була встановлена в роботах Андерсона і Бледсоу.

Для ілюстрації застосування перерахованих вище стратегій розглянемо порівняно простий приклад доведення теорем з теорії груп. Буде доводитися твердження про те, що в асоціативної системі в якій рівняння виду ха = 6 і ay = b мають ліве і праве рішення х і у, існує правий одиничний елемент, при формулюванні цього твердження на мові логіки предикатів використовуємо тримісний предикатний символ P (x y y y z), що інтерпретується як рівність ху = z. Після перетворення до виду диз'юнктів аксіоми існування рішень рівнянь ха = Ь і ay = Ь приймають вид:

існування рішення для ха = Ь; існування рішення для ау = 6.

Асоціативність виражається двома диз'юнкт:

Нарешті, заперечення твердження про існування правого одиничного елемента приводиться до вигляду:

У вихідній ситуації несе безліч складається з єдиного елемента?> 5, при застосуванні правил виведення будемо будувати лише лінійні висновки. Стратегія переваги одночленним дає лише дві можливості - застосування правила R1 до D5 і?) З, або до /) 5 і D 4 . Виберемо, наприклад, першу з них, отримаємо диз'юнкт:

(у міру потреби в нових диз'юнкт проводимо переобозначеніе змінних). Тепер несе безліч має вже два елементи - D $ і?) Б, і стратегія переваги одночленним залучає в розгляд також диз'юнкт D і Дг- Застосовуючи правило R1 до D і Dq, отримуємо диз'юнкт:

Далі з D? і D виводимо:

і, нарешті, уніфікуючи А з запереченням Z> 2, виводимо константу Л.

Розбираючи приклад, ми привели лише веде до мети мети ланцюжок виведення. Разом з тим, тут було вже досить велика кількість альтернативних висновків, не відсікаються перерахованими вище стратегіями: застосування правила резолюції до парам (?> 5,1) 4), (?> 2 ,?> Б), (А, А), а також альтернативні застосування цього правила до (а> а) і (а »а) дають нові диз'юнкт, які в свою чергу призводять до нових наслідків. Таким чином, в цілому зберігається розгалужених характер розглянутого в описаній процедурі логічного висновку, і це обмежує область ефективної її застосовності класом порівняно простих завдань, де проведення повного перебору є все ще реалізованим.

Спроби застосування викладеної вище процедури автоматичного доведення теорем в різних прикладних задачах, пов'язаних з логічним висновком, привели до створення мови ПРОЛОГ. Не зупиняючись на технічних подробицях, викладених в інструкціях з програмування на цій мові, ми наведемо тут лише "загальнологічних" схему організації та функціонування програм на ПРОЛОГ'е. кожна така програма являє собою упорядкований набір диз'юнктів (А>?> 2, ..., А) »причому вхідний інформацією для програм також служить деякий диз'юнкт?> о. Програма намагається знайти таку підстановку сг, для якої сукупність диз'юнктів {а (А), А> А> • • •> А} стає нездійсненним, причому вона не зупиняється, знайшовши першу таку <т, а продовжує пошук і перераховує всі знайдені а аж до вичерпання всіх можливостей, закладених в її схемі перерахування. Сама ця схема виключно проста - по суті, це повний перебір всіх можливих лінійних висновків, які визначаються диз'юнкт А, ...,?> П , реалізований за принципом "спочатку вглиб". Більш детально, функціонування програми відбувається наступним чином. Поточна ситуація описується за допомогою набору трійок 5 = (5i, ..., S m ), де кожне S it i = 1, ..., m, має вигляд (сг *, Д *, & Л, Oi - підстановка, Щ - диз'юнкт, ki € {1,2, ..., п + 1}. У вихідній ситуації т = 1, <7i = е - тотожна підстановка, D =?> о,

до = 1. На черговому кроці перетворень відбувається розгляд "поточної" трійки S m = (a m , fc m ), VK Si

і перебір всіх диз'юнктів номер яких не менше до т . Для кожного Dj, Dj = Q i V • • • V Q Pi робиться спроба уніфікації літер До 1 і -iQi . Як тільки це вдалося зробити, визначається резольвента D ' диз'юнктів D * m і Dj, і до кінця набору S приєднується нова трійка т о * 9 D 1), де о * - уніфікуються підстановка. Одночасно індекс до т в трійці S m замінюється на j + 1, і процес відновлюється. Якщо перегляд усіх диз'юнктів Dj закінчився безрезультатно і нова трійка S m +1 не виникла, то або т = 1, і тоді програма завершує роботу (тобто завершує процес перерахування результуючих підстановок), або т> 1, і тоді трійка S m відкидається, після чого - перехід до наступного кроку. Винятковим є випадок, коли диз'юнкт D ' виявився константою Л. В цьому випадку трійка S m + i не вводиться, а лише робиться заміна кт на j + 1 і відбувається видача чергового результату - підстановки т а'. Потім - перехід до чергового кроку.

Диз'юнкт D {= Q V- • vQ p ПРОЛОГ-програми можна інтерпретувати як послідовність "операторів" • • •, виконуваних як підпрограми для реалізації умови Q. Тут виникають два принципово різних властивості, яких не було у операторів програмування "звичайних" алгоритмічних мов. По-перше, відсутній чіткий поділ програмних змінних, що зустрічаються в операторі, на вхідні і вихідні, і в різних ситуаціях в одній і тій же програмі ролі таких змінних можуть змінюватися. По-друге, оператор реалізується як би в режимі перерахування своїх "вихідних" змінних: спочатку знаходиться перша версія набору цих значень, реалізуються наступні оператори, і якщо при їх обробці виникає в певний момент помилкове умова, то відбувається повернення до раніше розглянутого оператору, який видає чергову версію набору значень вихідних змінних, і так далі.

Такий "режим перерахування" істотно спрощує програмування: зникають не тільки ускладнюють налагодження оператори "goto", але і стають вкрай рідкісними в явно виділені в програмі конструкції з циклами, так як ці цикли реалізуються автоматично. Мабуть, вказане обставина і обумовило в значній мірі подальший розвиток ПРОЛОГ'а - в першу чергу поява в ньому великої кількості вбудованих предикатів, що реалізуються інтерпретатором (або компільованих) без залучення механізму логічного висновку, але зі збереженням зазначеного принципу перерахування вихідних значень. У ПРОЛОГ були введені також деякі додаткові засоби управління ходом виконання програми, і в кінцевому підсумку програмування на ньому значно наблизилося до програмування на традиційних алгоритмічних мовах, хоча б в тому сенсі, що написання програми тут також повинна передувати розробка алгоритму, що враховує істотно специфіку конкретної завдання і включає в себе оптимізацію застосовуваної схеми обчислень. Практична значимість описаної вище процедури автоматичного доведення теорем як універсального засобу вирішення завдань виявилася в результаті вельми скромною, будучи явно відсунути на другий план надається ПРОЛОГ'ом можливістю програмувати "майже без циклів".

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

вправи

3.10. Які з наступних виразів є правильними виразами (формулами і термами) логіки предикатів:

  • 3.11. Індукцією з побудови формули доведіть лему 15 про інтерпретації.
  • 3.12. Вказати вільні і пов'язані входження змінних в наступні формули:

3.14. Показати, що такі формули не є загальнозначущими:

3.15. Показати, що якщо А і В - формули логіки предикатів, то наступні формули є загальнозначущими:

3.16. Довести, що будь-яка формула А з вільними змінними xi, ... х п здійсненна тоді і тільки тоді, коли здійсненна формула 3xi • • • 3 х п А.

3.17. Довести, що будь-яка формула А з вільними змінними xi, ... х "общезначима тоді і тільки тоді, коли общезначима формула Vxi ... Vxni4.

 
<<   ЗМІСТ   >>