4.4. Правило резолюции для исчисления предикатов

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

- правило резолюции в исчислении высказываний, если в предложениях С₁ и С₂ есть унифицируемые контрарные литералы Р₁ и Р₂, т.

Пример.

Пусть имеются родительские дизъюнкты:

Д1:

Д2:

Здесь и - контрарные литералы. Их можно унифицировать, если в Д1 заменить x на f(z): {f(z)//x}, а в Д2 заменить y на a: {a//y}.

Получаем:

Д1:

Д2:

Резольвента: