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

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

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

Пример.

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

Д1:

Д2:

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

Получаем:

Д1:

Д2:

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

Дата добавления: 2014-01-15