Page 40 - 6109

мул, який використовують тільки з'єднувачі типу , , ~.
Негативна або позитивна атомарна формула називається літералом
Літерал називається позитивним, якщо він не стоїть під знаком запе-
речення.
Літерал називається негативним, якщо він стоїть під знаком заперечення.
Диз'юнктом (або фразою теорії) називається диз'юнкція деякої кількості
атомарних формул.
Кожна формула – множина літералів, які з'єднані символом . Негативні
і позитивні літерали відповідно групуються. Схематично фраза має такий
вигляд:
Р,  P 2  ... Р п  N t  N 2  ... N m,
де Р 1, ...,Р n – позитивні літерали, a N 1, ..., N m – негативні. З іншого боку,
фразу можна розглядати як узагальнення поняття імплікації. Дійсно, якщо А і В

атомарні формули, тоді формулу А  В можна переписати і в такому
еквівалентному вигляді: ~ A  В. Звідси отримаємо фразову формулу В  ~ А.
Фраза має таку семантику. Всі позитивні атомарні формули виступають у
ролі альтернативних висновків, а негативні є необхідними умовами. Наприклад,
A  B  ~C  ~D зазначає, що А і В будуть істинними тоді і тільки тоді, коли є
істинними С і D. Елементарна фраза має тільки один літерал.
У теорії і практиці автоматичного доведення теорем найвживанішими є
фрази спеціального типу, які називаються фразами Хорна (або хорківськими
диз'юнктами)
Фразою Хорна називається диз'юнкція довільної кількості атомарних
формул, з яких позитивною є не більше ніж: одна (тобто у фразі Хорна лише
одна атомарна формула може не стояти під знаком заперечення). Фрази
Хорна по суті є імплікаціями. Справді, розглянемо фразу ~ A  ~ В  ~ С  D
(кожний з літералів А, В, С, D може залежати від довільної кількості констант і
змінних, тут це несуттєво). Усі літерали, крім D, є негативними, отже, дана
фраза являє собою фразу Хорна. Але відповідно до правил де Моргана вона
еквівалентна фразі ~ (ABC)  D. А це, в свою чергу, є іншою формою запису
імплікації (твердження D випливає з кон'юнкції тверджень А, В, С).
Розглянемо ще один приклад. Нехай маємо формулу
(особа (петро)  особа (Іван))  ((особа (X)  мати (X, Y))  ~особа (Y)),
яка після відповідних дій перетворюється на:
особа (петро):-.
особа (Іван):-.
особа (Х) :- мати (X, Y), особа (Y).
Останній запис уже нагадує текст прологівської програми.

4.4 Метод резолюцій

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

40