3.4. Приведення формул до нормальних форм.

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

Дамо неформальний опис такого переведення, що має шість основних дій.

Дія 1. Вилучення імплікацій і тотожностей.

Вилучення імплікацій “” і тотожностей “” можна провести на основі формул:

а  b дорівнює ( ~ а)  b,

а  b дорівнює (а & b)  (~ а & ~ b),

а  b дорівнює (а  b) & (b  а).

Так, формула "x(P(x)F(x)) перетвориться на формулу "x(~P(x)F(x)).

Дія 2. Втягнення заперечення всередину.

Ця дія застосовується для випадків, коли “~” вживана у формулі, що не є частковою. Тоді робиться така заміна на основі правил:

~ (а & b) дорівнює (~ a)  (~ b),

~ $u, r дорівнює "u, ~r,

~ "u, r дорівнює $u, ~ r.

Наприклад, ~(P(x)& F(x)) переводиться у ~ P(x)& ~F(x).

Після другої дії у наших формулах запишаться лише заперечення, прив'язані до конкретних формул. Часткові твердження з або без "~" попереду ми називаємо точними. У наступних кількох діях ми будемо поводитися з точними твердженнями як з простими одиницями.

Дія 3. Заміна змінних.

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

Тому, $x(P(x)&F(x,y)) перетворюється за допомогою сколемізації на P(c₁)&F(c₁, у),

де c₁, – деяка нова константа, що ніде раніше не використовувалась. Тут важливим є застосування символу, який раніше ніде не вживався, оскільки твердження $ не каже, що є певна відповідність, а лише стверджує, що є така відповідність існує. Може виявитись, що “с₁” пов'язана з якимось іншим константним символом, але ця інформація не надається даним твердженням.

Коли у формулі використовуються квантори узагальнення, сколемізація стає не такою простою. Наприклад yх: Р(х, у) переходимо до y Р(h(y), у)/

Дія 4. Переміщення квантора узагальнення назовні.

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

"x(P(x)"y(G(y) F(x,y))) перетворюється на "x"y (P(x) (G(y) F(x,y))).

Оскільки кожна змінна тепер зв'язана квантором узагальнення ззовні формули, то квантори узагальнення більше не несуть додаткової інформації. Отже, можна скоротити формули, опустивши ці квантори. Ми просто мусимо пам'ятати, що кожна змінна зв'язана кванторами узагальнення, які ми опустили.

Дія 5. Перенесення “&” через “”.

Логічна формула повинна бути зведена до особливої форми – нормальної кон'юнктивної формули, в якій кон'юнкції не з'являються посеред диз'юнкцій. Для цього існують два правила:

(a & b)  c дорівнює (a  b)&(b  c),

a  (b & c) дорівнює (a  b) & (a  c).

Наприклад, фразу P(x)(G(y,x)&(F(x)D(x)) можна перетворити на фразу (P(x)(G(y,x)) & (P(x)F(x)D(x)).

Дія 6. Перехід до фраз.

Тепер наша формула є набором атомарних формул, розділених “” або пов'язаних “&”. Якщо не брати до уваги “”, в нас може вийти таке:

(A&B)&(C&(D& E)),

де змінні можуть заміщати складні твердження, але без "&" всередині. По-перше, тепер дужки не потрібні, оскільки для "&" вони не мають зна­чення, і наш вираз еквівалентний до

A&B&C&D&E.

По-друге, порядок теж не має значення. По-третє, нам не потрібні і "&", оскільки ми знаємо, що наша формула – це послідовність тверджень, з'єднаних “&”, і останні можна опустити, сказавши, що це є множина {А, В, С, D, Е}. Кажучи, що це множина, ми наголошуємо на тому, що порядок не суттєвий. Елементи цієї множини називаються фразами. Отже, будь-яка формула предикатного числення еквівалентна (в певному розумінні) до множини фраз.

Повернемося до самої фрази. Оскільки елементами фрази є або точні, або розділені точно “” твердження, то їх загальний вигляд може набувати кого вигляду:

((F  W)  X )  (Y  Z),

змінні є точними. Тому можна знову перейти до множини розділених фраз {F, W, X, Y, Z}.

Тепер формула остаточно досягла фразової форми. Підсумуємо дещо.

Отже, фразова форма логіки предикатів задає такий спосіб запису фор­мул, який використовують тільки з'єднувачі типу &, , ~.

Негативна або позитивна атомарна формула називається літералом. Кожна формула – множина літералів, які з'єднані символом . Негативні і позитивні літерали відповідно групуються. Схематично фраза має такий вигляд:

Р,  P₂  ... Р_п  N_t  N₂  ... N_m,

де Р₁, ...,Р_n – позитивні літерали, a N₁, ..., N_m – негативні. З іншого бо­ку, фразу можна розглядати як узагальнення поняття імплікації. Дійсно, якщо А і В атомарні формули, тоді формулу А  В можна переписати і в такому еквівалентному вигляді: ~ A  В. Звідси отримаємо фразову фор­мулу В  ~ А.

Фраза має таку семантику. Всі позитивні атомарні формули виступа­ють у ролі альтернативних висновків, а негативні є необхідними умовами. Наприклад, AB~C~D зазначає, що А і В будуть істинними тоді і тільки тоді, коли є істинними С і D.

Елементарна фраза має тільки один літерал. Теорія записується у ви­гляді множини фраз, які неявне з'єднані між собою символом &. У літе­ратурі зустрічається і друга форма запису фрази за допомогою зворотної стрілки (читається як "імплікується"). Так, остання фраза може мати ви­гляд А, В  ~ С, ~ D.

Для скорочення об'ємів обчислень на практиці застосовують спеціаль­ний клас фраз – фрази Хорна. Аналогічно, фразу Хорна можна записати також кількома способами. Наприклад, твердження A  ~B  ~C  ~D еквівалентне A  B,C,D і в мовах логічного програмування набуває вигляду A:- В, С, D

Розглянемо ще один приклад. Нехай маємо формулу

(особа (петро) & особа (Іван)) & ((особа (X)  мати (X, Y))  ~особа (Y)), яка після відповідних дій перетворюється на:

особа (петро):-.

особа (Іван):-.

особа (Х):-мати (X, Y), особа (Y). Останній запис уже нагадує текст прологівської програми.