18. Использование метода резолюций в логике предикатов

18.1. Подстановка и унификация

В математической логике широко используются приемы подстановки и унификации.

Подстановка – приём, в результате которого из некоторых данных формул получают их частные случаи, например, {(t₁,x₁),…,(t_n,x_n)}, где пара (t_j,x_i) означает, что всюду, где производится данная подстановка, переменная x_i заменяется термом t_j.

Пример [29].

Литерал Р(х,f(y),b) после подстановок:

₁={(z,x), (w,y)}; ₂={(a,y)}; ₃={(g(z),x), (a,y)}

имеет вид:

P_1=P(z,f(w),b); P_2=P(x,f(a),b); P_3=P(g(z),f(a),b).

Здесь P_i означает частный случай Р, полученный при подстановке _i.

Композиция двух подстановок _i и _j.

Композиция подстановок _i_j получается при применении подстановки _j к термам подстановки _i, с последующим добавлением любых пар из _j, содержащих переменные, не входящие в число переменных из _i [29].

Например:

_i={(f(x),z)} и _j={(a,x),(b,y),(d,z)}, то _i_j={(f(а),z),(b,y)}.

Нетрудно убедиться, что применение к литералу последовательно подстановок _i и _j даёт тот же результат, что и применение подстановки _i_j: .

Композиция подстановок ассоциативна: (_i_j)_k=_i(_j_k).

Унификация.

Множество литералов {L_i} называется унифицированным, если существует такая подстановка , что L_1=L_2=,…=L_n; .

Подстановка  называется унификатором для {L_i}.

Унификация применяется и для формул. Формулы, имеющие совместный частный случай, называются унифицируемыми, а набор подстановок – общим унификатором.

Наименьший возможный унификатор называется наиболее общим унификатором.

Известен алгоритм унификации, определяющий, являются ли две заданные формулы унифицируемыми, и, если это так, то позволяющий найти наиболее общий унификатор.

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

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

При доказательстве теорем в математической логике используются представления суждений в виде дизъюнкции литералов (в виде предложений, в клаузальной форме). Литерал 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)}.