Пусть С1 и С2 – предложения в исчислении высказываний.
Пусть , , где Р – пропозициональная переменная, — любые предложения.
Правило вывода называется правилом резолюции, где
С1, С2 — родительские предложения,
— резольвента,
— контрарные литералы.
Правило резолюции очень мощное правило вывода и многие ранее рассмотренные правила являются частным случаем правила резолюции.
Примеры.
1. Правило вывода modus ponens:
2. Правило транзитивности
Унификация
Если в формулу А вместо переменных подставить формулы , то получится формула В, которая является частным случаем формулы А.
.
Набор подстановок называется унификатором.
Таким образом, унификация состоит в том, что мы пытаемся сделать одинаковыми различные предикаты.