ОСНОВИ ДИСКРЕТНОГО АНАЛІЗУ.
Автори: Н.Д.Федоренко,В.В.Демченко

     3.21. ПОБУДОВА ДОВЕДЕНЬ У ЛОГІЦІ ПРЕДИКАТІВ

Основною задачею логіки предикатів є встановлення істинності предикатних формул. Позначимо черездеякий предикат з довільним числом аргументів, а черезвідповідну кванторову групу. Тоді закон дистрибутивності, наприклад, матиме вигляд:

.

      Для одномісних предикатів його можна довести через процедуру конкретизації:

;;;;;
;;.

.

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

      Основні правила доведення алгебри предикатів.

1. Правило універсальної конкретизації.

, якщовільне дляв.

2. Правило екзинстенціональної конкретизації.

.

3. Правило екзинстенціонального узагальнення.

, девільне дляв.

4. Правило всезагальності.

.

5. Правило існування.

.

6. Правило узагальнення.

Якщо то, то, якщоне входить в жодну формулу з.

      Розглянемо приклади.

      Приклад 15. Нехай дана предикатна клауза:

.

Позначимо

;
;
.

Тоді.

Якщо транзитивність справджується, то і предикатна клауза також.

      Приклад 16. Довести істинність клаузи:

.

      Процедура ідентифікації приводить до

; ;

;

; ;

,

;

;

.

Звідки слідує істинність вихідної клаузи.

      Приклад 17. Довільна семантика логіки висловлювань може бути виражена в предикатній формі. Дана проста легенда: Якщо Ваня ходить всюди за Ніною, а Ніна знаходиться в кіно, то де буде знаходитися Ваня?

      =`"знаходиться там, де".

      Складемо клаузу:

.

Тобто, треба довести наступне речення: чи існує таке місце, де знаходився б Ваня.

      Перетворимо нашу клаузу у протиріччя:

.

Квантори всезагальності опускаємо, бо відсутні квантори існування. Доведення оформимо у вигляді дерева (рис.9)



Рис.9

      При конкретизації , доводиться, що дійсно існує місце, в якому знаходиться Ваня.

      Зауважимо, що метод резолюції можна модифікувати так, щоб доведення дало відповідь у предикатній формі: "Ваня знаходиться в кіно". Це можливо тоді, коли до того, що треба довести дописати диз'юнкцію з протилежним твердженням, утворивши таким чином тавтологію:

.

      Тоді дерево логічного висновку буде наступним (рис. 10).



Рис.10

      Більшість задач з використанням предикатів носить пошуковий характер. Пошукові задачі реалізуються мовою логічного програмування - ПРОЛОГ. Зупинимося на основних управляючих структурах та функціональних елементах цієї мови. Оскільки логіка висловлювань працює з правильно побудованими реченнями, існує можливість змішування об'єктивних та суб'єктивних речень, а також висловлювань, взятих з різних ієрархічних рівнів предметної області. Щоб обійти таку помилку, задачу, яку доводять, оформляють в виді структури деревовидної форми.

      За корінь дерева приймається деяка ціль, істинність якої треба довести.

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

.

      Кожне - підціль основної ціліі залежить в свою чергу, від інших правил.

; .

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

      В мові ПРОЛОГ реалізована процедура уніфікації, з допомогою якої проводиться порівняння цілі з правилами, а правила cпівставляться з фактами. В результаті уніфікації змінним присвоюються конкретні значення так, що предикат цілі стає істинним фактом в випадку сприятливого виходу. Для розуміння утворення уніфікації розглянемо конкретний приклад програми.

      Приклад 18. Нехай задана легенда.

      Василя цікавлять книги, комп'ютери та автомобілі. Михайла цікавить дещо, що цікавить Василя, але це є технікою і це вироблено в Японії. Відомо, що комп'ютери та автомобілі - це техніка. Крім того відомо, що комп'ютери випускають в Америці, а автомобілі - Америці і Японії.

      Запитання: "що цікавить Михайла?".

      Щоб краще скористуватися програмою, всі предикати та конкретні значення змінних не кодуються окремими буквами, а приводяться на словах. Зліва від тексту програми приведемо символьні вирази, щоб в аналітичній формі продемонструвати метод резолюцій, який лежить в основі інтерпретації ПРОЛОГу. При цьому всі склеювання проводяться з квантором всезагальності, але сам квантор не вказується.

      Програма.

1. Інтерес(Василь,комп'ютери) .

2. Інтерес(Василь,книги) .

3. Інтерес(Василь,автомобілі) .

4. Інтерес(Михайло,).

5.(інтерес(Василь,) .

6. Техніка(), .

7. Виготовлено(,Японія) .

8. Техніка(комп'ютери) .

9. Техніка(автомобілі) .

10. Виготовлено(комп'ютери,Америка) .

11. Виготовлено(автомобілі,Америка) .

12. Виготовлено(автомобілі,Японія) .

Ціль: 13. Інтерес(Михайло,)

      Програма дає можливість скласти протиріччя, яке розв'язується в рамках методу резолюції:

.

      Нуль можна отримати, коли. Тоді,нейтралізується предикатами 3,9,13.

      Пошук значенняпроходить через процедуру уніфікації, яку можна виділити шляхом трасування програми (покрокового протоколювання процесу виконання програми).

      Позначимо:B - виклик нового предикату, П - повторний виклик предикату, У - успішне завершення процедури уніфікації, тобто викликаний предикат відповідає якому-небудь факту, Н - неуспішне завершення уніфікації, У - вказує на те, що існує ще один факт з уніфікацією, яка підходить. Символ підкреслення на місці х називається анонімною змінною і повністю замінює х при трасуванні програми. Рядок трасування закінчується числом, яке відповідає номеру роздруківки програми.

      Приведемо трасування програми.

1. В: ціль ( ) - 13.

2. В: інтерес (Михайло, -) - 1.

3. П: інтерес (Михайло, -) - 2.

4. П: інтерес (Михайло, -) - 3.

5. У: інтерес (Михайло, -) - 4.

6. В: інтерес (Василь -) - 5.

7. У: інтерес (Василь, комп'ютери ) - 1y.

8. В: техніка (комп'ютери) - 6.

9. У: техніка (комп'ютери) - 8.

10. В: виготовлено (комп'ютери, Японія) - 7.

11. П: виготовлено (комп'ютери, Японія) - 10.

12. П: виготовлено (комп'ютери, Японія) - 11.

13. Н: виготовлено (комп'ютери, Японія) - 12.

14. П: інтерес (Василь, -) - 5.

15. У: інтерес (Василь, книги) - 2у.

16. В: техніка (книги) - 6.

17. П: техніка (книги) - 8.

18. Н: техніка (книги) - 9.

19. П: інтерес (Василь, -) - 5.

20. У: інтерес (Василь, автомобілі) - 3.

21. В: техніка (автомобілі) - 6.

22. П: техніка (автомобілі) - 8.

23. У: техніка (автомобілі) - 9.

24. В: виготовлено (автомобілі, Японія) - 7.

25. П: виготовлено (автомобілі, Японія) - 10.

26. П: виготовлено (автомобілі, Японія) - 11.

27. У: виготовлено (автомобілі, Японія) - 12.

28. У: Ціль ( ) - 13.

      Для відповіді на запитання "Що цікавить Михайла?", або в предикатній формі - інтерес Михайла, ПРОЛОГ - система шукає факти і заголовки правил, які зіставляються з ціллю. Перші три факти не відповідають цілі, далі слідує правило, заголовок якого замінюється трьома підцілями. В рядку 6 викликається підціль, потім ПРОЛОГ - система повертається на початок програми, де її чекає "успіх". Виставляється показник "у", до якого система повернеться у випадку "неуспіху", який може з'явитися в іншому місці програми. В рядку 8 викликається виклик другої підцілі - техніка (комп'ютери), для яких знаходиться факт (рядок 9). Проте для третьої підцілі (комп'ютери, Японія) - потрібного факту не має (рядок 13). Тоді змінна х звільнюється від своєї конкретизації (комп'ютери) і приймає нове значення "книги". Ця конкретизація не задовольняє другу підціль (рядок 18). Змінна знову звільнюється і приймає значення "автомобілі". При цій конкретизації задовольняються всі три підцілі, тобто пошук закінчується успіхом, інтерес (Михайло, автомобілі) є тим конкретизованим предикатом, при якому забезпечена істинність клаузи.

      Граф пошуку цілі "інтерес (Михайло,) зображений на рис.11.



Рис.11.

      Бінарне дерево отримано в результаті підстановок предметних констант на місце змінних, правила замінювалися фактами, а ціль - підцілями.