4.3.Правило резолюции для исчисления высказываний

Пусть С₁ и С₂ – предложения в исчислении высказываний.

Пусть , , где Р – пропозициональная переменная, - любые предложения.

Правило вывода называется правилом резолюции, где

С₁, С₂ - родительские предложения,

- резольвента,

- контрарные литералы.

Правило резолюции очень мощное правило вывода и многие ранее рассмотренные правила являются частным случаем правила резолюции.

Примеры.

1. Правило вывода modus ponens:

2. Правило транзитивности

Унификация

Если в формулу А вместо переменных подставить формулы , то получится формула В, которая является частным случаем формулы А.

.

Набор подстановок называется унификатором.

Таким образом, унификация состоит в том, что мы пытаемся сделать одинаковыми различные предикаты.