ijk+1xk+1 ¢ ¢ ¢ijnxnM[x1; : : : ; xk¡1; xk; xk+1; : : : ; xn],

истинна в I.

Расширим интерпретацию I до I0, включив функцию f(x1; : : : ; x xk (функция, которая отображает x1; : : : ; xk¡1 в xk). Тогда

8x1 ¢ ¢ ¢ 8xk¡1ijk+1xk+1 ¢ ¢ ¢ijnxn

M[x1; : : : ; xk¡1; f(x1; : : : ; xk¡1); xk+1; : : : ; xn],

истинна вI0, т.е. F1 истинна в I0, что противоречит предположению. Следовательно, F должна быть противоречивой.

Следующий шаг доказательства.

Пусть в F имеется m кванторов существования. Положим F0 = F (F1 была определена ранее). Определим, что Fl; l = 1; m, получается из Fk¡1 заменой переменной, связанной первым слева квантором существования, сколемовской функцией. Ясно, что Fm = S.

Используя те же рассуждения, можно показать, что Fl¡1 противоречива тогда и только тогда, когда Fl противоречива для всех l = 1; m. В конечном счете мы заключим, что F противоречива тогда и только тогда, когда S противоречива. Теорема доказана. £

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

Наша цель состоит в применении метода резолюций для логики предикатов первого порядка. Существенным в применении метода резолюций является нахождение контрарных пар литералов. Если клозы не содержат переменных, то резолюция выполняется так же, как и для высказываний. Если клозы содержат переменные, то задача усложняется.

Пример 5.9.

C1 : P (x) _ Q(x),

C2 : :P (f(y)) _ R(x).

Литералы P (x) и P (f(y)) в исходном виде не образуют контрарную пару. Однако если подставить a 2 D вместо y в C2 и f(a) вместо x в C1 и C2, то получим

C10 : P (f(a)) _ Q(f(a)), C20 : :P (f(a)) _ R(f(a)).

Теперь P (f(a)) и :P (f(a)) контрараны и из C10 и C2 можно получить резольвенту C0 : Q(f(a)) _ R(f(a)).

В общем случае, подставив f(y) вместо x в C1 и C2, получим:

C1? : P (f(y)) _ Q(f(y)), C2? : :P (f(y)) _ R(f(y)).

Литералы P (f(y)) и :P (f(y)) теперь контрарны и можно получить резольвенту

C? : Q(f(y)) _ R(f(y)). J

Определение. Подстановка – это конечное множество вида

ft1=v1; : : : ; tn=vng,

где vi – переменная, ti – терм, отличный от vi, и все vi различны.

Выражением называют терм, множество термов, множество атомов, множество клозов, формулу и т.д. Любое выражение, не содержащее переменных, называют основным, например, основной терм. Если термы основные, то подстановка называется основной. Подстановка, которая не содержит элементов называется пустой и обозначается ".

Пример 5.10.

ff(z)=x; y=zg; fa=x; g(y)=y; f(g(b))=zg – примеры подстановок; fx=a; z=yg – не подстановка, так как a не переменная. J

Пусть µ = ft1=v1; : : : ; tn=vng – подстановка, E – выражение. Тогда Eµ – выражение, полученное из E заменой одновременно всех вхождений переменных vi; i = l1; m в E на термы

ti.

Определение. Eµ называется примером E.

Пример 5.11.

µ = fa=x; f(b)=y; c=zg; E = P (x; y; z) – выражение,

Eµ = P (a; f(b); c) – основной пример.

Пусть заданы две подстановки:

µ = ft1=x1; : : : ; tn=xng и ¸ = fu1=y1; : : : ; um=ymg.

Определение. Композиция подстановок µ и ¸ (обозначается µ ± ¸) есть подстановка, которая получается из множества

ft1¸=x1; : : : ; tn¸=xn; u1=y1; : : : ; um=ymg

удалением всех элементов tj¸=xj, для которых tj¸ = xj и всех элементов ui=yi, таких, что yi 2 fx1; : : : ; xng.

Пример 5.12.

Пусть µ = ft1=x1; t2=x2g = ff(y)=x; z=yg, ¸ = fu1=y1; u2=y2; u3=y3g = fa=x; b=y; y=zg.

Тогда µ ± ¸ = ft1¸=x1; t2¸=x2; u1=y1; u2=y2; u3=y3g = = ff(b)=x; y=y; a=x; b=y; y=zg

Так как t2¸ = x2, то t2¸=x2 (т.е. y=y) удаляется. Далее, y1 и y2 2 fx1; x2g, значит u1=y1 и u2=y2 (т.е. a=x и b=y) тоже удаляются.

Врезультате получим:

µ± ¸ = ff(b)=x; y=zg. J

Нетрудно заметить, что композиция подстановок ассоциативна и дает тот же результат, что и последовательное их применение, т.е. выражение E(µ ± ¸) эквивалентно (Eµ)¸.

В процедуре доказательства методом резолюций для отождествления контрарных пар литералов придется унифицировать два или более выражений, т.е. нужно найти подстановку, которая может сделать несколько выражений тождественными.

Определение. Подстановка µ называется унификатором для множества выражений fE1; : : : ; Ekg тогда и только тогда, когда E1µ = E2µ = ¢ ¢ ¢ Ekµ.

Множество fE1; : : : ; Ekg унифицируемо, если для него существует унификатор.

Пример 5.13. Множество выражений E = fP (a; y); P (x; f(z))g унифицируемо, т.к. подстановка µ1 = fa=x; f(z)=yg является его унификатором. Другой унификатор: µ2 = fa=x; a=z; f(a)=yg. J

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

Определение. Унификатор ¾ для множества выражений fE1; : : : ; Ekg

является наиболее общим унификатором (НОУ) тогда и только тогда, когда для каждого унификатора µ этого множества существует такая подстановка ¸, что µ = ¾ ± ¸.

В предыдущем примере µ1 есть НОУ, а µ2 = µ1 ± fa=zg.

5.4.0.1 Алгоритм унификации

Этот алгоритм позволяет найти НОУ для конечного множества выражений, если оно унифицируемо. Если множество неунифицируемо, алгоритм выявит этот факт.

Рассмотрим выражение P (a) и P (x). Они не тождественны. Чтобы отождествить выражения, нужно сначала найти рассогласование, а затем попытаться его исключить. Для P (a) и P (x) рассогласование будет fa; xg. Так как x – переменная, то x можно заменить на a и, таким образом, устранить рассогласование (рассогласование начинается с 3-й знаковой позиции в выражениях). В этом заключается идея алгоритма унификации.

Множество рассогласований D непустого множества выражений E получается выявлением первой слева позиции, в которой не для всех выражений из E находится один и тот же символ, и затем выписыванием из каждого выражения в E подвыражения, которое начинается с символа, занимающего эту позицию.

Пример 5.14. Пусть E = fP (x; f(y; z)); P (x; a); P (x; g(h(k(x))))g. Первая позиция, в которой не все выражения содержат один и тот же символ – пятая (первые 4 символа, включая скобки,одинаковы во всех выражениях P (x; : : :)). Таким образом, множество рассогласований есть

ff(y; z); a; g(h(k(x)))g.

5.4.0.2 Описание алгоритма

Шаг 1. Положить k = 1; Ek = E; ¾k = ".

Шаг 2. Если Ek состоит из одного выражения (т.е. все выражения равны), то останов: ¾k есть НОУ для E. В противном случае найти множество рассогласований Dk для Ek.

Шаг 3. Если в Dk существуют такие элементы vk и tk, что vk – переменная, не входящая в tk, то на Шаг 4; иначе стоп: множество не может быть унифицировано.

Шаг 4. Положить ¾k+1 = ¾k ± ftk=vkg и Ek+1 = Ekftk=vkg. (Заметим, что Ek+1 = E¾k+1).

Шаг 5. Положить k = k + 1; на Шаг 2.

Пример 5.15.

Найти НОУ для множества выражений:

E = fP (a; x; f(g(y))); P (z; f(z); f(u))g.

Шаг 1. k = 0; E0 = E; ¾0 = ".

Шаг 2. Так как в E выражения различны, то ¾0 не является НОУ для E. Множество рассогласований D0 = fa; zg.

Шаг 3. В D0 есть переменная z, не входящая в a.

Шаг 4. Положим ¾1 = ¾0 ± ft0=v0g = " ± fa=zg = fa=zg.

E1 = Eft0=v0g = Efa=zg = fP (a; x; f(g(y))); P (a; f(a); f(u))g

Шаг 5. k := k + 1 = 1; на Шаг 2.

Шаг 2. Множество E1 содержит более одного выражения. Множество рассогласований для E1: D1 = fx; f(a)g.

Шаг 3. Из D1 находим: v1 = x; t1 = f(a).

Шаг 4. ¾2 = ¾1 ± ft1=v1g = fa=zg ± ff(a)=xg = fa=z; f(a)=xg.

E2 = E1ft1=v1g = E1ff(a)=xg = fP (a; f(a); f(g(y))); P (a; f(a); f(u))g. Шаг 5. k = 2; на Шаг 2.

Шаг 2. Множество E2 содержит более одного выражения. Множество рассогласований для E2: D2 = fg(y); ug.

Шаг 3. v2 = u; t2 = g(y); u не содержится в g(y).

Шаг 4. ¾3 = ¾2 ± fg(y)=ug = fa=z; f(a)=x; g(y)=ug.

E3 = E2fg(y)=ug = fP (a; f(a); f(g(y))); P (a; f(a); f(g(y)))g = = fP (a; f(a); f(g(y)))g.

Шаг 5. k = 3; на Шаг 2.

Шаг 2. Так как E3 содержит одно выражение, то