Интерпретация формул. Формула имеет определенный смысл, т.е., обозначает некоторое высказывание, если существует какая-либо интерпретация. Интерпретировать формулу — это значит связать с ней определенное непустое множество D, т.е. конкретизировать предметную область, называемую также областью интерпретации, и указать:
· для каждой константы в формуле конкретный элемент из D;
· для каждой n -местной функциональной буквы в формуле конкретную n-местную функцию на D;
· для каждой n -местной предикатной буквы в формуле конкретное отношение между n элементами из D.
Пример 9.1.
Рассмотрим атом: G(f(a,b),g(a,b)) и следующую интерпретацию:
D - множество действительных чисел;
а=2, b=3;
f - функция сложения f(a,b)=a+b;
g - функция умножения g(a,b)=a*b;
G - отношение “не меньше”.
При такой интерпретации приведенная ниже формула обозначает высказывание “сумма 2+3 не меньше произведения 2*3 ”. Это утверждение неверно и поэтому G(f(a,b),g(a,b)) =Л. Если видоизменить интерпретацию, приняв b = 1 или b = 2, то G(f(a,b),g(a,b)) =И. Очевидно, существует много других интерпретаций, для которых приведенная формула в одних случаях имеет значение Л, в других — И.
Пример 9.2.
Рассмотрим формулу G(f(g(X,X),g(Y,Y)),g(a,g(Y,Y))) при интерпретации примера 2.2. Эта формула обозначает высказывание “ Х*Х +Y*Y>=2*X*Y ”, которое верно при любых X и Y из D и имеет значение И.
Пусть F и G - любые две ППФ, то значение истинности составного выражения, построенного из этих ППФ, даются таблицей истинности (табл. 9.1).
Таблица 9.1. Таблица истинности.
| F | G | ù F | F Ú G | F Ù G | F ® G | F «G |
| И | Л | И | И | И | И | И |
| Л | И | И | И | Л | И | Л |
| И | Л | Л | Л | Л | Л | И |
| Л | Л | И | Л | Л | И | И |
Таблица 9.2. Таблица эквивалентности.
| Эквивалентные формулы | ||
| ù F (ù F) | F | |
| F ® G | ù F Ú G | |
| F «G | (F ® G)Ù(G ® F) | |
| ù(F Ù G) ù(F Ú G) | ù F Úù G ù F Ùù G | законы де Моргана |
| F Ù(G Ú H) F Ú(G Ù H) | (F Ù G)Ú(F Ù H) (F Ú G)Ù(F Ú H) | законы дистрибутивности |
| F Ú G F Ù G | G Ú F G Ù F | законы коммуникативности |
| (F Ú G)Ù H (F Ù G)Ú H | F Ú(G Ù H) F Ù(G Ú H) | законы ассоциативности |
| F ® G | ù G ® F | контрапозиционный |
| F Ùù F F Úù F F Ù 0 F Ù 1 F Ú 0 F Ú 1 | 0 1 0 F F 1 | |
| " XF(X) $ XF(X) | " YF(Y) $ YF(Y) | законы немых переменных |
| ù($ XF(X)) ù(" XF(X)) | " X (ù F(X)) $ X (ù F(X)) | |
| " X(F(X) Ù G(X)) $ X(F(X) Ú G(X)) | " XF(X) Ù" XG(X) $ XF(X) Ú$ XG(X) |
Если истинности двух ППФ независимо от интерпретации, то говорят, что эти ППФ являются эквивалентными. Пользуясь таблицей истинности легко установить следующие эквивалентности (табл. 9.2).
Принцип резолюций
Аппарат логики предикатов используется для представления задачи в виде теоремы: формула Н логически следует из формулы G, т.е. G ® Н. Доказательство этой теоремы состоит в том, чтобы показать, что каждая интерпретация, удовлетворяющая G, удовлетворяет и Н, или что ù G Ú Н истинно для любой интерпретации, так как ù(ù G Ú H)= G Ùù Н, то на практике обычно доказывают невыполнимость множества предложений G Ùù Н.
С целью упрощения доказательства теоремы все формулы представляются в виде дизъюнкций литералов. Литералом (или литерой) называют атом или его отрицание. Формулу, представляющую собой дизъюнкцию литералов, называют предложением (или дизъюнктом).
Например:
R(Z,a,g(X)) Ú ( ù T(U)) Ú(ù U(b,k(c)).
Иными словами в каждой формуле необходимо исключить все логические операции (включая кванторы), кроме дизъюнкции и уменьшить область действия знака отрицания до одной предикатной буквы.
Преобразование ППФ в предложения.
Перед тем как объяснить процесс резолюции, покажем, что любую ППФ исчисления предикатов первого порядка можно преобразовать в множество предложений, используя законы эквивалентности. Процесс такого преобразования состоит из последовательных этапов, которые покажем на следующем примере ППФ:
((" X)((P(X) Ù Q(X,a)) ® (R(X,b) Ù((" Y)((" Z)(R(Y,Z) ® T(X,Y)))))) Ú ((" X)S(X)).
Исключение символов эквивалентности и импликации. Для этого воспользуемся следующими законами эквивалентности: (F «G) заменим на ((F ® G)Ù(G ® F)) и (F ® G) заменим на (ù F Ú G). В нашем примере такая подстановка даст
((" X)(ù(P(X) Ù Q(X,a)))Ú(R(X,b) Ù((" Y)((ù(" Z)(R(Y,Z))Ú T(X,Y))))))Ú ((" X) S(X).
Уменьшение области действия знаков отрицания. Нужно выполнить такое преобразование, чтобы каждый знак отрицания применялся не более чем к одной атомной формуле. Для этого используем следующие законы эквивалентности:
(ù(ù F)) и F
(ù(F Ú G)) и (ù F)Ù(ù G)
(ù(F Ù G)) и (ù F)Ú(ù G)
(ù($ X) F(X)) и (" X)(ù F(X))
(ù(" X) F(X)) и ($ X)(ù F(X))
Полученная нами ППФ преобразуется к виду:
((" X)((ù P(X) Úù Q(X,a) Ú(R(X,b) Ù((" Y)((($ Z)ù R(Y,Z))Ú T(X,Y)))))) Ú ((" X) S(X)).
Разделение переменных. В пределах области действия квантора переменная, связанная с этим квантором, представляет собой немую переменную. Такую переменную в области действия квантора можно заменить любой другой (не встречающейся) переменной, при этом значение истинности ППФ не изменится. Стандартизация переменных в пределах ППФ означает переименование немых переменных с той целью, чтобы каждый квантор имел свою, свойственную только ему, немую переменную. Так вместо записи
(" Х)(Р(Х) Ú($ Х) Q(Х))
можно написать
(" X)(P(X) Ú($ Y) Q(Y)).
Полученная на предыдущем этапе ППФ преобразуется к виду
((" X)((ù P(X) Úù Q (X,a)Ú(R (X, b)Ù((" Y)((($ Z)ù R(Y,Z))Ú T(X,Y))))))Ú ((" U) S(U)).
Исключение кванторов существования. Рассмотрим ППФ
(" X)($ Y)P(X, Y)),
которую можно прочитать как: “Для всех X существует некоторое Y (возможно, зависящее от X) такое, что P(X,Y) ”. Поскольку квантор существования находится в области некоторого квантора общности, то можно допустить, что “существующий” Y зависит от X. Пусть эта зависимость определяется функцией Y=g(X), отображающей каждое X в Y. Такая функция называется сколемовской или функцией Сколема. Заменив Y на g(X), мы исключим квантор существования, и наша ППФ примет вид:
(" X)(P(X,g(X)).
Пусть ППФ ($ Y) P(Y) является подформулой другой ППФ, в которой Х1..., Хn вантифицированы универсально. Тогда удаляют Y и заменяют встречающуюся Y сколемовской функцией f(Х1..., Хn). Заметим, что эта функция, будет содержать столько аргументов, сколько имеется универсальных квантификаторов слева от формулы ($ Y) P(Y). Эта функция, как мы уже говорили, просто выражает существование соответствия априори между совокупностью значений Х1..., Хn и значениями Y. Поскольку эта функция заранее неизвестна, то в каждой замене Y мы должны записывать новую функциональную букву, которая отличается от уже имеющихся. Когда слева от символа “$” отсутствуют символы “"”, то вводимая функция Сколема не будет содержать аргументов: следовательно это будет новая константа, называемая константой Сколема. Так ППФ ($ Y) P (Y) заменится на Р(а), где про константу “ а ” известно, что она существует.
После выполнения замены Z функцией Сколема g(X,Y) наша ППФ будет иметь вид
((" X)((ù P(X) Úù Q(X,a) Ú(R(X,b) Ù((" Y)((ù R(Y,g(X,Y)))Ú T(X,Y)))))) Ú ((" U) S(U)).
Перемещение всех квантификаторов общности в начало ППФ (без изменения их относительного порядка). Каждый квантор общности имеет свою переменную и поэтому такие кванторы можно переместить в начало формулы, считая, что область действия каждого из них включает всю последующую часть ППФ. Говорят, что результирующая ППФ находится в префиксной форме. Она состоит из цепочки кванторов, называемой префиксом, и следующей за ней бескванторной формулы, называемой матрицей.
Префиксная форма для нашей ППФ имеет вид
(" X)(" Y)(" U)(ù P(X) Úù Q(X,a) Ú(R(X,b) Ù(ù R(Y,g(X,Y)) Ú T(X,Y)))Ú S(U)).
Приведение матрицы к конъюнктивной нормальной форме. Матрица находится в конъюнктивной нормальной форме, если она записана как конъюнкция конечного множества дизъюнкций литералов. Например:
(P(X) Ú Q(X,Y))Ù(P(Y) Úù R(Y))
Q (X)/\ R (X, Y)
ù R(Y)
Любую матрицу можно привести к конъюнктивной нормальной форме применением законов ассоциативности и дистрибутивности операций Ú и Ù. После приведения матрицы нашего примера ППФ в конъюнктивную нормальную форму эта ППФ примет следующий вид
(" X)(" Y)(" U)(ù P(X) Úù Q (X,a)Ú(R(X,b) Ú S(U)) Ù (ù P(X) Úù Q(X,a) Úù R(Y,g(X,Y))Ù T(X,Y) Ù S(U)).
Исключение кванторов общности. Поскольку все переменные в ППФ должны быть связаны, то можно предположить, что для каждой из них имеется квантор общности. При этом порядок расположения этих кванторов роли не играет, так что можно их исключить из ППФ. После исключения кванторов из ППФ у нас остается лишь матрица в конъюнктивной нормальной форме.
Исключение символов конъюнкции. Теперь можно исключить символы Ù, путем замены выражения типа (Р Ù Q) на множество ППФ { Р, Q }. В результате выполнения таких замен получим конечное множество ППФ, каждая из которых является дизъюнкцией литералов. А любая ППФ, содержащая дизъюнкцию литералов, как мы условились, является предложением.
Наш пример ППФ преобразуется в следующее множество предложений:
ù P (X) Úù Q(X,a) Ú (R(X,b) Ú S(U)
ù P(X) Úù Q(X,a) Úù R(Y,g(X,Y)
T(X,Y)
S(U)
Переименование (разделение) переменных. Символы переменных должны быть изменены так, чтобы каждый появился не более, чем в одном предложении. Напомним, что (" Х (Р(Х) Ù Q(Х)) эквивалентно (" Х)Р(Х) Ù(" Y)Q(Y). Теперь наши предложения приобретают вид
ù P(X) Úù Q(X,a) Ú(R(X,b)ÚS(U)
ù P(Z) Úù Q(Z,a) Úù R(Y,g(Z,Y)
T(A,B)
S(C)
Вместо переменных в литералах могут находиться термы, не содержащие переменных. Тогда говорят, что имеет место основной частный случай. Например. P(a.f(g(b))) является основным частным случаем P(X,Y).
Пример 9.3.
Преобразовать высказывание “Все дети имеют матерей” в предложения, т.е. в дизъюнкцию литералов. Это высказывание можно представить следующей ППФ:
" X $ Y (ребенок(X) ® мать(Y)Ùотносится(X, Y)).
Для удаления квантора существования заменим переменную Y функцией Сколема g(Х), т.е. Y=g(X), откуда получим:
" Х (ребенок(Х) ® мать(g(Х))Ùотносится(Х,g(Х))).
Теперь можно исключить квантор общности, который распространяет свое действие на все выражение Кроме того заменяем символ “импликация” дизъюнкцией, используя закон P ® Q º ù P Ú Q, откуда получаем:
ùребенок(Х)\/мать(g(Х))/\относится(Х,g(Х)).
Используя закон
P \/(Q/\R) º (PÚQ)/\ (PÚR)
можем написать
ùребенок(Х)Úмать(g(Х)),
ùребенок(Х)Úотносится(Х,g(Х)).
Полученные два предложения можно интерпретировать так: “Если X — ребенок, то он относится к матери, выражаемой функцией g(X) ”. Из них следует:
ребенок(X) ® мать(g(X)) и
ребенок(X)Úотносится(X,g(X)).
Резольвенты. Говорят, что литерал является конкретным, если он не содержит никакой переменной, Например, ù Р (а) или Q(a,f(b)) являются конкретными литералами, в то время как ù Р(Х) или Q(X<f(y)) не являются таковыми. Конкретным предложением является дизъюнкция конкретных литералов.
Пусть имеются два конкретных предложения
P1Ú P2Ú...ÚРn и ù P1ÚQ2Ú...ÚQn.
Здесь литерал ù Р1 является отрицанием литерала Р1. Из этих двух предложений можно вывести новое предложение, называемое резольвентой или резолюцией. Резольвентой является дизъюнкция этих предложений с последующим исключением пары P1 и ù P1.
Рассмотрим несколько частных случаев получения резольвенты.
Предложение Q является резольвентой двух конкретных предложений Р и ù P Ú Q (или Р и Р ® Q). Следовательно, принцип резолюций покрывает правило вывода, называемое modus ponens.
Предложение ù Р Ú Q (или P ® Q) является резольвентой конкретных предложений ù P Ú R, ù R Ú Q (или P ® R и R ® Q). Это правило вывода называют сцеплением.
Из предложений Р иù Р получается пустое предложение, которое является признаком противоречия.
Два конкретных предложения могут не иметь резольвенты или могут иметь множество резольвент. Например, из P Ú Q Ú R и ù P Úù Q Ú S получаются резольвенты Q Úù Q Ú R Ú S или P Úù P Ú R Ú S (которые в действительности являются эквивалентными).
Предложение ù Р является резольвентой конкретных предложений ù Q и ù P Ú Q (или ù Q и P® Q). То есть принцип резолюций вновь покрывает правило вывода.
Для того, чтобы обобщить это правило на случай предложений, содержащих переменные, рассмотрим процесс унификации предложений, приводящий к тому, что они будут содержать дополнительные литералы.
Унификация. Рассмотрим, например, два предложения:
ù F(X) Ú G(X) и F(f(Y)).
Если первое предложение заменить на
ù F(f(Y)) Ú G(f(Y)),
то принцип резолюций для этих предложений реализуется более просто: после исключения дополнительных литералов ù F(f(Y)) и F(f(Y)) получаем предложение G(f(Y)). Операция унификации представляет собой процесс замены переменных с целью появления дополнительных литералов в различных предложениях.
Заменой s, называют конечное множество упорядоченных пар s=((t1|U1),..., (tn|Un)}, где пара (ti|Ui) означает, что переменная Ui заменяется термом ti. Применение замены s={tilUi}i к некоторому выражению (терму или формуле) обозначается через Es и называется установлением Е в соответствии с s. В предложении Е заменяют все начальные появления каждой переменной Ui на ti.
Пример 9.4.
Пусть E=F(g(X),a,Y),
s1 ={ Z|X,U|Y }, s2={Y|X,f(X)|Y}, s3={blX,m(b)|Y}.
Имеем:
Es1=F(g(Z),a,U), Es2=F(g(Y),a,f(X)), Es3=F(g(b),a,m(b)).
Заметим, что при переходе от Е к Es2 только начальные экземпляры X и Y являются объектами замены, а не экземпляры, возникшие в процессе применения s2. Отсюда следует, что результат не зависит от порядка применения элементов замены.
Композицией двух замен a и b называется замена g, обозначаемая g=a°b полученная следующим образом:
а) применяют b к термам a (к левым частям);
b) исключают из b пары ti | Ui такие, что Ui является переменной a;
с) собирают пары, полученные в а) и b).
Например,
{a|X,g(Y,Z,U)|V}o{b|X,c|Y,f(X)|Z,k(d)|V,f(X)|W}={a|X,g(c,f(X),U)|U,c|Y, f(X)|Z, f(X)|W}.
Нетрудно убедиться в том, что применение к литералу последовательно замен a и b дает тот же результат, что и применение замены g=a°b. То есть (Еa)b = Е(a°b). Известно, что композиция замен ассоциативна:
(a°b)°g = a°(b°g).
Легко доказать, что в общем случае a°b ¹ b°a.
Унификаторы. Множество выражений {Еi} (термов или формул) является унифицируемым, если существует такая замена (унификатор) s, что все Eis идентичны. Обозначим выражение, полученное с помощью унификатора s через {Ei}s.
Пример 9.5.
Замена
s = {a|X, c|Y, c|U, b|Z, b|U, g(b)|W}
является унификатором для
{Ei}i={F(X,f(Y),g(b)),F(X,f(c),g(Z)),F(X,f(c),g(U), F(X,f(U),W)},
поскольку все выражения устанавливаются в
F(a.f(с),g(b)).
Может существовать множество унификаторов для данного множества выражений.
Простейшим унификатором множества выражений {Ei} называют унификатор r такой, что для любого другого унификатора s для {Еi} существует замена s ’ такая, что s=r°s’.
Легко показать, что для любого унифицируемого множества Е существует простейший унификатор и если r1 и r2 такие унификаторы для множества {Еi}, тогда {Еi}r1 и {Еi}r2 идентичны.
В примере 9.5 простейшим унификатором для множества выражений {Е1,Е2,ЕЗ,Е4} является r={c|Y, c|U, b|Z, b|U, g(b)|W} заметим, что s=r°{а|Х}.
Сущность принципа резолюций. На практике установление невыполнимости множества предложений осуществляется посредством принципа резолюций. Речь идет о процедуре логического вывода новых предложений из множества исходных.
Рассмотрим два предложения P(X) Ú Q(Y) и R(Z) Úù Q(Y). Из этих предложений можно вывести резольвенту P(X) Ú Q(Z), т.е. (P(X) Ú Q(Y),R(Z) Úù Q(Y)} ® P(X) Ú R(Z) }.
Процесс применения принципа резолюций к двум предложениям с целью получения резольвенты называется резольвенцией, или резолюцией.
Если любая интерпретация, удовлетворяющая множеству исходных предложений G, удовлетворяет и предложению H, полученному из G, то H называют следствиемG.
Принцип резолюций состоит:
В получении новых предложений на основании множества исходных и вновь получаемых предложений;
В отыскании частных случаев формул F(t1,...,tn) из F(V1,...,Vn) при подстановке вместо Vi произвольных термов ti, т.е. F(V1,...,Vn) ® F(t1,...,tn).
Резольвенту двух предложений можно получить следующим образом:
1. Переименовать переменные двух предложений, так чтобы последние стали одинаковыми.
2. Найти подстановку, преобразующую литерал одного предложения в дополнительный по отношению к некоторому литералу другого предложения и произвести эту замену в обоих предложениях.
3. Вычеркнуть дополнительные друг к другу литералы.
4. Удалить одинаковые литералы в предложении кроме одного.
5. Дизъюнкция литералов, оставшихся в обоих предложениях, является резольвентой.
Например, исходя из G=P(X,f(a)) ÚP (X,f(Y)) Ú Q(Y) и Н =ù P(Z,f(a)) Úù Q(Z) получают три различные резольвенты.
Резольвенту, получаемую на основании двух дополняющих друг друга литералов, например Р(Х) и ù Р(Х) называютпустым предложением или пустой резольвентой и обозначают символом œ.
Например, исходя из G = ù Р(Х) и Н = P(f(Y)) Ú P(Z) получает две пустых резольвенты.
Если некоторая последовательность резолюций, применяемых к исходному множеству предложений Е и множеству резольвент, полученных в процессе резолюции, приводит к пустому предложению, то множество Е является невыполнимым.
