<<

стр. 2
(всего 2)

СОДЕРЖАНИЕ

дем сканировать записанные выражения вертикальными линиями. Пропустив
k столбцов, состоящих из одинаковых символов, внесем в множество D все термы,
попадающие в k + 1-ый столбец. В нашем случае D (E) = {x, g (y)};

3. Построим унификатор ?1 для множества D (?1 = g (y)/x ) и применим его к вы-
ражениям: E1 ?1 = A (g (y) , f (u)) , E2 ?1 = A (g (y) , f (h (z))); в дальнейшем будем
работать уже с этими выражениями.
4. Если множество E еще не унифицировано, перейдем к шагу 1, работая уже с
множеством E = {E1 ?1 , E2 ?1 }

Очевидно, что, в соответствии с алгоритмом, рано или поздно множество E будет
унифицировано (в нашем случае на втором шаге, ?2 = h (z)/u ), причем полученный
унификатор ? = ?1 ? ?2 ? . . . ? ?n будет самым общим. В случае, если множество неуни-
фицируемо (например, разные выражения содержат различные константы), алгоритм
будет выполняться бесконечно, однако такая ситуация невозможна по условию теоремы
(множество выражений унифицируемо).
Трудоемкость данного алгоритма является не почти линейной, как может показать-
ся вначале, а экспоненциальной вследствие действия под названием occur check , то
есть “проверка вхождения”: ? (x ? Var, t ? Ter) : x ? t. Она предотвращает зациклива-
/
ние алгоритма, гарантируя, что disagreement set содержит только те термы, которым
не принадлежит некоторая входящая в него переменная, то есть, позволяет избежать
циклических замен вида [f (x)/x] для множества D = {x, f (x)}.

6.1 Формальная Система Опровержения
Нормальная форма Скулема. Любая формула языка логики первого порядка может
быть приведена к нормальной форме Скулема (Skolem) к виду

?x1 ?x2 ?x3 . . . ?xn (C1 ? C2 ? C3 ? . . . ? Cn )
36 Язык Пролог


где Ci фразы, конечные дизъюнкции литералов. Все кванторы всеобщности (?) выно-
сятся вперед, кванторы существования (?) недопустимы. В скобках находится выраже-
ние в конъюнктной нормальной форме (КНФ) конъюнкции элементарных дизъюнк-
ций.

Замечание 6.2 Литерал атомная формула или ее отрицание.

Процесс приведения выражения к нормальной форме Скулема состоит из следую-
щих этапов: сначала с помощью семантических эквивалентностей осуществляется пе-
реход к КНФ, после чего все кванторы выносятся за скобки и исключаются кванторы
существования.
Проиллюстрируем исключение квантора существования на примерах. Для исклю-
чения ’?x’ из ?x?y (A (x, y)) внесем в сигнатуру языка новую константу c и запишем:
?y (A (c, y)). В случае другого расположения кванторов, например, ?y?x (A (x, y)), необ-
ходимо ввести в сигнатуру уже новую унарную функцию f : ?y (A (f (y) , y)); приведение
?y?z?x (A (x, y, z)) требует введения бинарной функции: ?y?z (A (g (y, z) , y, z)).
В дальнейшем мы будем работать только с формулами в нормальной форме Ску-
лема. Это не сужает круг рассматриваемых формул, так как любая формула языка
логики первого порядка может быть записана в таком виде. Будем писать для крат-
кости: P = {C1 , C2 , C3 , . . . , Cn } вместо P = ?x1 ?x2 ?x3 . . . ?xn (C1 ? C2 ? C3 ? . . . ? Cn ).
Информация о наличии кванторов всеобщности не теряется, так как здесь мы имеем
дело только с замкнутыми формулами и для переменных всеобщность следует автома-
тически.
Введем правила вывода. Пусть C1 , C2 , Q некоторые фразы. Будем говорить, что
C1 и C2 выводят Q в формальной системе опровержения R и записывать C1 , C2 |=R Q,
если:

• Существуют такие подстановки ?1 , ?2 , что C1 ?1 и C2 ?2 не имеют общих имен
переменных;

• Существуют такие множества литералов {L1 , L2 , L3 , . . . , Ln } ? C1 ?1 и {L1 , L2 , L3 , . . . , Ln } ?
C2 ?2 , где литералы второго множества являются отрицаниями литералов первого,
что объединенное множество со снятыми отрицаниями {L1 , L2 , L3 , . . . , Ln , L1 , L2 , L3 , . . . , Ln }
унифицируемо, его самый общий унификатор ?;

• Формула Q имеет вид:

((C1 ?1 \ {L1 , L2 , L3 , . . . , Ln }) ? (C2 ?2 \ {L1 , L2 , L3 , . . . , Ln })) ?

Пример 6.4 C1 = {A (z) ? ¬B (y) ? A (g (x))}, C2 = {¬A (x) ? ¬C (x)}. Переименуем
переменные в соответствии с правилом 1: ?1 = ? (пустая замена), ?2 = {u/x}. Да-
лее, рассматривая множества литералов, получим ? = g (x)/z , x/u . Здесь наличие
6.1 Формальная Система Опровержения 37


множеств {Li } и Lj позволяет избавиться от не унифицируемых литералов, вхо-
дящих в одну формулу в положительном, а в другую в отрицательном виде. Замена
переменных позволяет избежать неунифицируемых множеств вида {x, f (x)}. Напри-
мер, {¬x, f (x)} |=R ?, так как в процессе редукции (удаления литералов, ведущих к
лжи) остается пустое множество, которое семантически эквивалентно лжи.

Теорема 6.2 Пусть множество фраз S невыполнимо, тогда S выводит пустую фра-
зу в этой формальной системе опровержения (S |=R ).

Эту теорему можно назвать теоремой о “полноте наоборот”: тогда как полнота в
обычном понимании означает, что, если некое выражение семантически истинно, то
оно истинно и синтаксически, эта теорема утверждает о том, что семантическая ложь
выводит пустой литерал.
Рассмотрим алгоритм проверки выполнимости множества фраз:

REPEAT {S := Res (S)} UNTIL { ? S} : PRINT ’S невыполнимо’

Здесь Res (S) множество резольвентов, то есть всех возможных выводов из пар фраз,
принадлежащих S. Если множество выполнимо, данный алгоритм будет работать бес-
конечно.

Пример 6.5 Запишем формулировку Парадокса Брадобрея:

?x?y (B (x) ? ¬S (y, y) > S (x, y)) ? ?x?y (B (x) ? S (y, y) > ¬S (x, y))

Мы хотим доказать, что ¬?xB (x), или, что то же самое, что ?B (x) |= ?, то
есть, существование семантического противоречия.
Представим данную формулу (а также цель) в виде множества фраз в нормаль-
ной форме Скулема: {¬B (x) , S (y, y) , ¬S (x, y)}, {¬B (x) , ¬S (y, y) , ¬S (x, y)}, {B (c)}.
Выведем из двух первых фраз новую: {¬B (x)}, и получим новую систему: {¬B (x)},
{B (c)}, из которой выводится пустое множество .

Алгоритм представляет каждую формулу в виде набора фраз и, совмещая каждую
с каждой, пытается сократить результат с учетом унификации до получения пустой
фразы на выходе.
Можно оптимизировать алгоритм путем ввода правил, ограничивающих полный пе-
ребор. Таким образом, получаем два класса стратегий, которых придерживаются алго-
ритмы: полные стратегии, которые для противоречивого набора входных фраз всегда
рано или поздно получают на выходе ложь, и неполные, позволяющие оптимально об-
рабатывать некоторый класс задач, но допускающие невозможность найти ответ для
других (грубо говоря, алгоритм зацикливается при некоторых корректных входных
данных).
38 Язык Пролог


Рассмотрим структуру PROLOG-программы. Автоматический доказатель язы-
ка PROLOG основан на схожих принципах и использует неполную стратегию, ко-
торая заключается в следующем: рассматриваются первые две фразы; затем к вы-
водам из них добавляется третья и рассматриваются выводы уже из этого набора
и так далее. Неполноту этой стратегии можно продемонстрировать на примере: из
(A ? B) ? (A ? ¬B) ? (¬A ? B) ? (¬A ? ¬B) никогда не будет получена ложь. Одна-
ко, при некоторых ограничениях на входные фразы данная стратегия является полной,
а именно, если программа состоит только из фраз Хорна (Hoarn).

Определение 6.8 Фразы Хорна – это фразы, содержащие не более одной положи-
тельной атомной формулы.

Например, A ? ¬B, ¬A ? B и ¬A ? ¬B – фразы Хорна, а A ? B нет; фразы Хорна
также записываются следующим образом: A0 ? ¬A1 ? ¬A2 ? ¬A3 = A0 < A1 , A2 , A3 ,
на языке PROLOG A0 : ? ? A1, A2, A3.; фраза Хорна, не содержащая положительных
литералов, называется целью: < A1 , A2 , A3 = : ? ? A1 , A2 , A3 ..
Таким образом, PROLOG-программа состоит из набора фраз Хорна и цели.

Пример 6.6 Dog(Rex).
Cat(Felix).
Animal(X) :- Cat(X).
Animal(X) :- Dog(X).
:- Animal(Rex).
Программа говорит о том, что Rex это Dog, Felix это Cat, любой Cat это
Animal и любой Dog также Animal; доказать: Rex Animal. Автоматический дока-
затель выдаст ответ ’Yes’. Можно также задать цель :– Animal(X), и ответ будет
’Rex’ и ’Felix’.

Скажем в заключение, что автор не претендует на полноту изложения в данной
книге тем в ней затронутых. Что касается языков логического программирования, то
читатель заинтерсовавшийся, может продолжить свое знакомство с ними.

<<

стр. 2
(всего 2)

СОДЕРЖАНИЕ