Реферат: Инженерия знаний
Для использования этого метода необходимо исходную формулу привести к ДНФ.
ДНФ: 
- дизъюнкция литер
рii – атом или отрицание атома.
Потом ДНФ представляют в виде множества дизъюнктов
В методе резолюций – имеется одно правило вывода
В результате из 2-х дизъюнктов получаем новую, называется руовентой
- получаем пустой дизъюнкт , который всегда ложный.
Если множество содержит пустой дизъюнкт , то оно является не выполнимым.
Получается пустой дизъюнкт, который доказывает что данное множество является невыполнимым.
Метод резолюций применяется до тех пор пока не получится пустой– дизъюнкт
m,n – const
подстановка вместо переменной константы –унификация.
В данном случае выполняем подстановку {n/y}:
Из (1)и (2) => a(x)
c(x,n) (5)
Из (3) и (5) , выполняя ь подстановку {m/n}=> c(m,n) (6)
Из (4) и (6) без подстановок => 0
Принцип резолюций в Прологе
В Прологе используются хордовские дизъюнкты, т.е. дизъюнкты, содержащие одну литеру без отрицания.
На пример 
=> 
конъюнкция
без
отрицания
Могут использоваться дизъюнкты , которые вообще не содержат литер. –