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, У), особа (У). Останній запис уже нагадує текст прологівськсгі програми.