Резольвенция и факторизация

При доказательстве теорем в математической логике используются представления суждений в виде дизъюнкции литералов (в виде предложений, в клаузальной форме). Литерал L₁ называется дополнительным литералу L₂, если L₁ является отрицанием L₂.

Резольвента двух предложений получается следующим образом [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)}.

Дата добавления: 2015-07-11