2015-03-27
737
При доказательстве теорем в математической логике используются представления суждений в виде дизъюнкции литералов (в виде предложений, в клаузальной форме). Литерал L1 называется дополнительным литералу L2, если L1 является отрицанием L2.
Резольвента двух предложений получается следующим образом [29]:
1) переменные одного предложения переименовываются таким образом, чтобы они отличались от переменных другого предложения;
2) находится подстановка, при которой какой-либо литерал одного предложения становится дополнительным к какому-либо литералу другого предложения и эта подстановка производится в оба предложения;
3) литералы, дополнительные друг к другу, вычёркиваются;
4) если имеются одинаковые литералы, то все они, кроме одного в каком-либо предложении вычёркиваются;
5) дизъюнкция литералов, оставшихся в обоих предложениях, и есть резольвента.
Используется также факторизация. Фактором какого-либо предложения называется следствие этого предложения [29]:
1) находится подстановка при которой какие-либо литералы одинаковы;
|
|
|
2) после выполнения этой подстановки все одинаковые литералы, кроме одного, вычёркиваются;
3) дизъюнкция оставшихся литералов и есть фактор.
Процесс нахождения фактора называется факторизацией.
Пример [29].
Резольвента 
при подстановке {(g(x),x}, то есть g(x) заменяет x.
.
Здесь резольвенты нет. Переменные: x, y – термы: g(x), f(x).
Вместо переменной можно подставить терм, но вместо функции или константы терм подставить нельзя!
Пример [26].
{P(x,a,f(g(a))),P(z,y,f(u))}.
В этом случае наименьший общий унификатор: {(z,x),(a,y),(g(a),u)}.
Просто унификатор: {(b,x),(a,y),(b,z),(g(a),u)}.
