ВУЗ: Не указан
Категория: Не указан
Дисциплина: Не указана
Добавлен: 27.11.2019
Просмотров: 1713
Скачиваний: 4
можемо вказати деякий елемент c, для якого твердження P (c, у) є істинним, але тепер c залежить від змінної у. Тому від формули vy a*? P (*, у) можна перейти до Фоомули>>P (* Ш& _Tyr 7i (v) rf деяка функц]я,_в цтрщ невизначена. Вона має назву функція Сколема.
^вантори узагальнення усуваються MexaHj4Ho на основі стандартної домовленості: вважається, що якщо фраза залежить віддеяких змінних, то всі вони зв'язані квантором узагальнення. Наприклад якщо;с,», і — змінні, то від формули здійснюється перехід
і*/* » У* УУ V* P (.т, у, z)
до формули l*(*,y,z).
Для детальнішого ознайомлення з основами числення предикатів рекомендуємо звернутися до відповідного підручника з математичної логіки, наприклад [112,179].
3. Фразова форма запису логічних формул
Як зазначалося раніше, логічна формула, записана за допомо-ю імплікацій і тотожностей, може бути переписана в термінах кон'юнк-цій, диз'юнкцій і заперечень. Розглянемо, як твердження числення преди-кііпв перетворюється на спеціальну уніфіковану фразову форму. Набори фраз, записаних у такій формі, нагадують програми логічних мов програмування, дослідження яких нас також цікавитиме. Дамо неформальний опис такого переведення, що має шість основних дій. Дія 1. Вилучення Імплікацій 1 тотожностей. Вилучення імплікацій '—»" і тотожностей "<-»" можна провести на основі формул, наведених у n. 7.2. Наприклад формула *
. all (X, чоловік (X) —> людина (X)) X *^ ^j
перетвориться на *T7" ■ / ^(
o// (X, ~ чоловік (X) v людина (X)).
ДІя 2. Втягнення заперечення всередину.
Ця дія застосовується для випадків, коли "~" вживана у формулі, що не є частковою. ТодІ робиться така заміна:
~ (людина (Іван) & живий (Іван)} переводиться у л^ ( hA- Д C\ ) "
~ (людина (Іван) v ~ живий (Іван))
~ all (Y, люди (У)) перетворюється на <vV( V/ л* /£\
exists (Y, ~люди(¥)).
Можливість цІєїдГїзумовлена такими рівностями:
~ (а & Ь) означає те саме, що й(~ a)v (~ Ь),
~ exlsts (й, г) означає те саме, що й all (й, ~г),
~ аїІ (й, г) означає те саме, що й exists (u,~fy.
Після другої дії у наших формулах залишаться лише заперечення, при-н’язані до конкретних формул. Часткові твердження з або без "~" попереду ми називаємо точними. У наступних кількох діях ми будемо поводитися з точними твердженнями як з простими одиницями.
Д|яЗ. Заміна амінних
>іа£тупна _дія включає, вилучення Існуючих кванторів.^ Це робиться шляхом вставлення нових константних символів на місце, де були змінні, що являють собою Існуючі квантори. Тобто, замість того, щоб говорити, що існує об'єкт з певним набором характеристик, можна створити ім'я для такого об'єкта і просто сказати, що в нього єСнотеми штучного інтелекту. Сурова HLM характеристики. В цьому I полягає основна суть введення сколемівських констант. Ця дія є не noBHjcTK) еквівалентною, але вона має одну важливу властивість Існує Інтерпретація символів формули, яка справджує формулу тільки тоді, коли існує інтерпретація для сколемівської версії формули. Для наших потреб цієї форми відповідності достатньо.
Тому, наприклад:
exists (X, чоловік (X), & батько (X, Іван)) перетворюється за допомогою сколемізацІЇ
на
чоловік (gl) & батько (gl, Іван)
де "gl" — деяка нова константа, що ніде раніше не використовувалась. Константа "gl" представляє певного чоловіка (чоловік), чиїм батьком (батько) був Іван (Іван). Тут важливим є застосування символу, який раніше ніде не вживався, оскільки твердження "exists " не каже, що певна людина є сином Івана, а лише стверджує, що є така людина. Може виявитись, що "gl " пов'язана з якимось іншим константним символом, але ця інформаЩя не надається даним твердженням.
Коли у формулі використовуються квантори узагальнення, сколемІза-ція стає не такою простою. Наприклад, якщо ми перетворимо
all (X, людина (X) -> exists (Y, мати (X, У))) ("кожна людина має матір") на all (X, людина (X) ->мати (X, g2)),
то це б означало, що всі люди мають одну матір — "g2 ". Коли змінні зв'язані квантором узагальнення, їх перетворюють на функціональні символи, щоб показати, наскільки "exlsts" залежить від того, з чим зв'язана змінна. Тому останній приклад потрібно перетворити таким чином:
all (X, людина (X) ->мати (X. g2 (X))).
У даному разі "g2 " позначає функціональний символ, який за ім'ям людини видасть вам ім'я ії матері.
Дія 4. Переміщення квантора узагальнення назовні.
Ця дія дуже проста. )<вантор узагальнення переміщується назовн^ при цьому Формула зберігає свій попередній зміст. Наприклад,
all (X, чоловік (X) -> all O', жінка (У) -> подобається (X, У))) перетворюється на all (X, all (Y, чоловік (X) -> (жінка (У) -» подобається (X, Y))))
Оскільки кожна змінна тепер зв'язана квантором узагальнення ззовні формули, то квантори узагальнення ббіьше не несуть додаткової інформації. Отже, можна скоротити формули, опустивши ці квантори. Ми просто мусимо пам'ятати, що кожна змінна зв'язана кванторами узагальнення, які ми опустили.
Дія 5. Перенесення "&" через 'У.
Логічна формула повинна буги зведена до особливої форми — нормальної кон'юнктивної формули, в якій кон'юнкції не з'являються посеред диз'юнкцій. Для цього існують два правила:
__ (A &B) v C дорівнює(Л y B)&\By C),
A v (В & О дорівнює {A у В) & (A v Q. ^
Наприклад, Фразу
відхідний_день (X) v (працювати (Іван, X) & (злий (Іван) v сумний (Іван))) можна трактувати так: "для будь-якого X, X може бути вихідним днем, або Іван може
Смотеми шіучіірго Інтьлвіоу. Суром Км працювати $ XI бути влим або сумним " Останню можна пере творити на фразу (вимідниО_день (X) v (працювати (Іван, X) &
((вшгідниО_день p() v (злий іІвон) v сумний (Іван))) *)
*для всІх K no-nepuia, X або вихідний, або Іван працює в X, по-друге, або вихідний або Іван сумний та злиЙ)".
^^n*RP?iAAStABMk *
Тепер наша формула e набором атомарних формул, розділених V або відв'язаних "&", Якщо не брати до уваги V, в нас може вийтитаке:
♦Де і4Лщш^Л'фАЕй> змІннІ можуть заміщати складні твердження, але без "&" всередині. Понтерше, тепер дужкинепотрКінІ, оскільки для "&" вони не мають знамення, I наш вираз еквівалентний до 4***c*o*e.
Пр-друге^порядок теж не має значення. Потрете, нам не потрібні ї "&", оскільки ми знаємо, що наша формула — це послідовність тверджень, з'єднаних "&", і останні мОЖна опустити, сказавши,що це є множина (А, В, С,щ E}. Кажучи, що це множина, ми наголошуємо на тому, що порядок не суттєвий. Елементи цієї множини називаються фразам^ Отже, будь-яка формула предикатного числення еквівалентна (в певному po зумІ н н I ЩшБн и н и фраз.
Повернемося досамої фрази. Оскільки елементами фрази є або точні, або розділені точно "v" твердження, то їХ загальний вигляд _ може набувати нікого ((K v яо v X) v (f у 2), вигляду:
де змінні є точними. Тому можна знову перейти JV> - Множини розділених ючнихфраз tyj WjX,YjZ}.
Тепер формула остаточнодосягла фразової форми.Підсумуємо дещо.
Отже, фразова форма логіки предикатів задає такий спосіб запису формул, який використовують тільки з'єднувачі типу &, v, ~.
Негативна або позитивна атомарна формула називається літералом. Кожна формула — множина літералів, які з'єднані символом v. Негативні I позитивні літерали відповідно групуються. Схематично фраза має такий вигляд:
де Я, v7yv — f.vtf,vAjv ,,. Af., />в ^ рп _ ПОЗИТИВНІ ЛІТвраЛИ, а л/р :.,Nm —
негативні. 3 іншого боку, фразу можна розглядати як узагальнення поняття імплікації. Дійсно, якщо А і В атомарні формули, тоді формулух 4 в можна переписати ів такому еквівалентномувигляді:-хув.Звідси отримаємо фразовуформулу*у~А
Фраза має таку семантику. Всі позитивні атомарні формули виступають у ролі альтернативних висновків, а негативні є необхідними умовами.Наприклад, ЛчШ v~cv~D зазначає, що A I В будуть Істинними тодіі тільки тоді, коли є
істинними C I D.
Елементарна фраза має тільки один лІтерал. Теорія записується у вигляді множини фраз, які неявно з'єднані між собою символом &. У літературі зустрічається I друга форма запису фрази за допомогою зворотної стрілки (читається як "імплІкується"). Так, остання
фраза може мати вигляд4.в^~с*~л
Для скорочення об'ємів обчислень на практиці застосовують спеціальний клас фраз
t
№1ЄМН
MHyWH'ttiMHIMKTf.
(>tW>HM
— фрази Хорна Аналогічно, фразу Хорма можна мписаш також кількома способами.
Наприклад, твердження
Jv-*v-Cv-D
екаїаалентне
X+-B.CD
1 в мовах логічного програмування набуває вигляду A:- В, C, 0.
Розглянемо ще один приклад. Нехай маемо формулу
(особа (nempo) & особа (Іван)) & ((особа (X) v ~ мати (X, y)) v *• особо (У)), яка після відповідних дій перетворюється иа-.
особа (nempo)'.-. ,
особа
(Іван):-.
особа (X):-Mamu (X, У), особа (У). Останній запис уже нагадує текст прологівськсгі програми.
4 Аналіз і доведення теорем
Тепер, коли ми знаємо, як зводити формули числення предикатів до певної стандартної форми, ми повинні дізнатися, що з ними робити, як і де їх можна застосувати. Цілком очевидно, що, маючи набір тверджень, варто дослідити, які наслідки т
з них випливають. Нагадаємо, що твердження, які ми вважаемо істинними, називають 8Кс|омами та гіпотезами, а тІ твердження, що з них випливають,— теоремами.
У цьому розділі ми' розглянемо на неформальному рівні процес автоматичного jQOBefleHJHe_TeopeM. Як уже зазначалося раніше, звістка про те, що цифрові комп'ютери можуть автоматично доводити теореми, у 60-ті роки спричинила бурхливий сплеск ентузіазму. Перші спроби знайти загальний алгоритм для вирішення задачі автоматизації дедуктивних побудов простежуються в роботах Лейбнща, Пеано, Пльберта. Центральне місце серед сучасних методів автоматичного доведення теорем займає метод резолюцій, запропонований Дж. Робінсоном у 1965 p. Використання цього методу виявилося ефективнішим, ніж класичне виведення на осно-ві modus ponens,
Оскільки числення предикатів є алгоритмічно нерозв'язним, метод ре-юлюцій дозволяє встановити, що деяка формула є теоремою, якщо вона насправді є'теорембїоГ Для формул, що не є теоремами, метод резолюцій може працювати нескінченно довго.
Саме на цій основі з'явилися ідеї, на яких базуються мови логічного програмування. Одним з фундаментальних проривів того часу було відкриття Дж. Робінсоном принципу аналізута його застосування до автоматичного доведення теорем. Аналіз — це правило висновків, як одне твердження може випливати з Іншого. Використовуючи аналітичний принцип, ми можемо на основі аксіом довести теореми стандартним шляхом з наших аксіом. Ми тільки маємо вирішити, до яких тверджень їх застосувати, \ відповідний висновокдістанемо автоматично.
Аналіз розроблено і для роботи з формулами у фразовій форм). Маючи дві фрази, що пов'язані відповідним чином, він створить нову фразу, що буде наслідком перших двох.-Основна Ідея — це те, що якщо одна й та сама часткова формула зустрічається у правІй частині однієї структури I в лівш частині Іншої. то фраза отримується з'єднанням двох фраз з вилученням дубльованих формул,які з них випливають.Наприклад: 1 злий (ман)',
сумний (hOHli>o6o4u0_день (сьогодні), йдг_дощ (сьогодні), та неприемно (Нюн):- злиО (Іван), стомлений (hoH). випливає сутий (Іван);
неприємно (Іван):іюбочий_день (сьогодні), йде_дощ (сьогодні), стомлений (Іван),
Це виведення можна Інтерпретувати так. Із тверджень "якщо сьогодні будень I йде дощ, то Ьан сумниО або злий " та "коли Іван злий та стомлений, тодІ йому неприємно " можна вивести твердження "якщо сьогодні робочий^день, або йде дощ, або Іван стомився, тодІ вІн сумний I йому неприємно ",
Але насправді не все так просто.
По-перше, набагато складніше, коли фрази містять змінні. У такому ра-и виведення вкдочае дод^т^ову операціїо, яка здІйснює "затвердження" змінних до такого випадку" коли формули можна вважати ідентичними. Наше друге спрощення — це те, що в загальному аналізі дозволяється кшь-ком літералам справа відповідати кільком літералам зліва. Але може так трапитися, що лише один лІтерал вибрано з кожного пункту. Поглянемо на прикладзІ змінними:
• будь-яка інформаційна одиниця задається вербально, тобто у формі, наближеній 7
Щ (7.2) зв'язано з "Іван" e (7.3) та 2 в (7.3) зв'язано зщ (У) в (7.2)). Тому ми можемо аналізувати (7.1) і (7.4), що дасть нам професор (Іван); професор (Іван):-.
Це рівнозначно факту: Іван — професор.
У формальному визначенні аналізу процес "спрощення", яким ми тут скористались, називається унІфІкоцІею. Даний набір часткових формул може буги уніфікованим, якщо ix можна підігнати пЩ одну. Далі ми побачимо, що уніфікація та відповідність — це одне й те саме.
Існує така можливість, що ми маємо змогу продовжувати дії аналізу відносно гіпотез і спостерігати, чи не отримаємо потрібний результат. На жаль, ми не можемо цього гарантувати, навітьякщотелвердження, в якому ми зацІкавлен{, і справді випливає зтих, що маємо. Наприклад у полередньомупрйкладі ми неможемо отримати окремий пункт "професор (Іван) ", хоча це і логічно. Чи не означає це, що аналіз не є достатньо ефективним засобомдля наших цілей? Але це не так. Ми можемо переорієнтувати наші
Сшммміммпійиммм ( 'тмН М. зусилля таким чином, щоб аналіз гарантовано міг вирішувати наші задачі, якщо це взагалі можливо.
Важливою властивістю аналізу t та, що якщо набір пунктів непослідовний, то аналіз зможе отримати s них лише порожній пункт
Набір формул є непослідовним, якщо на існує можливостей інтерпретації предикатів, константних символів і символів функцій, що дозволило б швидко виразити твердження. Порожній пункт є логічним вираженням помилковості I релрезентуе твердження, яке не може бути вірним. Отже, аналіз може нам сказати, коли наші формули неправильні, отримуючи цейдоказ суперечності.