Метод резолюции

Пра́вило резолю́ций — правило вывода в исчислении высказываний и исчислении предикатов.

Исчисление высказываний

Пусть C₁ и C₂ - два предложения в исчислении высказываний, и пусть $C_1 = P \or C'_1$, а $C_2 = \lnot P \or C'_2$, где P - пропозициональная переменная, а C'₁ и C'₂ - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

Правило вывода

$\frac{C_1, C_2}{C'_1 \or C'_2} R$

называется правилом резолюции.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение $C'_1 \or C'_2$ - резольвентой, а формулы P и $\lnot P$ - контрарными литералами.

Исчисление предикатов

Пусть C₁ и C₂ - два предложения в исчислении предикатов.

Правило вывода

$\frac{C_1, C_2}{(C'_1 \or C'_2)\sigma} R$

называется правилом резолюции в исчислении предикатов, если в предложениях C₁ и C₂ существуют унифицированные контрарные литералы P₁ и P₂, то есть $C_1 = P_1 \or C'_1$, а $C_2 = \lnot P_2 \or C'_2$, причём атомарные формулы P₁ и P₂ являются унифицируемыми наиболее общим унификатором σ.

В этом случае резольвентой предложений C₁ и C₂ является предложение $(C'_1 \or C'_2)\sigma$, полученное из предложения $C'_1 \or C'_2$ применением унификатора σ.