Логическое и функциональное программирование (стр. 13 из 16)

Дедушка(x, y) : x – дедушка y.

Используя эти предикаты можно записать следующие утверждения:

(1) ("x1)("y1)("z1)((отец(x1, y1) Ùотец(y1, z1)) ® дедушка(x1, z1)):

если x1 отец y1, а y1 отец z1, то x1 дедушка z1.

(2) ("x2, y2, z2, w2)((отец(x2, y2) Ù брат(x2, z2) Ù отец(z2, w2)) ® кузен(y2, w2)) .

(3) ("x3, y3, z3)((отец(x3, y3) Ù отец(x3, z3) Ù

) ® брат(y3, z3)).

Предположим также, что помимо этих логических формул заданы следующие факты:

(4) Отец(Александр, Сергей),

(5) Отец(Сергей, Ричард).

(6) Отец(Сергей, Иван).

Сначала неаксиоматически зададим процедуру, которая из логических формул выводит заключение. Вывод формулы C из логических формул A, Bбудем задавать в виде схемы:

А: Все люди смертны

В: Сократ – человек

С: Сократ – смертен.

Если в переменную подставляется значение, то слева от наклонной черты запишем имя переменной, а справа – значение. Например, если в переменную xподставляется значение Сократ, то будем это записывать как x/Сократ.

Предположим, теперь, что требуется доказать – истинна или ложна логическая формула. В ее истинности или ложности можно убедиться логической процедурой, применив ранее заданные логические формулы. Эта процедура выглядит аналогично процедуре доказательства теорем, когда выдвигается некоторая теорема, а справедливость ее устанавливается из известных аксиом.

Например, предположим, что задан вопрос: «Кто дедушка Ричарда?». Его можно записать в виде:

($x)(дедушка(x, Ричарда)).

Ответ может быть получен в следующей последовательности:

Поскольку заключение получается из комбинации уже существующих правил, ответ является результатом процедуры восходящего вывода.

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

В логике предикатов такая процедура полностью формализована и носит название метода резолюции.

Для применения этого метода исходную группу логических формул преобразуют в нормальную форму. Преобразование проводится в несколько стадий.

4.2.2 Процесс нормализации

4.2.2.1Префиксная нормальная форма

Рассмотрим фразу «любой человек имеет отца». Ее можно представить в логике предикатов в следующем виде:

("x)(человек(x) ® ($y)(отец(y, x))).

$ находится внутри ППФ. Это не всегда удобно, поэтому целесообразно вынести все кванторы за скобки, чтобы они стояли перед ППФ. Такая форма носит название префиксной нормальной формы.

Преобразование к префиксной нормальной форме произвольной ППФ можно легко выполнить машинным способом, используя для этого несколько простых правил.

Во-первых, необходимо исключить связки ® и ». По определению:

Следовательно, во всех комбинациях ППФ можно ограничиться тремя связками Ú, Ù и ` .

Предикат, не содержащий переменных, аналогичен высказыванию, поэтому такие предикаты будем обозначать F, G. Когда некоторое выражение выполняется для любого квантора " и $ будем записывать такой квантор Q.

Легко показать:

1.

Это соответствует: высказывание не имеет отношения к квантору переменной, которая включена в другой предикат.

Между предикатами существует следующее соотношение:

Таким образом, «необязательно F(x) выполняется для всех x» º «существует такое x, что F(x) не выполняется»; «не существует такое x, что выполняется F(x)» º «для всех xне выполняется F(x)».

Далее имеем:

2.("x)F(x)Ù("x)H(x) = ("x)(F(x)ÙH(x))

($x)F(x)Ú($x)H(x) = ($x)(F(x)ÚH(x)).

Это означает, что квантор " обладает дистрибутивностью относительно Ù, а $ - относительно Ú.

С другой стороны:

("x)F(x)Ú("x)H(x)¹("x)(F(x)ÚH(x)).

($x)F(x)Ù($x)H(x)¹($x)(F(x)ÙH(x)).

Это легко показать. Пусть для первого выражения xопределен на множестве D ={а, б, в}, при этом истиной являются F(а), F(б), H(в). Тогда левая часть не выполняется, а правая истинна. На самом деле справедливо:

("x)F(x)Ú("x)H(x)®("x)(F(x)ÚH(x)).

($x)F(x)Ù($x)H(x)®($x)(F(x)ÙH(x)).

Смысл этих формул в том, что описание для двух разделенных предикатов не совпадает с описанием, использующим эти предикаты одновременно как одно целое и с одинаковыми переменными. Поэтому, изменив все переменные в их правых частях, получим:

("x)F(x)Ú("x)H(x) = ("x)F(x) Ú ("y)H(y),

($x)F(x) Ù($x)H(x) = ($x)F(x) Ù ($y)H(y).

Теперь H(y) не содержит переменной xи поэтому не зависит от связывания x. Отсюда:

3. ("x)F(x)Ú("x)H(x) = ("x)("y)(F(x) Ú H(y)),

($x)F(x) Ù($x)H(x) = ($x)($y)(F(x) Ù H(y)).

Таким образом, процесс получения префиксной нормальной формы можно представить как последовательность шагов:

1. Используя формулы для ®, », заменим их на Ù, Ú, ¾.

2. Воспользовавшись выражениями

внесем отрицания внутрь предикатов.

3. Вводятся новые переменные, где это необходимо.

4. Используя 1, 2, 3 получаем префиксную нормальную форму.

В качестве примера рассмотрим следующее выражение:

Шаг1:

Шаг2:

Шаг 3: нет необходимости.

Шаг 4: используем выражение 1 по переменной z –

Теперь применяем выражение 1 по переменной w –

4.2.2.2Скалемовская нормальная форма

Дальнейшее преобразование предполагает полное исключение из формулы кванторов. При этом необходимо сохранить семантику. Это достигается за счет введения скалемовских функций. Для описания этой функции рассмотрим следующий пример: ("x)($y)подсистема(x,y), для каждого x существует y такой, что xего подсистема.

Это означает, что если выделить конкретное x, то для этого x существует y, удовлетворяющее функции подсистема(x, y). Иными словами, yзависит от x, то есть, если задано x, то и существует соответствующее ему y. Отсюда следует, что yможно заменить на функцию f(x), которая задает отношение между xи y. Поскольку f(x) возникло из-за того, что переменная y квантифицирована $, при подстановке функции на место y, квантор $ уже не требуется. Таким образом, исходную логическую формулу можно переписать: ("x) подсистема(x, f(x).

Такая функция называется скалемовской.

Приоритетность действия кванторов, имеющихся в префиксной форме, определяется слева направо. Например: ("x)($y)("z)F(x, y, z) Þ ("x)("z)F(x, f(x), z). А для случая: ("x)("z)($y)F(x, y, z) Þ ("x)("z)F(x, f(x, y), z).

Таким образом, переменной, которая в логической формуле влияет на связанную квантором существования переменную, является любая переменная с квантором общности, которая стоит левее переменной из квантора существования. Если переменная связанная квантором существования является крайней слева, такую формулу можно заменить функцией без аргументов (константой):

($x)("y)подсистема(x, y) =подсистема.

Если проделать эту операцию для примера, получим:

В случае, когда в одной логической формуле имеется более двух связанных квантором существования переменных, то сколемовская функция также будет распадаться на различные функции.