Новости

Хорнівські диз’юнкти. Принцип резолюцій. Алгоритм уніфікації. Процедура доказу теорем методом резолюцій для хорнівських диз’юнктів. Особливості роботи з негативними знаннями в Пролозі

Работа добавлена:






Хорнівські диз’юнкти. Принцип резолюцій. Алгоритм уніфікації. Процедура доказу теорем методом резолюцій для хорнівських диз’юнктів. Особливості роботи з негативними знаннями в Пролозі на http://mirrorref.ru

Лекція 2.

Логічні основи Прологу

Хорнівські дизюнкти. Принцип резолюцій. Алгоритм уніфікації. Процедура доказу теорем методом резолюцій для хорнівських диз’юнктів. Особливості роботи з негативними знаннями в Пролозі.

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

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

Говорять, що задано якусь формальну систему F, якщо визначені:

  1. алфавіт системи — лічильна кількість символів;
  2. формули системи — деяка підмножина всіх слів, які можна утворити із символів, що входять в алфавіт (звичайно задається процедура, що дозволяє складати формули із символів алфавіту системи);
  3. аксіоми системи — виділена множина формул системи;
  4. правила виводу системи — скінченна  множина відносин між формулами системи.

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

Алфавіт логіки першого порядку становлять наступні символи:

  1. змінні (будемо позначати їх останніми літерами англійського алфавітуu, v, x, y, z);
  2. константи (будемо позначати їх першими літерами англійського алфавітуa, b, c, d);
  3. функціональні символи (використаємо для їхнього позначення ближні літериf іg);
  4. предикатні символи (позначимо їх дальніми літерамиp,q іr);
  5. пропозиціональні константи істина та неправда (true іfalse);
  6. логічні зв'язки¬ (заперечення),(кон’юнкція),(диз'юнкція),(імплікація);
  7. квантори: (існування), (загальності);
  8. допоміжні символи(,),,.

Усякий предикатний і функціональний символ має визначене число аргументів. Якщо предикатний (функціональний) символ маєn аргументів, він називаєтьсяn-місцевим предикатним (функціональним) символом.

Термом будемо називати вираз, утворений із змінних та констант, можливо, із застосуванням функцій, а точніше:

  1. усяка змінна або константа є терм;
  2. якщоt1,...,tn — терми, аfn-місцевий функціональний символ, тоf(t1,...,tn) — терм;
  3. інших термів немає.

По суті справи, всі об'єкти в програмі на Пролозі представляються саме у вигляді термів.

Якщо терм не містить змінних, то він називаєтьсяосновним абоконстантним термом.

Атомна абоелементарна формула отримується шляхом застосування предиката до терм, точніше, це виразp(t1,...,tn), деp — n-місцевийпредикатний символ, аt1,...,tn — терми.

Формули логіки першого порядку отримуються  наступним чином:

  1. всяка атомна формула і є формула;
  2. якщоA іB — формули, аx — змінна, то вираз¬A(читається "не A" або "заперечення A"),A B (читається "A і B"),A B (читається "A або B"),A B (читається "Aтягне B"),х (читається "для деякого x" або "існує x") іx (читається "для будь-якого x" або "для всякого x")- формули;
  3. інших формул немає.

У випадку якщо формула має виглядx абох, її підформулаA називаєтьсяобластю дії квантораx абох відповідно. Якщо входження змінноїx у формулу перебуває в області дії квантораx абох, то воно називаєтьсязв'язаним входженням. У протилежному випадку входження змінної у формулу називаєтьсявільним.

Щоб не збільшувати надмірно обсяг лекції, ми не будемо розглядати повний список аксіом і правил виводу логіки першого порядку. Ті з них, які знадобляться нам надалі, будуть наведені у відповідних місцях.

Літералом будемо називати атомну формулу або заперечення атомної формули. Атом називаєтьсяпозитивним літералом, а його заперечення —негативним літералом.

Диз’юнкт — це диз'юнкція скінченного числа літералів. Якщо диз’юнкт не містить літералів, його називаютьпорожнім диз’юнктом і позначають за допомогою символу.

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

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

Формула перебуває у попередній (абопрефексній)нормальній формі, якщо вона представлена у виглядіQ1x1,...,Qnxn, деQi — це квантор або , а формулаA не містить кванторів. ВиразQ1x1,...,Qnxn називаютьпрефіксом, а формулуAматрицею.

Формула перебуває всколемівській нормальній формі, якщо вона перебуває у попередній нормальній формі та не містить кванторів існування.

Алгоритм приведення довільної формули обчислення предикатів до множини диз’юнктів

Перший крок. Зводимо вихідну формулу до попередньої нормальної форми. Для цього:

  1. користуючись еквівалентністюA B ¬AB виключимо імплікацію;
  2. перенесемо всі заперечення усередину формули, щоб вони стояли тільки перед атомними формулами, використовуючи наступні еквівалентності:
  3. ¬(A  B)  ¬A  ¬B
  4. ¬(A  B)  ¬A  ¬B
  5. ¬(xA)  x¬A
  6. ¬(xA)  x¬A
  7. ¬¬A A
  8. перейменовуємо зв'язані змінні так, щоб жодна змінна не входила в нашу формулу одночасно пов'язано і вільно.
  9. виносимо квантори в початок формули, використовуючи еквівалентності:

Qx(x) B Qx(A(x) B), якщоB не містить змінноїx, аQ {, }

Qx(x) B Qx(A(x) B), якщоB не містить змінноїx, аQ {, }

x(x)  x(x)  x(A(x)  B(x))

x(x)  x(x)  x(A(x)  B(x))

Q1x(x) Q2x Q1x2y(A(x) B(y)), деQ {, }

Q1x(x) Q2x Q1x2y(A(x) B(y)), деQ {, }

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

Якщо усунений квантор існування - самий лівий квантор у префіксі формули, замінимо всі входження у формулу змінними, зв'язаними цим квантором, на нову константу і викреслимо квантор із префікса формули.

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

Провівши цей процес для всіх кванторів існування, одержимо формулу, що перебуває в сколемівській нормальній формі. Алгоритм усунення кванторів існування придумав Сколемо в 1927 році.

Має місце теорема про те, що формула і її сколемізація еквівалентні в сенсі виконуваності.

Третій крок. Елімінуємо квантори загальності. Отримана формула буде безкванторною і еквівалентна вихідній в сенсі виконуваності.

Четвертий крок. Приведемо формулу до конюнктивної нормальної форми, для чого скористаємося еквівалентностями, що виражають дистрибутивність:

A  (B  C)  (A  B)  (A  C)

A  (B  C)  (A  B)  (A  C)

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

Отримаємо множину диз’юнктів, еквівалентну вихідній формулі в тому сенсі, який дає нам наступна теорема.

Теорема. Формула є тотожно помилковою тоді й тільки тоді, коли множина диз’юнктів, отриманих з її, являється невиконуваною.

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

Приклад. Перетворимо формулуx(P(x) y(P(y) ¬Qx,y))) в еквівалентну їй множину диз’юнктів.

Перший крок. Приведемо вихідну формулу до попередньої нормальної форми. Елімінувавши імплікацію, одержимо формулуx(¬Px) y(P(y) ¬Q(x,y))). Винесемо зміннуy за дужки:xy(¬Px) (P(y) ¬Q(x,y))). Це можна зробити, тому що формула¬Px) не залежить від змінноїy. Якби вона залежала, то можна було б перейменувати зв'язану зміннуy.

Другий крок. Проведемо сколемізацію отриманої формули. Лівіше квантора існування знаходиться квантор загальності, виходить, потрібно замінити всі входження змінної y новим унарним функціональним символом, залежним відx. Одержимо формулу, що перебуває в сколемівській нормальній формі:x(¬Px) (P(f(x) ¬Q(x,f(x)))).

Третій крок. Елімінуємо квантор загальності:¬Px) (P(f(x)) ¬Q(x,f(x))).

У четвертому та п'ятому кроках необхідності немає, оскільки формула вже являє собою диз’юнкт:¬Px) P(f(x)) ¬Q(x,f(x)).

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

Підстановка — це множина виду{x1/t1,..., xn/tn}, де для всіхi,xi — змінна, аti — терм, причомуxiti (відображення змінних у терми). При цьому всі змінні, вхідні в підстановку, різні (для будь-якогоij xixj).

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

Підстановка, у якій всі терми основні, називаєтьсяосновною підстановкою.

Простий вираз — це терм або атомна формула.

ЯкщоA — простий вираз, аθ — підстановка, то отримується шляхом одночасної заміни всіх входжень кожної змінної зA відповідним термом. називається окремим випадком (прикладом) виразуA. Змістовно підстановка заміняє кожне входження змінноїxi на термti.

Нехайθ іη — підстановки,θ={x1/t1,..., xn/tn},η={y1/s1,...,yn/sn}. Композиціяθη отримується з множини{x1/t1η,...,xn/tnη,y1/s1,..., yn/sn} видаленням парxi/tiη, деxitiη і парyi/si, деyi співпадають з одним ізxj.

Приклад. Нехайθ={x/f(y),y/z}, η={x/a,y/b,z/y}. Побудуємоθη. Для цього візьмемо множину{x/f(b),y/y,x/a,y/b,z/y} і викинемо з нього париy/y (тому що замінювана змінна співпадає з термом),,x/a,y/b (тому що замінювана змінна з підстановкиη співпадає із замінюваною змінної з підстановкиθ). Одержимо відповідь:θη={x/f(b),z/y}.

Підстановкаθ називаєтьсябільш загальною, ніж підстановкаη, якщо існує така підстановкаγ, щоη=θγ.

Підстановкаθ називаєтьсяуніфікатором простих виразівA іB, якщоAθ=Bθ. ПроA іB у такій ситуації говорять, що вониуніфіковані.Уніфікація використовується в Пролозі для композиції і декомпозиції структур даних.

Приклад.A=p(f(x),z) іB=p(y,a) уніфіковані. Можна взяти в якості їхнього уніфікатора підстановку{y/f(x),z/a} або підстановку{y/f(a),x/a,z/a}.

Загалом кажучи, дві формули можуть мати нескінченно багато уніфікаторів. Уніфікаторθ називаютьнайбільш загальним (абонайпростішим)уніфікатором простих виразівA іB, якщо він є більш загальною підстановкою, ніж всі інші уніфікатори простих виразівA іB.

Приклад. У розглянутому вище прикладі найбільш загальним уніфікатором є підстановка{y/f(a),z/a}.

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

Пример.НехайS={p(f(x),h(y),a),p(f(x),z,a),p(f(x),h(y),b)}.Множинанеузгодженостей дляS d(S)={h(y),z}.

Алгоритм уніфікації

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

Крок 1. Припустимоk=0,0.

Крок 2. ЯкщоSk — одноелементна множина, зупиняємо алгоритм,k — найбільш загальний уніфікатор дляS. У протилежному випадку будуємо множину неузгодженостейd(Sk) і переходимо до третього кроку.

Крок 3. Якщо вd(Sk) існує зміннаx і термt такі, щоx не входить вt, то припускаємо щоk+1=k{x/t}. Збільшуємо на одиницюk, переходимо до другого кроку. Інакше зупиняємо алгоритм, множинаS не уніфікована.

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

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

Тепер можна перейти до розглядуметоду резолюцій.

У чому взагалі полягає завдання? Ми хочемо побудувати алгоритм, що дозволяв би нам автоматично давати відповідь на питання, чи може бути виведено деякий висновок з множини наявних посилок. Відомо, що в загальному випадку навіть для логіки першого порядку такий алгоритм неможливий. Як правило, формальні системи, для яких можна побудувати подібний розв'язний алгоритм, мають невелику виразну силу. До них, наприклад, відноситься логіка висловлювань і логіка одномісних предикатів.

Однак Робінсон вирішив, що правила виведення, використовувані комп'ютером при автоматичному виведенню, не обов'язково повинні збігатися із правилами виведення, що використовуються при "людському" виведенні. Зокрема, він запропонував замість правила виведення "modus ponens", яке затверджує, що зA іA B виводитьсяB, використати його узагальнення,правило резолюції, що складніше розуміється людиною, але ефективно реалізується на комп'ютері. Давайте спробуємо розібратися із цим правилом.

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

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

Графічно це правило можна зобразити так:

(A  B, P  ¬P/AB

ТутA P іB ¬P— батьківські диз’юнкти,P і¬P— контрарні літерали,A B — резольвента.

Якщо батьківські диз’юнкти складалися тільки з контрарних літералів, то резольвентою буде порожній диз’юнкт.

Приклад. Правило виведення "modus ponens" отримується із правила резолюції, якщо взяти в якості батьківських диз’юнктівC1=A,C2=¬AB( A B). Контрарними літералами в застосуванні цього правила будутьA і¬Aрезольвентою — формулаB.

Сформулюємо правило резолюції для логіки першого порядку.

Нехай є два диз’юнктаC1 іC2, у яких немає загальних змінних,L1 — літерал, що входить у диз’юнктC1,L2 — літерал, що входить у диз’юнктC2. Якщо літерали мають найбільший загальний уніфікаторθ, то диз’юнкт(C1θ–L1θ)(C2θ–L2θ) називаєтьсярезольвентою диз’юнктівC1 іC2. ЛітералиL1 іL2 називаються контрарними літералами. Те ж правило записується в графічному вигляді як

(A  P2, B  ¬P)/(AB)θ

ТутP1 іP2 — контрарні літерали,(A B)θ — резольвента, отримана з диз’юнкта(A B) застосуванням уніфікатораθ,A P1 іB P2 — батьківські диз’юнкти, аθ — найбільш загальний уніфікаторP1 іP2.

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

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

Можливі, загалом кажучи, три випадки:

  1. Цей процес ніколи не завершується.
  2. Серед поточноїмножини диз’юнктів не виявиться таких, до яких можна застосувати правило резолюції. Це означає, щомножина диз’юнктів виконувана, а отже, вихідна формула не виводиться.
  3. На черговому кроці отримана порожня резольвента. Це означає, щомножина диз’юнктів нездійсненна, а отже, початкова формула виводиться.

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

З іншого боку, ми опираємося на результат, що формулу можна вивести з деякої множини формул тоді й тільки тоді, коли описана множина диз’юнктів невиконувана. А також на те, що множина диз’юнктів невиконувана тоді й тільки тоді, коли з неї при застосуванні правила резолюції можна вивести порожній диз’юнкт.

По суті,метод резолюцій недосконалий і приводить до "комбінаторного вибуху". Однак деякі його різновиди (або стратегії) досить ефективні. Однієї із самих вдалих стратегій єлінійна абоSLD-резолюція дляхорнівських диз’юнктів (Linear resolution with Selection function for Definition clauses), тобто диз’юнктів, що містять не більше одного позитивного літерала. Їх називаютьпропозиціями абоклозами.

Якщо диз’юнкт складається тільки з одного позитивного літерала, він називаєтьсяфактом. Диз’юнкт, що складається тільки з негативних літералів, називаєтьсяпитанням (абометою абозапитом). Якщо диз’юнкт містить і позитивний, і негативні літерали, він називається правилом. Правило виведення виглядає приблизно так¬A¬A2...¬AnB. Це еквівалентно формуліA1 A2... An B, що на Пролозі записується у вигляді

B:–A1,A2,...,An.

Логічною програмою називається кінцева не порожня множинахорнівських диз’юнктів (фактів і правил).

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

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

У підсумку виконання програми може завершитися невдачею, якщо одну з підмети не вдалося уніфікувати з жодним дизъюнктом програми, і може завершитися успішно, якщо був виведений порожній диз’юнкт, а може й просто зациклитися.

Хорнівські диз’юнкти. Принцип резолюцій. Алгоритм уніфікації. Процедура доказу теорем методом резолюцій для хорнівських диз’юнктів. Особливості роботи з негативними знаннями в Пролозі на http://mirrorref.ru


Похожие рефераты, которые будут Вам интерестны.

1. Реферат Жанрові та концептуальні особливості роману Л. Толстого «Анна Кареніна». Художній паралелізм композиції як основних художній принцип втілення проблематики роману; особливості його стилю

2. Реферат Основніфункції і особливості роботи в СУБД

3. Реферат Алгоритм сортировки методом пузырька

4. Реферат Алгоритм обчислення кореня рівняння методом ітерацій

5. Реферат Особливості організації методичної роботи в ліцеї, гімназії, колегіумі

6. Реферат Особливості роботи над професійно-орієнтованим завданням з курсу Диференційна психологія

7. Реферат Захмарні сховища даних. Основні поняття. Призначення. Особливості роботи

8. Реферат Магнітоелектричний логометр: конструктивні особливості, принцип дії, область застосування

9. Реферат Прилад порівняння - вимірювальний одинарний зрівноважений міст постійного струму: особливості конструкції, принцип дії, область застосування

10. Реферат Алгоритм жазу жолдарымен құрылымымен таныстыру. Алгоритм құруға үйрету