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

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

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

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

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

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

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

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

Пример.

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

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

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

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

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

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

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

Пример :