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