Спец_главы_математики

§2.7. Скулемизация алгебраических систем

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

Алгебраическая система A = hA; §i называется обогащением алгебраической системы A0 = hA0; §0i, если A = A0, § ¶ §0 и совпадают интерпретации всех сигнатурных символов из §0 в системах A и A0.

Если система A сигнатуры § является обогащением системы A0 сигнатуры §0, то A0 называется обеднением алгебраической системы A и

обозначается через A ¹ §0.

П р и м е р 2.7.1. Система A = hZ; +; ¢; 0; 1i является обогащением системы B = hZ; +; 0; 1i, а система C = hZ; +; 0i обеднением

системы B. ¤

Пусть § некоторая сигнатура, §S сигнатура, полученная из § добавлением:

а) новых константных символов c' для каждой формулы ' сигнатуры §, имеющей вид 9x0 Ã(x0);

б) новых n-местных функциональных символов f' для каждой фор-

мулы ' = 9x0 Ã(x0; x1; : : : ; xn) сигнатуры §, имеющей n > 0 свободных переменных.

Тогда сигнатура §S называется скулемизацией сигнатуры §. Через S(§) обозначим множество следующих предложений сигна-

туры §S, называемых аксиомами Скулема:

а) 9x0 Ã(x0) ! Ã(c') для каждой формулы ' = 9x0 Ã(x0) сигнатуры §;

б) 8x1 : : : xn(9x0 Ã(x0; x1; : : : ; xn) ! Ã(f'(x1; : : : ; xn); x1; : : : ; xn)) для каждой формулы ' = 9x0 Ã(x0; x1; : : : ; xn) (n > 0) сигнатуры §.

Согласно аксиомам Скулема из существования элемента, который можно подставить вместо переменной x0 в формулу Ã, следует возможность подстановки значения некоторой функции f' (константы c'), зависящего от оставшихся свободных переменных.

Если A алгебраическая система сигнатуры §, то любое ее обогащение AS = hA; §Si, являющееся моделью множества S(§), называется скулемизацией системы A. Возникающие при обогащении константы и операции, соответствующие символам c' и f', называются

скулемовскими константами и скулемовскими функциями.

51

Отметим, что в отличие от §S и S(§) скулемизация AS не определяется однозначно, поскольку из существования элементов, которые можно подставлять вместо переменных x0, вообще говоря, не следует

их единственность.

П р и м е р 2.7.2. Рассмотрим алгебраическую систему A =

hf

0; 1

g

;

P

(1)

; R

(2)

интерпретациями PA =

0; 1

, RA =

i с

f

g

f

(0; 0); (0; 1); (1; 1) .

S

g

В скулемизации A

для формулы ' - 9x P (x)

константный сим-

вол c' может быть проинтерпретирован как 0 или как 1, поскольку A j= P (0) и A j= P (1). Для функционального символа f'0, где '0 - 9x0R(x0; x1), возможны интерпретации f'0 = f(0; 0); (1; 0)g или f'0 = f(0; 0); (1; 1)g. ¤

Предложение 2.7.1. Любая алгебраическая система A имеет некоторую скулемизацию AS.

В следующем параграфе при работе с методом резолюций нам предстоит с помощью скулемизации снимать кванторы с формул, находящихся в предклазуальной нормальной форме. Говорят, что формула ' находится в клазуальной нормальной форме, если она получается из формулы Ã, находящейся в предклазуальной нормальной форме, удалением всех кванторов существования с одновременной заменой соответствующих переменных на термы, определяемые аксиомами Скулема, и последующим удалением всех кванторов всеобщности.

П р и м е р 2.7.3. 1. В примере 2.4.1 найдена формула

8x 9y 9u 8v (:'(x; y) _ Ã(u; v));

находящаяся в ПКНФ. С помощью скулемовских функций f1(x) и f2(x), заменяющих переменные y и u соответственно, эта формула преобразуется к следующей формуле, находящейся в КлНФ:

(:'(x; f1(x)) _ Ã(f2(x); v)):

2. Формула

9x 8y 8z 8u 9v ((P (x; y; z; u) _ :Q(z; u; v)) ^ R(x; z; v))

сигнатуры fP (4); Q(3); R(3)g находится в ПКНФ и приводится к следующей КлНФ с помощью скулемовской константы c, заменяющей переменную x, и скулемовской функции f(y; z; u), заменяющей переменную v:

(P (c; y; z; u) _ :Q(z; u; f(y; z; u))) ^ R(c; z; f(x; z; u)): ¤

52

§ 2.8. Метод резолюций в исчислении предикатов

Зафиксируем некоторую сигнатуру §.

Подстановкой сигнатуры § называется конечное множество вида ft1=x1; : : : ; tn=xng, где ti терм сигнатуры §, отличный от переменных xi (1 6 i 6 n), и все переменные x1; : : : ; xn различны. Подстановка, которая не содержит элементов, называется пустой и обозначается через ".

Мы будем использовать греческие буквы для записи подстановок.						,
y=z	c =x	F	y		=y
П р и м е р 2.8.1. Множества fF1(z)=x; (1) g, (1)f 1 (0),		(0)2(		)
F1(F2(c2))=zg подстановки сигнатуры § = fF1 , F2	; c1 ; c2 g. ¤

Пусть µ = ft1=x1; : : : ; tn=xng подстановка сигнатуры §, W множество формул (термов) сигнатуры §. Тогда W µ множество формул (термов) сигнатуры §, полученных из формул (термов) множества W заменой в них одновременно всех вхождений xi (1 6 i 6 n) на термы

ti (1 6 i 6 n). При этом предполагается, что выполняются все условия на записи формул (')xt11;:::;t;:::;xnn, ' 2 W .

Если W = f©g или W = ftg, где © формула, t терм сигнатуры §, то вместо f©gµ и ftgµ будем писать ©µ и tµ соответственно.

П р и м е р	2.8.2. Пусть µ			=	c	=x; F (c		)=y; y=z	g	подстановка
	(0)	(0)	; F (1)	(3)f	1		2			© = (F (x) ¼
сигнатуры § = fc1		; c2		; F1	g, t		= F1(x; y; z),

F1(x; c1; z)). Тогда tµ = F1(c1; F (c2); y), ©µ = (F (c1) ¼ F1(c1; c1; y)).

Пусть µ = ft1=x1; : : : ; tn=xng и ¸ = fq1=y1; : : : ; qm=ymg подстановки сигнатуры §. Тогда композиция подстановок µ и ¸ (µ±¸) есть под-

становка, которая получается из множества ft1¸=x1; : : : ; tn¸=xn; q1=y1; : : :, qm=ymg вычеркиванием всех элементов tj¸=xj, для которых tj¸ = xj,

ивсех элементов qi=yi, таких, что yi 2 fx1; : : : ; xng.

Пр и м е р 2.8.3. Пусть µ = ft1=x1; t2=x2g = fF (y)=x, z=yg, ¸ = fq1=y1; q2=y2; q3=y3g = fc1=x; c2=y; y=zg подстановки сигнатуры § =

fc(0)1 ; c(0)2 ; F (1)g. Тогда ft1¸=x1; t2¸=x2; q1=y1, q2=y2, q3=y3g = fF (c2)=x; y=y; c1=x; c2=y; y=zg. Так как t2¸ = y, то y=y должно быть вычеркнуто.

Так как x; y 2 fx; yg, то c1=x, c2=y также должны быть вычеркнуты. Таким образом, µ ± ¸ = fF (c2)=x, y=zg. ¤

У п р а ж н е н и е. Доказать: 1) ассоциативность композиции подстановок, т. е. (µ ± ¸) ± ¹ = µ ± (¸ ± ¹) для любых подстановок µ, ¸, ¹;

2)µ ± " = " ± µ для любой подстановки µ. ¤ Подстановка µ сигнатуры § называется унификатором для множе-

ства f©1; : : : ; ©kg формул сигнатуры §, если ©1µ = : : : = ©kµ. Множество формул f©1; : : : ; ©kg сигнатуры § называется унифицируемым,

если для него существует унификатор сигнатуры §.

53

П р и м е р 2.8.4. Множество fP (c1; y); P (x; F (c2))g формул сигнатуры § = fc(0)1 ; c(0)2 ; P (2); F (1)g унифицируемо, так как подстановка µ = fc1=x; F (c2)=yg является его унификатором. ¤

Унификатор ¾ для множества f©1; : : : ; ©kg формул сигнатуры § называется наиболее общим унификатором (НОУ), если для каждого унификатора µ сигнатуры § этого множества существует подстановка ¸ сигнатуры § такая, что µ = ¾ ± ¸.

Пусть W = f©1; : : : ; ©kg непустое множество атомарных формул сигнатуры §. Множеством рассогласований в W называется множество термов ft1; : : : ; tkg, где ti входит в ©i и начинается с символа (который есть либо сигнатурный символ, либо переменная), стоящего на первой слева позиции в ©i, на которой не для всех формул ©1; : : : ; ©k

находится один и тот же символ.
x	F		y;
П р и м е р 2.8.5. Пусть W = fP (x; F (y; z)); P (x; c), P ((1),		(
F1(z)))g множество формул сигнатуры § = fP (2), F (2), F1	g. Во

всех трех формулах первые четыре символа P (x; совпадают, а на пятом месте в первой и второй формулах стоят разные символы: F , c. Таким образом, множество рассогласований в W fF (y; z); c; F (y;

F1(z))g. ¤

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

Пусть W конечное непустое множество атомарных формул. Алгоритм унификации для множества W :

Шаг 1. Полагаем k = 0, Wk = W , ¾k = ".

Шаг 2. Если Wk одноэлементное множество, то остановка: ¾k НОУ для W . В противном случае найдем множество Dk рассогласований для Wk.

Шаг 3. Если существуют xk; tk 2 Dk такие, что xk переменная, не входящая в терм tk, то перейти к шагу 4. В противном случае остановка: множество W не унифицируемо.

Шаг 4. Полагаем ¾k+1 - ¾k±ftk=xkg и Wk+1 - Wkftk=xkg (заметим, что Wk+1 = W ¾k+1).

Шаг 5. Присвоить k значение k + 1 и перейти к шагу 2.

Теорема 2.8.1. Если W конечное непустое унифицируемое множество атомарных формул, то алгоритм унификации будет всегда заканчивать работу на шаге 2 и последняя подстановка ¾k будет НОУ для W . ¤

54

П р и м е р 2.8.6. Найти НОУ для множества W = fP (c; x, F2(F1(y))),

P(z; F2(z); F2(u))g.

1.Положим k = 0, W0 = W , ¾0 = ".

2.Так как W неодноэлементное множество, то ¾0 не является

НОУ для W . Множество рассогласований для W0 есть D0 = fc; zg.

3.В D0 существует переменная x0 = z, которая не встречается в терме t0 = c. Поэтому переходим к шагу 4.

4.Полагаем ¾1 - ¾0 ± fc=zg = " ± fc=zg = fc=zg, W1 - W0fc=zg = fP (c; x; F2(F1(y))); P (c; F2(c); F2(u))g.

5.Присваиваем k = 1.

6.Так как W1 неодноэлементное множество, множество рассогласований для W1 есть D1 = fx; F2(c)g.

7.Из D1 находим, что x1 = x, t1 = F2(c).

8.Полагаем ¾2 - ¾1 ±fF2(c)=xg, W2 - W1fF2(c)=xg = fP (c; F2(c); F2(F1(y))); P (c; F2(c); F2(u))g.

9.Присваиваем k = 2.

10.Так как W2 неодноэлементное множество, множество рассогласований для W2 есть D2 = fF1(y); ug.

11.Из D2 найдем, что x2 = u, t2 = F1(y).

12. Полагаем ¾3	- ¾2 ± fF1(y)=ug = fc=z; F2(c)=x; F1(y)=ug, W3
- W2fF1(y)=ug =	fP (c, F2(c), F2(F1(y))), P (c, F2(c), F2(F1(y)))g =

fP (c; F2(c); F2(F1(y)))g.

13. Множество W3 одноэлементно. Поэтому ¾3 = fc=z, F2(c)=x;

F1(y)=ug НОУ для W . ¤

П р и м е р 2.8.7. Определить, унифицируемо ли множество W = fP (F1(c); F2(x)); P (y; y)g.

1.Положим k = 0, W0 = W , ¾0 = ".

2.Так как W0 неодноэлементное множество, множество рассогла-

сований для W0 есть D0 = fF1(c); yg.

3.Из D0 находим, что x0 = y, t0 = F1(c).

4.Полагаем ¾1 - ¾0 ± fF1(c)=yg = fF1(c)=yg, W1 - fP (F1(c),

F2(x)), P (F1(c); F1(c))g.

5.Присваиваем k = 1.

6.Так как W1 неодноэлементное множество, множество рассогла-

сований для W1 есть D1 = fF2(x); F1(c)g.

7. В D1 нет элемента, который был бы переменной. Поэтому множество W не унифицируемо. ¤

Литерой сигнатуры § называется атомарная формула или отрицание атомарной формулы сигнатуры §. Дизъюнктом сигнатуры § называется литера сигнатуры § или дизъюнкция литер сигнатуры §.

55

Примеры дизъюнктов сигнатуры § = fP (1); F1(1); F2(2); c(0)g

P (F1(x)), :P (F1(x)), P (F1(x)) _:(F1(x) ¼ F2(x; y)), P (F2(F1(x), z)) _ :P (F2(x; y)) _ (x ¼ c).

Пусть © дизъюнкт сигнатуры § вида Ã1 _ ¢ ¢ ¢ _ Ãn _ Â или :Ã1 _

¢ ¢ ¢ _ :Ãn _ Â, где Ãi атомарные формулы сигнатуры § (1 6 i 6 n). Предположим, что множество формул fÃ1; : : : ; Ãng имеет НОУ ¾. Тогда Ã1¾ _¾ или соответственно :Ã1¾ _¾ называется склейкой ©. Полученную формулу в дальнейшем будем обозначать через ©¾.

П р и м е р 2.8.8. В формуле © = P (x) _ P (F (y)) _ :P2(x) подформулы P (x) и P (F (y)) имеют НОУ ¾ = fF (y)=xg. Следовательно,

©¾ = P (F (y)) _ :P2(F (y)) склейка ©. ¤

Пусть ©1, ©2 два дизъюнкта, не имеющих общих переменных, L1, L2 литеры в ©1 и ©2 соответственно. Если литеры L1 и L02 ´ :L2 имеют НОУ ¾, то дизъюнкт, получаемый из дизъюнкта ©1¾ _ ©2¾ вычеркиванием L1¾ и L2¾, называется бинарной резольвентой ©1 и ©2, а литеры L1 и L2 называются отрезаемыми литерами. Если ©1¾ = L1 и ©2¾ = L2, то полагаем бинарную резольвенту ©1 и ©2 равной 0.

Если ©1 и ©2 имеют общие переменные, то, заменив в формуле ©2 эти общие переменные на переменные, не встречающиеся в ©1 и ©2, получим формулу ©02, которая не имеет общих переменных с формулой ©1. Бинарной резольвентой формул ©1 и ©2 называется бинарная

резольвента формул ©1 и ©02.

П р и м е р 2.8.9. Найти бинарную резольвенту формул ©1 -

P1(x)_ P2(x) и ©2 - :P1(c) _ P3(x).

Заменив переменную x в ©2 на y, получим ©02 = :P1(c) _ P3(y).

Выбираем L1 = P1(x), L2 = :P1(c). Так как :L2 ´ L02 = P1(c), то L1 и L02 имеют НОУ ¾ = fc=xg. Бинарная резольвента формул ©1 и ©02

получается из ©1¾_©02¾ = P1(c)_P2(c)_:P1(c)_P3(y) вычеркиванием P1(c) и :P1(c). Следовательно, P2(c) _ P3(y) бинарная резольвента

©1 и ©2, а P1(x) и :P1(c) отрезаемые литеры. ¤

Резольвентой дизъюнктов ©1 и ©2 (res(©1; ©2)) является одна из следующих бинарных резольвент:

бинарная резольвента ©1 и ©2;

бинарная резольвента склейки ©1 и ©2;

бинарная резольвента ©1 и склейки ©2;

бинарная резольвента склейки ©1 и склейки ©2.

П р и м е р 2.8.10. Найти res(©1; ©2), где ©1 = P (x) _ P (F (y)) _

P1(F1(y)), ©2 = :P (F (F1(c1))) _ P2(c2).

Склейка ©1 есть ©01 = ©1fF (y)=xg = P (F (y)) _ P1(F1(y)). Бинарная резольвента ©01 и ©2 есть P1(F (F1(c1))) _ P2(c2). Следовательно,

res(©1; ©2) = P1(F (F1(c1))) _ P2(c2). ¤

56

Пусть S множество дизъюнктов сигнатуры §. Резолютивный вывод формулы © из S есть такая конечная последовательность ©1, : : :, ©k дизъюнктов, что ©k = © и каждый дизъюнкт ©i или принадлежит S, или является резольвентой дизъюнктов, предшествующих ©i.

Универсальным замыканием формулы ©(x1; : : : ; xn) называется предложение 8x1; : : : ; xn ©(x1; : : : ; xn).

Теорема 2.8.2. (теорема о полноте метода резолюций). Если S

множество дизъюнктов сигнатуры §, то множество универсальных замыканий формул из S невыполнимо тогда и только тогда, когда существует резолютивный вывод нуля из S. ¤

П р и м е р 2.8.11. Доказать невыполнимость множества формул

W = f©1; : : : ; ©6g, где

©1 = P1(c1; F (c2); F (c3)), ©2 = P2(c1),

©3 = P1(x; x; F (x)),

©4 = :P1(x; y; z) _ P3(x; z),

©5 = :P2(x) _ :P1(y; z; u) _ :P3(x; u) _ P3(x; y) _ P3(x; z),

©6 = :P3(c1; c3).

Построим резолютивный вывод 0 из W :

©7 = res(©2; ©5) = res(©2; ©5fz=yg) = :P1(z; z; u) _ :P3(c1, u) _

P3(c1; z);

©8 = res(©3; ©7) = :P3(c1; F (x)) _ P3(c1; x); ©9 = res(©6; ©8) = :P3(c1; F (c3));

©10 = res(©4; ©9) = :P1(c1; y; F (c3)); ©11 = res(©1; ©10) = 0. ¤

П р и м е р 2.8.12. Выполнимо ли множество предложений f©1; ©2g? Если множество выполнимо, построить систему, на которой предложения ©1 и ©2 истинны:

©1 - 9y 8x z((P1(x; z) ! (P2(x) ^ P3(y))) ^ P4(y));

©2 - 8x ((P4(x) ! :P3(x)) ^ 9y P1(x; y)):

Приведем формулы ©1, ©2 к предклазуальной нормальной форме:

©1 ´ 9y 8x; z ((:P1(x; z) _ P2(x)) ^ (:P1(x; z) _ P3(y)) ^ P4(y)),

©2 ´ 8x 9y ((:P4(x) _ :P3(x)) ^ P1(x; y)).

Введением символов скулемовской константы c и скулемовской функции F получаем, что выполнимость множества формул f©1; ©2g сигна-

туры § = fP1(2); P2(1); P3(1); P4(1)g равносильна выполнимости множества

57

формул
f8x; z ((:P1(x; z) _ P2(x)) ^ (:P1(x; z) _ P3(c)) ^ P4(c));	(2.1)
8x ((:P4(x) _ :P3(x)) ^ P1(x; F (x)))g;

сигнатуры §0 = § [ fc; F (1)g, что в свою очередь равносильно выполнимости множества формул

f8x; z (:P1(x; z) _ P2(x)); 8x; z (:P1(x; z) _ P3(c));	(2.2)
P4(c); 8x (:P4(x) _ :P3(x)); 8x P1(x; F (x))g:

Действительно, пусть множество формул f©1; ©2g выполнимо. То-

гда существует алгебраическая система A = hA; §i и c0 2 A, для которых A j= 8x z (:P1(x; z) _ P2(x)) ^ 8x z (:P1(x; z) _ P3(c0)) ^ P4(c0) и

A j= 8x (:P4(x) _ :P3(x)).

Кроме того, для любого a 2 A найдется элемент в A, который обо-

значим через G(a), такой, что A j= P1(a; G(a)), т. е. A j= 8x P1(x; G(x)). Тогда в системе A0 = hA; §0i, где c0 является интерпретацией c 2 §0,

G интерпретацией F 2 §0, истинны формулы из (2.2), а значит, и формулы из (2.1).

Напротив, если все формулы из (2.1) истинны в системе A0 = hA; §0i, то, очевидно, формулы (2.2) и ©1, ©2 будут истинны и в системе A = hA; §i.

Приведем формулы из (2.2) к КлНФ и исследуем на выполнимость с помощью метода резолюций получившееся множество дизъюнктов

f:P1(x; z) _ P2(x); :P1(x; z) _ P3(c); P4(c); :P4(x) _ :P3(x);

P1(x; F (x))g:

(2.3)

Имеем

res(:P1(x; z) _ P3(c); P1(x; F (x))) = P3(c), res(P3(c); :P4(x) _ :P3(x)) = :P4(c), res(:P4(c); P4(c)) = 0.

Построили резолютивный вывод нуля. Следовательно, множество дизъюнктов (2.3) невыполнимо. Тогда и множество предложений (2.1) невыполнимо, что равносильно невыполнимости множества предложе-

ний f©1; ©2g. ¤

П р и м е р 2.8.13. Выполнимо ли множество предложений f©1; ©2; ©3g? Если выполнимо, построить систему, на которой эти предложения

истинны: ©1 - 9x (P1(x) ^ 8y(P2(y) ! P3(x; y))), ©2 - 8x (P1(x) ! 8y (P4(y) ! :P3(x; y))),

©3 - 8x (P2(x) ! :P4(x)).

58

Приведем формулы ©1, ©2, ©3 к ПКНФ:

©1 ´ 9x 8y (P1(x) ^ (:P2(y) _ P3(x; y)),

©2 ´ 8x y (:P1(x) _ :P4(y) _ :P3(x; y)),

©3 ´ 8x (:P2(x) _ :P4(x)).

Из полученных формул получаем следующие формулы, находящиеся в КлНФ:

(P1(c) ^ (:P2(y) _ P3(c; y)), (:P1(x) _ :P4(y) _ :P3(x; y)), (:P2(x) _ :P4(x)).

Так же, как в примере 2.8.12, строим множество дизъюнктов:

fP1(c); :P2(y) _ P3(c; y); :P1(x) _ :P4(y) _ :P3(x; y);

:P2(x) _ :P4(x)g: (2.4)

Исследуем это множество на выполнимость с помощью метода резолюций:

res(P1(c); :P1(x) _ :P4(y) _ :P3(x; y)) = :P4(y) _ :P3(c; y);

res(:P2(y) _ P3(c; y); :P4(y) _ :P3(c; y)) = :P2(y) _ :P4(y): (2.5)

Других резольвент для множества (2.4) нет, поэтому резолютивный вывод 0 из (2.4) не существует. Рассмотрим множество, составленное из констант, входящих в формулы (2.4), т. е. множество fcg. Определим на fcg предикаты P1, P2, P3, P4 так, чтобы множество формул из (2.4) и (2.5) выполнялось на системе hfcg; P1; P2; P3; P4i. Из (2.5) следует, что необходимо потребовать c 2= P4, или hc; ci 2= P3 и c 2= P2. Положим c 2= P4, hc; ci 2= P3, c 2= P2. Из (2.4) следует, что необходимо потребовать c 2 P1. Таким образом, на системе hfcg; P1; P2; P3; P4; ci выполняются все формулы из (2.4). Более того, на ней истинны все формулы из (2.4) с навешанными на них кванторами всеобщности по переменным x, y, что равносильно истинности формул ©1, ©2, ©3 на

системе hfcg; P1; P2; P3i.

П р и м е р 2.8.14. Выполнимо ли множество предложений f©1; ©2g? Если выполнимо, построить систему, на которой эти предложения истинны:

©1 - 9u 8x 9z 8y (P3(z)^((P2(x; z)^:P1(u))_:((P3(y) ! P1(y)) ! P1(u)))),

©2 - 8x (9y P2(x; y) ! :P3(x)).

Преобразуем формулы ©1 и ©2 к предклазуальной нормальной форме:

©1 ´ 9u 8x 9z 8y (P3(z) ^ (P2(x; z) _ :P3(y) _ P1(y)) ^ :P1(u)), ©2 ´ 8x; y (:P2(x; y) _ :P3(x)).

59

Исследуем на выполнимость множество дизъюнктов
fP3(F (x)); P2(x; F (x)) _ :P3(y) _ P1(y); :P1(c);
:P2(x; y) _ :P3(x)g;	(2.6)

которое получается из преобразованных формул после введения символов скулемовской константы c и скулемовской функции F . Имеем

res(:P1(c); P2(x; F (x)) _ :P3(y) _ P1(y)) = P2(x; F (x)) _ :P3(c), res(P2(x; F (x)) _ :P3(c); :P2(x; y) _ :P3(x)) = :P3(c); res(P2(x; F (x)) _ :P3(y) _ P1(y); :P2(x; y) _ :P3(x)) =

:P3(y) _ P1(y),

res(:P3(y) _ P1(y); P3(F (x))) = P1(F (x)),

res(:P2(x; y) _ :P3(x); P3(F (x))) = :P2(F (x); y):

(2.7)

Таким образом, резолютивного вывода 0 из множества (2.6) не существует. Построим алгебраическую систему A = hA; P1; P2, P3; F; ci, в которой будут истинны формулы (2.6) и (2.7) с навешанными на них кванторами всеобщности по переменным x, y. Ясно, что c 2 A.

Так как A j=

8x(:P3(c) ^ P3(F (x)), то F (c)

6=

c. Положим A -

f

c; c0

g и

F (c)

-

c0

. Так как

A =

8

xP

(F (x))

, то необходимо, что-

c0

j

3

бы

F (c0) = c0

и

2

P

3. Из (2.7) следует, что

c = P

3. Поскольку

2

A =

8

x; y (P

(F (x))

_ :

P

(F (x); y))

c0

2

P

1,

(c0

; c) = P

2,

j

1

2

P

, полагаем

2

(c0; c0) = P

2. Предикаты

P

и

доопределяются произвольно. Та-

2

1

2

ким образом, в системе hfc; c0g; P1; P2; P3i такой, что c0 2 P1, (c0; c); (c0, c0) 2= P2, c 2= P3, c0 2 P3, истинны формулы ©1 и ©2. ¤

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

П р и м е р 2.8.15. Установить, что из посылки “Студенты суть граждане” следует заключение “Голоса студентов суть голоса граждан”.

Пусть формулы S(x); C(x) и V (x; y) означают “x студент”, “xгражданин” и “x есть голос y” соответственно. Тогда посылка и

заключение запишутся следующим образом:
8y (S(y) ! C(y))	(посылка),
8x (9y(S(y) ^ V (x; y)) ! 9z(C(z) ^ V (x; z)))	(заключение).

Формула, соответствующая посылке, эквивалентна дизъюнкту :S(y)_ C(y). Поскольку

60