Метод резолюций
Содержание:
Бинарная резольвента
Пусть имеется 2 дизъюнкта
$P_1^n t_1 … t_n \lor F, \neg P_1^n s_1…s_n \lor G$
$s_1, …s_n$ - какие-то термы
$\sigma$ - унификатор $p_1^nt_1… t_n$ и $p_1^ns_1..s_n$
Бинарной резольвентой называется дизъюнкт $F^{\sigma} \lor G^{\sigma}$.
Пример.
- $\neg P_1^2 f_1^0 f_1^1 x_1 \lor P_1^1x_1$
- $P_1^2 x_2 x_3 \lor \neg P_2^1 x_3$
$\sigma = {x_2 f_1^0, x_3 f_1^1 x_1}$ $\neg P_1^2 f_1^0 f_1^1 x_1 \lor P_1^1 x_1$
$P_1^2 f_1^0 f_1^1 x_1 \lor \neg P_2^1 f_1^1 x_1$
Операция склейки
Это такая подстановка, уменьшающая количество слагаемых вследствие их совпадения.
Пример. $\neg P_1^2 x_1 x_2 \lor \neg P_1^2 x_2 x_1 \lor \neg P_1^2 f_1^0 f_1^0 \lor P_2^3 x_1 x_2 x_3$
$\sigma = {x_1 f_1^0, x_2 f_1^0}$ $\neg P_1^2 f_1^0 f_1^0 \lor P_2^3 f_1^0 f_1^0 x_3$
Резольвента
Пусть имется 2 дизъюнкта: $L_1 \lor F$ и $L_2 \lor G$. Резольвентой называется результат применения склейки на оба/любой/никакой дизъюнкт с последующим приминением правила резолюций.
Метод резолюций
Пусть имеется набор дизъюнктов $D_1, D_2, …, D_n$, если построится такая цепочка $G_1, G_2, .. G_m = F$, что каждый элемент цепочки либо один из дизъюнктов, либо получен из предыдущих дизъюнктов по правилу резольвенты.
Исходных дизъюнктов n.
Пример.
$D_1 = \neg P_1^1 x_1 \lor \neg P_2^1 x_1 \lor P_3^1 f_1^1 x_1$
$D_2 = P_1^1 x_2 \lor P_3^1 f_1^1 x_3$
$D_3 = P_1^1 f_1^0$
$\sigma = {x_1 f_1^0}$ $\neg P_1^1 f_1^0 \lor \neg P_2^1 f_1^0 \lor P_3^1 $
Пример дизъюнкта
Когда некоторому дизъюнкту применяется подстановку, то результат называется примером данного дизъюнкта. $D^{\sigma}$ - пример дизъюнкта D.
Лемма о подъеме
Пусть $D’_1$ - это пример дизъюнкта $D_1, D_2’$ - пример дизъюнкта $D_2$. $D’$ - резольвента $D_1’$ и $D’_2$, тогда существует резольвента $D$ для $D_1 $ и $D_2$, для которой $D’$ является примером.
Доказательство—–доделать:
Замятин, страница 107
Можем считать, что в $D_1$ и $D_2$ нет общих переменных символов. Тогда мы можем считать, что есть общая подстановка $\sigma = \sigma_1 \circ \sigma_2$.