27. Канонизация выражений в исчислениях предикатов.

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

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

30 Конъюктивная нормальная форма

31 Клаузальная нормальная форма

33 Метод резолюции в исчислении предикатов.

Суть метода резолюции состоит:

1. В проверке того, содержит или не содержит S пустое предложение;

2. В проверке того, выводится или не выводится пустое предложение из S, если оно в S отсутствует.

Введём новые определения:

1. Предикат и его отрицания вместе называются литералом или литерой;

2. Дизъюнкция литер, входящих в предложение называются дизъюнктом;

3. Дизъюнктом Хорна являются дизъюнкты, имеющие не более одного положительного литера;

4. Дизъюнкт, не содержащий никаких литер, называется пустым. Обычно его обозначают знаком . Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то он всегда ложен;

5. Контрарной парой литер называется пара, состоящая из P и P .

6. Резольвентой дизъюнктов называется новый дизъюнкт, образованный из оставшихся частей после вычёркивания контрарных пар литер.

Основная идея принципа резолюции заключается в проверке, содержит ли множество дизъюнктов S пустой дизъюнкт. Если S содержит пустой дизъюнкт, то формула является ложью, следовательно, “В” выводится из групп предикатов. Если же S не содержит , то следующие шаги процедуры заключаются в выводы новых дизъюнктов, пока не будет получен пустой дизъюнкт.

34. Унификация выражений в методе резолюций