Для применения правила резолюции нужны контрарные литералы в родительских дизъюнктах.
— правило резолюции в исчислении высказываний, если в предложениях С1 и С2 есть унифицируемые контрарные литералы Р1 и Р2, т. е. , , причем атомарные формулы Р1 и Р2 унифицируются общим унификатором s.
Пример.
Пусть имеются родительские дизъюнкты:
Д1:
Д2:
Здесь и — контрарные литералы. Их можно унифицировать, если в Д1 заменить x на f(z): {f(z)//x}, а в Д2 заменить y на a: {a//y}.
Получаем:
Д1:
Д2:
Резольвента: