Етап 2 — перенесення заперечення всередину формули

На цьому етапі обробляються випадки застосування заперечення до формул, що не є атомарними. Якщо такий випадок має місце, то формула переписується за відповідними правилами. Так, наприклад, формула

~(людина(цезар) & існуючий(цезар))

перетвориться в

~людина(цезар) # існуючий(цезар)

а

~all(Х, людина(Х))

перетвориться в

ехists(Х,~людина(Х))

Перетворення, що виконуються на другому етапі, засновані на наступних фактах:

~(α&β) означає те ж саме, що і(~α)#(~β)

~exists(ν, ρ) означає те ж саме, що і all(ν, ~ρ)

~all(ν, ρ) означає те ж саме, що і exists(ν, ~ρ)

Етап 3 — сколемізація

На наступному етапі видаляються квантори існування. Це робиться шляхом введення нових констант — сколемівських констант — замість змінних пов'язаних (введених) квантором існування.

наприклад, формула

exists(X, жінкa(X) & мати(Х, єва))

в результаті сколемізації перетвориться у формулу

жінка(g1) & мати(g1, єва)

де g1 — деяка нова константа, що не використовувалася раніше. Константа g1 представляє деяку жінку, мати якої є Єва.

Якщо формула містить квантори загальності, то процедура сколемізації вже не така проста. Наприклад, якщо у формулі

all(Х, людина(Х) -> ехists(Y, мати(Х, Y)))

Таким чином, при сколемізації попереднього прикладу повинно вийти

all(Х, людина(Х) -> мати(Х,g2(Х)))

В цьому випадку функціональний символ g2 відповідає функції, яка кожній конкретній людині ставить у відповідність його матір.

Етап 4 — винесення кванторів загальності на початок формули

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

all(Х, чоловік(Х) -> all(Y, жінка(Y) -> подобається(X,Y)) )

перетвориться в

all(Х, all(Y, чоловік(Х) -> (жінка(Y) -> подобається(X,Y))))

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

all(Х,живий(Х)#мертвий(Х)&all(Y,подобається(марії,Y)#брудний(Y))

тепер можна представити так:

(живий(Х) # мертвий(X)) & (подобається(марії,Y) # брудний(Y))

Ця формула означає, що, які б X і Y не були б вибрані, або X живий, або X мертвий, і або Марії подобається Y, або Y — брудний.

Етап 5 — використання дистрибутивних законів для & і #

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

(А & В) # C еквівалентна(A # С) & (B # C)

А # (B & С) еквівалентна(А # B) & (A # C)

Так, наприклад, формула:

вихідний(Х) # (працює(кирило, X) &

(сердитий (кирило) # сумовитий(кирило)))

(Для кожного X або X — вихідний день, або Кирило працює в день X і при цьому він або сердитий, або сумовитий) еквівалентна наступній:

вихідний(Х) # (працює(кирило, Х))&

(вихідний(Х) # (сердитий(кирило) # сумовитий(кирило)))

(Для кожного X, по-перше, X є вихідним днем або Кирило працює в день X; по-друге, або X — вихідний день, або Кирило сердитий або сумовитий).

Етап 6 — виділення множини диз’юнктів

Якщо у формулі порядок елементів нічого не міняє, тоді ці елементи можна записати у вигляді сукупності.

Сукупність {А, В, С, D, Е} у точності те ж саме, що і {B, А, C, Е, D}, {Е, D, В, C, А} і так далі. Формули, що є елементами сукупності, отриманої в результаті перетворення деякої формули обчислення предикатів, називаються диз’юнктами. Таким чином, кожна формула обчислення предикатів еквівалентна (в деякому розумінні) сукупності диз’юнктів.

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

((V # W) # X) # (Y # Z)

де змінні є літералами. Тепер ті ж самі міркування, які були зроблені про структуру формули на верхньому рівні, можна застосувати до диз’юнктів. Як і вище, дужки не впливають на значення диз’юнкта. Так само несуттєвий і порядок літералів. Таким чином, можна просто сказати, що диз’юнкт — це сукупність літералів (неявно сполучених диз'юнкцією). У останньому прикладі це буде {V, W, X, Y, Z}.

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

(вихідний(Х) # працює(кирило, Х))&

(вихідний(Х) # (сердитий(кирило) # сумовитий(кирило)))

Ця формула породжує два диз’юнкта. Перший диз’юнкт містить літерали:

вихідний(Х), працює(кирило, Х)

а другий літерали:

вихідний(Х), сердитий(кирило), сумовитий(кирило)

55.Форма запису диз’юнкторів

Очевидно, що для запису формул, представлених в стандартній формі, потрібний відповідний спосіб. Розглянемо його. Передусім, стандартна форма представляє сукупність диз’юнктів. Домовимося записувати диз’юнкти послідовно один за одним, пам'ятаючи при цьому, що порядок запису не має значення. У свою чергу, диз’юнкт є сукупністю літералів, частина з яких містить заперечення, а частина не містять його. Приймемо угоду записувати спочатку літерали без заперечення, а потім літерали із запереченням. Ці дві групи літералів розділятимемо знаком ':-'. Літерали без заперечення при записі будемо відділяти один від одного крапкою з комою (пам'ятаючи, звичайно, при цьому, що порядок запису літералів в кожній групі неважливий), а літерали із запереченням записуватимемо без знаку заперечення (~), розділяючи літерали комами. Запис кожного диз’юнкта закінчуватиметься крапкою. При такій формі запису диз’юнкт, що містить заперечення літералів K, L, ... і літерали А, В,... міг би бути представлений так:

А; B; … :- K, L, … .

Хоча прийняті припущення про форму запису диз’юнктів представляються довільними, в них закладений деякий мнемонічний зміст. Якщо записати диз’юнкт, явно вказавши усі знаки диз'юнкцій і заперечень і відокремивши літерали із запереченнями від літералів без заперечень, то вийде приблизно наступне:

(А # В #...) # (~K # ~L #...)

що еквівалентне

(А # В #...) # ~(K & L &...)

Це у свою чергу еквівалентне

(K & L & ...) -> (А # В #...)

Якщо записати замість ',' замість 'і', ';' замість 'або' і – ':-' замість 'є наслідком', то диз’юнкт природним чином набере наступного вигляду:

А; B; … :- K, L, … .

З врахуванням цих угод формула

(людина(адам) & людина(єва))&

((людина(Х) # ~мати(Х,Y)) # ~людина(Y))

записується так:

людина(адам) :-.

людина(єва) :— .

людина(Х) :— мати(Х, Y), людина(Y).

56.Принцип резолюцій і доказ теорем

Висловлювання, які початково вважаються істинними, називаються аксіомами або гіпотезами, а висловлювання, які випливають з них, називаються теоремами.

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

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

Наприклад, із

сумовитий(кирило); сердитий(кирило) :— робочий_день(сьогодні), іде_дощ(сьогодні).

і

неприємний(кирило) :- сердитий(кирило), втомлений(кирило).

випливає

сумовитий(кирило); неприємний(кирило) :- робочий_день(сьогодні), іде_дощ(сьогодні),втомлений(кирило).

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

Розглянемо один приклад застосування правила резолюцій за наявності змінних:

людина(f1(Х)); король(Х) :—. (1)

король(Y) :— шанує(f1(Y), Y). (2)

шанує(Z,артур) :— людина(Y). (3)

Два перших диз’юнкти представляють стандартну форму формули, яку можна виразити так: «якщо кожна людина шанує когось, то цей хтось — король». Змінні перейменовані для зручності пояснення. Третій диз’юнкт виражає висловлювання про те, що кожна людина шанує Артура. Застосовуючи правило резолюцій до (2) і (3) (співставляючи два відповідні літерали), отримуємо:

король(артур) :— людина(f1(артур)). (4)

(Y в (2) зіставлений з артур в (3), а Z в (3) зіставлений з f1(Y) в (2)). Тепер можна застосувати правило резолюцій (1) і (4), що дає:

король(артур); король(артур) :-.

Це еквівалентно факту, який свідчить, що Артур є королем.

57.Хорнівські диз’юнкти

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

Передусім, очевидно, що існують два види хорнівських диз’юнктів — диз’юнкти, що містять один літерал без заперечення і диз’юнкти, що не містять таких літералів. Називатимемо ці два типи хорнівських диз’юнктів відповідно диз’юнктами із заголовком і диз’юнктами без заголовка. Наступні приклади ілюструють вказані типи диз’юнктів (необхідно пам'ятати, що літерали без заперечення записуються зліва від знаку ':-'):

холостяк(Х) :— чоловік(Х), неодружений(Х).

:— холостяк(Х).

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

• Є тільки один диз’юнкт без заголовка.

• Усі інші диз’юнкти мають заголовки.

58.Пролог і диз’юнктори

У Пролозі безпосередньо можна представити тільки хорнівські диз’юнкти. Твердження програми на Пролозі відповідають хорнівським диз’юнктам із заголовком (у рамках певної процедури доведення теорем). А що в Пролозі відповідає цільовому диз’юнкту? Дуже просто, запитання в Пролозі

?— А1, А2, ..., Аn

у точності відповідає хорнівському диз’юнкту без заголовка

:- А1, А2, …, Аn

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

:— мати(іван, Х), мати(Х, Y).

і твердження

мати(U, V) :— батько(U, V), жінка(V).

отримуємо

:— батько(іван, Х), жінка(Х), мати(Х, Y).

59.Пролог і логічне програмування

Давайте розглянемо Пролог як кандидата на місце мови логічного програмування і подивимося, наскільки добре вона для цього підходить. Передусім, ясно, що деякі програми на Пролозі дійсно представляють опис проблемної області на мові логіки. Запис:

мати(Х, Y) :— батько(Х, Y), жінка(Y).

можна розглядати як опис того, що означає бути матір'ю (це означає бути жінкою і бути одним з батьків). Це твердження виражає висловлювання, яке, як ми припускаємо, має бути істинним, і, крім того, вказує, як показати, що хтось є матір'ю. Аналогічно, твердження:

приєднати([], X, X).

приєднати([А|В], C,[А,D]) :— приєднати(B, C, D).

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

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

З появою Прологу кінцева мета, що полягає в створенні мови логічного програмування, не була досягнута. Проте, Пролог дав практичну систему програмування, що має в деякій мірі властивості, які повинна мати мова логічного програмування, — ясність і декларативність.