<<
>>

3.5. Приведенная форма представления предикатов

Формула, в которой из логических символов встречаются только ⌐, &, U , причем отрицание должно стоять перед символами предикатов, называется приведенной формой.

Приведенная форма называется нормальной (ПНФ), если она не содержит символов кванторов или все символы кванторов стоят в начале формулы за скобками (кванторная приставка).

Алгоритм построения ПНФ

1. Исключить связки →, ~ с помощью законов преобразования логики предикатов.

2. Перенести знак ⌐ внутрь формулы.

3. Если нужно переименовать связанные переменные.

4. Используя законы преобразования логики предикатов перейти к КНФ.

Пример.

Исключаем импликацию
Переносим знак ⌐ внутрь формулы
Переименовываем связанные переменные.

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

. Чтобы выполнить сколемизацию надо:

1) Отбросить кванторы существования для чего

· если левее нет кванторов общности, то соответствующая переменная заменяется на константу Сколема (ас);

· иначе переменная заменяется функцией Сколема (fc) от переменных, на которые навешаны кванторы общности, стоящие левее данного квантора существования.

2) Отбросить кванторы общности.

Пример :

<< | >>
Источник: Викентьева О. Л.. Математическая логика и теория алгоритмов. Конспект лекций для студентов специальностей АСУ, ЭВТ, КЗИ. Пермь, 2007г.. 2007

Еще по теме 3.5. Приведенная форма представления предикатов: