Формула, в которой из логических символов встречаются только ⌐, &, Ú , причем отрицание должно стоять перед символами предикатов, называется приведенной формой.
Приведенная форма называется нормальной (ПНФ), если она не содержит символов кванторов или все символы кванторов стоят в начале формулы за скобками (кванторная приставка).
Алгоритм построения ПНФ
1. Исключить связки →, ~ с помощью законов преобразования логики предикатов.
2. Перенести знак ⌐ внутрь формулы.
3. Если нужно переименовать связанные переменные.
4. Используя законы преобразования логики предикатов перейти к КНФ.
Пример.
|
Исключаем импликацию |
|
|
Переносим знак ⌐ внутрь формулы |
|
|
Переименовываем связанные переменные. |
Чтобы избавиться от кванторов применяют процедуру сколемизации (от фамилии математика Skolem). Сколемизация позволяет получить запись предикатов, не содержащих свободных переменных в форме без кванторов.
. Чтобы выполнить сколемизацию надо:
1) Отбросить кванторы существования для чего
- если левее нет кванторов общности, то соответствующая переменная заменяется на константу Сколема (ас);
- иначе переменная заменяется функцией Сколема (fc) от переменных, на которые навешаны кванторы общности, стоящие левее данного квантора существования.
2) Отбросить кванторы общности.
Пример :