Семантика языка предикатов первого порядка

Интерпретация формул. Формула имеет определенный смысл, т.е., обозначает некоторое высказывание, если существует ка­кая-либо интерпретация. Интерпретировать формулу — это зна­чит связать с ней определенное непустое множество 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. Таблица истинности.

Таблица 9.2.Таблица эквивалентности.

Если истинности двух ППФ независимо от интерпретации, то говорят, что эти ППФ являются эквивалентными. Пользуясь таблицей истинности легко установить следующие эквивалентности (табл. 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) является подформулой другой ППФ, в которой Х₁..., Х_n вантифицированы универсально. Тогда удаляют Y и заменяют встречающуюся Y сколемовской функцией f(Х₁..., Х_n). Заметим, что эта функция, будет содержать столько аргументов, сколько имеется универсальных квантификаторов слева от формулы ($Y)P(Y). Эта функция, как мы уже говорили, просто выражает существование соответствия априори между совокупностью значений Х₁..., Х_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Ú...ÚQ_n.

Здесь литерал ùР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=((t₁|U₁),...,(t_n|U_n)}, где пара (t_i|U_i) означает, что переменная U_i заменяется термом t_i. Применение замены s={t_ilU_i}i к некоторому выражению (терму или формуле) обоз­начается через Es и называется установлением Е в соответствии с s. В предложении Е заменяют все начальные по­явления каждой переменной U_i на t_i.

Пример 9.4.

Пусть E=F(g(X),a,Y),

s₁={Z|X,U|Y}, s₂={Y|X,f(X)|Y}, s₃={blX,m(b)|Y}.

Имеем :

Es₁=F(g(Z),a,U), Es₂=F(g(Y),a,f(X)), Es₃=F(g(b),a,m(b)).

Заметим, что при переходе от Е к Es₂ только начальные экземпляры X и Y являются объектами замены, а не экземпляры, возникшие в процессе применения s₂. Отсюда следует, что результат не зависит от порядка применения элементов замены.

Композицией двух замен a и b называется замена g, обозначаемая g=a°b полученная следующим образом :

а) применяют b к термам a (к левым частям);

b) исключают из b пары t_i | U_i такие, что U_i является переменной 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, что все E_is идентичны. Обозначим выражение, полученное с помощью унификатора s через {E_i}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)).

Может существовать множество унификаторов для данного множества выражений.

Простейшим унификатором множества выражений {E_i} назы­вают унификатор r такой, что для любого другого унификатора s для {Е_i} существует замена s’ такая, что s=r°s’.

Легко показать, что для любого унифицируемого множества Е существует простейший унификатор и если r₁ и r₂ такие уни­фикаторы для множества {Е_i}, тогда {Е_i}r₁ и {Е_i}r₂ идентич­ны.

В примере 9.5 простейшим унификатором для множества выражений {Е₁,Е₂,Е_З,Е₄} является 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(t₁,...,t_n) из F(V₁,...,V_n) при подстановке вместо V_i произвольных термов t_i, т.е. F(V₁,...,V_n)®F(t₁,...,t_n).

Резольвенту двух предложений можно получить следующим образом:

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) получает две пустых резольвенты.

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