Taran_T_A_quot_Osnovy_Diskretnoy_Matematiki_qu

12.7.3. Доказательство логических следований

В данном разделе мы рассмотрим два способа доказательства логических следований: неформальный способ, основанный на доказательстве от противного, и формальный вывод в исчислении предикатов. В следующий главе будет рассмотрен более эффективный метод, позволяющий автоматизировать процесс доказательства логического следования (логической общезначимости).

Пример 12.1. На области определения «люди» заданы высказывания:

1.Некоторые студенты любят своих преподавателей.

2.Никто не любит невежественных людей.

Следовательно, ни один преподаватель не является невежественным.

Пусть P(x): x — студент, D(x): x — преподаватель, Q(x): x — невежественный, L(x, y): x любит y. Формализуем посылки:

по крайней мере одно значение y = a, такое что |D(a) → ¬Q(a)| = F, откуда получаем, что |D(a)| = T, |¬Q(a)| = F, т.е. |Q(a)| = T.

Из посылки F1: | x(P(x) & y(D(y) → L(x, y)))| = T следует, что существует по крайней мере одно значение x = b, такое, что |P(b) & y(D(y) → L(x, y))| = T, откуда получаем: |P(b)| = T и | y(D(y) → L(b, y))| = T. Поскольку последнее истинно для всякого

|Q(a) → ¬L(b, a)| = T. Так как |Q(a)| = T, то |¬L(b, a)| = T. Получаем, что истинны оба утверждения: |L(b, a)| = T и |¬L(b, a)| = T. Полу- ченное противоречие доказывает логическое следование.

В формальном выводе применяются правила: универсальной конкретизации (УК), экзистенциальной конкретизации (ЭК), удаления

&(уд. &), введения & (вв. &), правило MP.

Формальный вывод.

Пример 12.2. На области определения «люди» заданы высказывания:

1.Все старые члены конгресса — юристы.

2.Âñå женщины-юристы восхищаются каким-нибудь судьей.

3.Только судьи восхищаются судьями.

4.Все судьи восхищаются всеми судьями.

Что думает судья Джонс по поводу своей старой тещи, которая является членом конгресса? Ответ: Джонс восхищается своей тещей.

Проверить, что это заключение логически следует из заданных посылок.

Пусть х — предметная переменная, которая принимает значения из области определения «люди». Введем предикаты: J(x): x — судья;

L(x): x — юрист; C(x): x — член конгресса; W(x): x — женщина; А(х, у): х восхищается у, D – Джонс, T – теща. Формализуем посылки.

1. õ(Î(õ) & C(x) → L(x))

Все старые члены конгресса — юристы. 2. x(W(x) & L(x) → y(J(y) & A(x,y)))

Все женщины-юристы восхищаются каким-нибудь судьей.

3. x y(J(y) & A(x,y) → J(x))

Только судьи восхищаются судьями. 4. x(J(x) → y(J(y) → A(x,y)))

Все судьи восхищаются всеми судьями. 5. J(D)

Джонс – судья,

6. W(T) & O(T) & C(T)

старая теща, член конгресса.

Доказать: A(D, T) – судья Джонс восхищается тещей.

Глава 13. АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

13.1. Введение

Поиск общей разрешающей процедуры для проверки общезна- чимости формул был начат давно. Первым пытался найти такую процедуру Лейбниц (1646—1716), в дальнейшем над этим работала школа Гильберта. Эти попытки продолжались до тех пор, пока Ч¸рч и Тьюринг независимо друг от друга не доказали, что не существует никакой общей разрешающей процедуры, никакого алгоритма, проверяющего общезначимость формул в логике предикатов первого порядка. Тем не менее, существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима. Для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Принимая во внимание результат Ч¸рча и Тьюринга, это лучшее, что можно ожидать от алгоритма поиска доказательства.

Â1930 г. важный подход к автоматическому доказательству теорем был дан Эрбраном. По определению общезначимая формула есть формула, которая истинна при всех интерпретациях. Эрбран разработал алгоритм нахождения интерпретации, которая опровергает данную формулу. Однако, если данная формула на самом деле общезначима, то такой интерпретации не существует и алгоритм оканчивает работу за конечное число шагов. Метод Эрбрана служит основой для большинства современных методов автоматического поиска доказательства. Главный результат был получен Робинсоном, который ввел так называемый метод резолюций.

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

следующем. Пусть выполняется логическое следование: F1, F2 |= G. Тогда |= F1 & F2 → G логически общезначима, и, следовательно, |¬(F1 & F2 → G)| = |F1 & F2 & ¬G| ≡ F. Поскольку по определению посылки F1, F2 истинны, формула F1 & F2 & ¬G может обратиться

âложь только, если |¬G| = F, т.е. если |G| = T. Тогда логическое следствие выполнено. В принципе процедура опровержения формализует метод редукции. Проблема поиска автоматического доказательства при использовании процедуры опровержения значительно облегчается благодаря использованию так называемых «стандартных» форм формул. Любую формулу логики предикатов можно привести к эквивалентной ей предваренной нормальной форме,

когда все кванторы вынесены вперед, а в области действия кванторов формула находится в конъюнктивной нормальной форме. Если такая формула имеет только кванторы всеобщности, то она будет ложна, если найдется хотя бы одна интерпретация, которая обращает ее в ложь. Тогда эквивалентная ей исходная формула также будет ложна, а ее отрицание, соответственно, истинно. Если же среди кванторов имеются кванторы существования, то проблема усложняется. Однако, кванторы существования можно снять (на основании правила экзистенциальной конкретизации), в результате будет получена так называемая «скулемовская стандартная форма». Тогда поиск опровергающей интерпретации применяется к этой форме.

13.2. Предваренные нормальные формы

Определение 13.1. Формула А находится в предваренной нормальной форме (ПНФ), если она имеет вид: (Q1x1)...(Qnxn)М, где каждое Qixi åñòü õi èëè õi, а М — формула в конъюнктивной нормальной форме, не содержащая кванторов. (Q1x1)...(Qnxn) называется префиксом, а М — матрицей формулы А.

Теорема 13.1. Существует эффективная процедура приведения любой формулы логики предикатов к эквивалентной ей предваренной нормальной форме.

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

1.Пусть m = 0. Тогда формула А не содержит связок и находится

âÏÍÔ.

2.Предположим, что существует ПНФ для формулы В с числом связок n. Докажем, что существует ПНФ для формулы А с числом связок m = n + 1.

1 случай. Пусть существует ПНФ для В = (Q1x1)...(Qnxn)М. Формула А образована из В с помощью операции отрицания: А = ←(Q1x1)...(Qnxn)М. По законам де Моргана связка ←проносится через кванторы: ← xÌ ≡ x←Ì, ←xÌ ≡ x←М. Полученная формула будет находиться в ПНФ.

2 случай. Формула А образована из двух формул В1 и В2 с числом связок n < m с помощью связок конъюнкции & или

дизъюнкции : (Q1x1) ... (Qnxn) Ì1 & (Q1y1) ... (Qnyn)M2 èëè (Q1x1) ... (Qnxn) M1 (Q1y1) ... (Qnyn)M2. Тогда, если формулы В1 и В2 имеют кванторы по одной и той же переменной, используем

законы замены связанных переменных:

xP(x) ≡ yP(y), xP(x) ≡ yP(y),

так, чтобы ни одна свободная переменная не стала связанной в результате этой замены. После этого воспользуемся законами коммутативности для & и и законами пронесения кванторов:

x(P(x) & B) ≡ xP(x) & B, x(P(x) B) ≡ xP(x) B,x(P(x) & B) ≡ xP(x) & B, x(P(x) B) ≡ xP(x) B,

(B не содержит вхождений х).

3 случай. Формула А образована из В навешиванием квантораили . Тогда, поскольку В находится в ПНФ, вновь полученная формула будет в ПНФ.

Примеры.

1. Приведем к ПНФ следующую формулу:

xP(x) → x( yD(y) & L(x, y)) = ←xP(x) x( yD(y) & L(x, y)) = = x←P(x) x( yD(y) & L(x, y)) = x←P(x) z( yD(y) & L(z, y)) =

=x(←P(x) z( yD(y) & L(z, y))) =

=x( z( yD(y) & L(z, y)) ←P(x)) =

=x z( vD(v) & L(z, y)) ←P(x))) =

=x z v((D(v) & L(z, y)) ←P(x))) =

=x z v((D(v) ←P(x)) & (L(z, y)) ←P(x))).

2. Рассмотрим посылки примера 12.1.

x(P(x) & y(D(y) → L(x, y))) = x(P(x) & y(←D(y) L(x, y))) =

=x( y(←D(y) L(x, y)) & P(x)) =

=x y((←D(y) L(x, y)) & P(x)).

x(P(x) → y(Q(y) → ←L(x, y))) = x(←P(x) y(←Q(y) ←L(x, y))) =

=x( y(←Q(y) ←L(x, y)) ←P(x)) =

=x y(←Q(y) ←L(x, y) ←P(x)).

13.3.Скулемовские стандартные формы

Определение 13.2. Предваренная нормальная форма, содержащая только кванторы всеобщности, называется скулемовской стандартной формой (ССФ).

Процедура приведения ПНФ к скулемовской форме заключа- ется в элиминации (удалении) кванторов существования.

Пусть формула A находится в предваренной нормальной форме (Q1x1)...(Qnxn)M, где M есть конъюнктивная нормальная форма. Если квантор существования – первый слева квантор в префиксе: ( x1)(Q2x2)...(...(Qnxn)M, то его можно элиминировать на основании правила экзистенциальной конкретизации. Выберем константу c, отличную от других констант, входящих в M, заменим все вхождения x1, встречающиеся в M, на с, и вычеркнем квантор x1 из префикса.

Если же перед квантором существования стоит квантор всеобщности, например, x yM, то переменная y попадает в область действия квантора всеобщности, и выражение x y (для каждого x существует y) означает наличие некоторой функциональной зависимости y = f(x). Если квантору существования предшествует несколько кванторов всеобщности, то функция зависит от всех переменных, по которым навешены эти кванторы. В общем случае, если Qs1, …, Qsm — список всех кванторов всеобщности, встречающихся левее xr, 1 ≤ s1 < s2 < ... < sm < r, мы выберем m-местный функциональный символ f, отличный от других функциональных

символов, заменим все xr â M íà f(õs1, …, õsm) и вычеркнем xr из префикса. Затем весь этот процесс применим для всех кванторов

существования в префиксе; последняя из полученных формул есть

скулемовская стандартная форма — для краткости, стандартная форма (ССФ) формулы A. Функции, используемые для замены переменных квантора существования, называются скулемовскими функциями (константы есть нульместные функции).

Пример. Получим стандартную форму формулы A =

=x y z u v wP(x, y, z, u, v, w). В этой формуле левее x нет никаких кванторов всеобщности, левее u стоят y и z, а левееw стоят y, z и v. Следовательно, мы заменим переменную x на константу a, переменную u — на двуместную функцию f(y, z), переменную w — на трехместную функцию g(y, z, v). Таким образом, мы получаем следующую стандартную форму формулы A: S =

=y z v P(a, y, z, f(y, z), v, g(y, z, v)).

Для рассмотренных выше посылок из примера 12.1 ССФ имеет вид:x y((←D(y) L(x, y)) & P(x)) y((←D(y) L(à, y)) & P(à)),x y(←Q(y) ←L(x, y) ←P(x)).

Если предваренная нормальная форма эквивалентна исходной формуле, то скулемовская стандартная форма формулы A, вообще говоря, не эквивалентна ей. Например, пусть A = xP(x) и S = P(a) есть стандартная форма формулы A. Пусть I есть следующая интерпретация: область D = {a, b}, P(a) = F, P(b) = T. Тогда A истинна в I, но S ложна в I. Таким образом, A не эквивалентна S. Однако, если P(a) = F, P(b) = F, то |A| = F, и S = P(a) также принимает значение F для любого a. Таким образом, A ≡ S в том и только том случае, если A противоречива. Докажем, что это действительно так.

Теорема 13.2. Пусть S — стандартная форма формулы A. Тогда A противоречива в том и только том случае, когда S противоречива.

Доказательство. Пусть формула A находится в ПНФ, т.е.

A = (Q1x1) ... ... (Qnxn)M[x1, ..., xn]. (Запись M[x1, ..., xn] означает, что матрица M содержит переменные x1,..., xn). Пусть Qr — первый слева

квантор существования. Пусть A1 = ( x1) ... ( xr–1)(Qr+1xr+1)…

...(Qnxn)M[x1,..., xr–1, f(x1,..., xr–1), xr+1,…, xn], где f — скулемовская функция, соответствующая xr, 1 ≤ r ≤ n. Мы хотим показать, что A

противоречива тогда и только тогда, когда A1 противоречива. Предположим, что A противоречива. Если A1 непротиворечива, то существует такая интерпретация I, что A1 истинна в I, т.е. для всех x1,..., xr–1 существует по крайней мере один элемент f(x1,..., xr–1), äëÿ

которого (Qr+1xr+1) ... (Qnxn)M[x1,..., xr–1, f(x1,..., xr–1), xr+1,..., xn] истинна в I. Таким образом, A истинна в I, что противоречит предпо-

ложению, что A противоречива. Следовательно, A1 должна быть противоречива. С другой стороны, предположим, что A1 противоре- чива. Если A непротиворечива, то существует такая интерпретация I на области D, что A истинна в I, т.е. для всех x1,…, xr–1 существует

такой элемент xr, ÷òî (Qr+1xr+1) ... (Qnxn)M[x1,..., xr–1, f(x1,..., xr–1), xr+1,..., xn] истинна в I. Расширим интерпретацию I, включив в нее

функцию f(x1,..., xr–1) = xr, которая отображает (x1,..., xr–1) íà xr äëÿ âñåõ x1, ..., xr–1 в D, Обозначим это расширение I′. Тогда для всех

x1,..., xr–1 (Qr+1xr+1) ... (Qnxn)Ì[x1,..., xr–1, f(x1,..., xr–1), xr+1,..., xn] истинна в I′, ò.å. A1 истинна в I', что противоречит предположению, что A1

противоречива. Следовательно, A должна быть противоречивой. Предположим теперь, что в A имеется m кванторов существования. Пусть A0 = A. Пусть Ak получается из Ak–1 заменой первого квантора существования в Ak–1 скулемовской функцией, k = 1, ..., m. Тогда стандартная форма S = Am. Используя те же рассуждения, что были даны выше, мы можем показать, что Ak–1 противоречива тогда и только тогда, когда Ak противоречива при k = 1,..., m. Следовательно, A противоречива тогда и только тогда, когда S противоречива, что и требовалось доказать.

Определение 13.3. Предикатные буквы будем называть литерами. Дизъюнкция литер называется дизъюнктом, или клаузой (clause) (иногда — клозом). Однолитерный дизъюнкт называется единичным дизъюнктом. Когда дизъюнкт не содержит никаких литер, его называют пустым дизъюнктом. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен. Пустой дизъюнкт обозначается символом .

Пусть S — стандартная форма формулы A. Матрица формулы, представленной в ССФ, находится в конъюнктивной нормальной форме, т.е. в виде конъюнкции дизъюнктов. Будем представлять ССФ формулы A множеством дизъюнктов, где каждая переменная

считается управляемой квантором всеобщности. Множество дизъюнктов – это просто другая форма представления стандартной формы формулы A, поэтому в дальнейшем будем обозначать его так же, как и ССФ — символом S. Считаем, что множество дизъюнктов S есть конъюнкция всех дизъюнктов из S. Например, ССФ посылки из примера 12.1: y((←D(y) L(а, y)) & P(а)) может быть представлена множеством дизъюнктов: S = {←D(y) L(à, y), P(à)}.

Далее, если мы имеем A = A1 & ... & An, мы можем отдельно получить множества дизъюнктов Si, i = 1, …, n, где каждое Si представляет стандартную форму Ai. Затем пусть S = S1 ... Sn. Тогда A противоречива тогда и только тогда, когда S противоречиво. Говорят, что множество дизъюнктов невыполнимо, если соответствующая стандартная форма противоречива, и выполнимо в противном случае.

13.4. Эрбрановский универсум множества дизъюнктов

По определению, множество дизъюнктов невыполнимо тогда и только тогда, когда оно ложно при всех интерпретациях на всех областях. Так как невозможно рассматривать все интерпретации на всех областях, было бы удобно, если бы мы могли фиксировать одну такую специальную область H, что S невыполнимо тогда и только тогда, когда S ложно при всех интерпретациях на этой области. Эрбран показал, что такая область существует. Ее называют эрбрановским универсумом множества дизъюнктов S и определяют следующим образом.

Определение 13.4. Пусть H0 — множество констант, встреча- ющихся в S. Если никакая константа не встречается в S, то H0 состоит из одной произвольной константы, например, H0 = {a}. Для i = 1, 2, ... пусть Hi+1 есть объединение Hi и множества всех термов вида fn(t1, ..., tn) (при всех n) для всех функций fn, встречающихся в S, где tj (j = 1, ..., n) принадлежит Hi. Тогда каждое Hi называется множеством констант i-го уровня для S

è H∞ называется эрбрановским универсумом для S.

Примеры.

1. Пусть S1 = {P(a), ←P(x) P(f(x))}. Тогда H0 = {a};

H1 = {a, f(a)};

H2 = {a, f(a), f(f(a))};

……………………………..................

H∞ = {a, f(a), f(f(a)), f(f(f(a))),...}.

2. Пусть S2 = {P(x) Q(x), ←R(z), R(y) ←Q(y)}. Так как не существует никаких констант в S, положим H0 = {a}. Поскольку не

существует никаких функциональных символов в S, то H = H0 = = H1 = ... = {a}.

Определение 13.5. Пусть S есть множество дизъюнктов. Тогда множество атомов вида Pn(t1,..., tn) для всех n-местных предикатов Pn, встречающихся в S, где t1,..., tn — элементы эрбрановского универсума S, называется множеством атомов множества S, или эрбрановским базисом S.

Пример. Эрбрановский базис множества дизъюнктов S1 = {P(a), ←P(x) P(f(x))}:

À = {P(a), P(f(a)), P(f(f(a)), P(f(f(f(a))), …}.

Эрбрановский базис множества дизъюнктов S2 = {P(x) Q(x), R(z)←Q(x)}:

À = {P(a), Q(a), R(a)}.

Определение 13.6. Основной пример дизъюнкта C множества дизъюнктов S есть дизъюнкт, полученный заменой переменных в C на элементы эрбрановского универсума S.

Пример. Пусть S = {P(x), Q(f(y)) R(y)}, C = P(x) — дизъюнкт в S и H = {a, f(a), f(f(a)), ...} — эрбрановский универсум S. Тогда P(a), P(f(a)), P(f(f(a))) есть основные примеры C.

Определение 13.7. Пусть S — множество дизъюнктов, H — эрбрановский универсум S и I — интерпретация S над H. Говорят, что I есть H-интерпретация множества S, если она удовлетворяет следующим условиям:

1.I отображает все константы из S в самих себя;

2.пусть f есть n-местный функциональный символ и h1,..., hn — элементы H. В I через f обозначается функция, которая отображает (h1,..., hn) (элемент из Hn) â f(h1,..., hn) ( элемент из H).

При этом не возникает никаких ограничений при придании значения любому n-местному предикатному символу в S. Пусть A = {A1, A2,..., An,...} — эрбрановский базис множества S. H-интерпретацию I удобно представлять в виде: I = {m1, m2,..., mn,...}, ãäå mj åñòü Aj èëè ←Aj для j = 1, 2, ... Смысл этого множества в том, что если mj åñòü Aj, то атому Aj присвоено значение «истинно», в противном случае — значение «ложно».

Пример. Рассмотрим множество S = {P(x) Q(x), R(f(y))}. Эрбрановский универсум H для S есть H = {a, f(a), f(f(a)), ...}. В S входят три предикатных символа: P, Q и R. Следовательно, эрбрановский базис S есть

A = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)),...}.

Некоторые H интерпретации множества S:

I1 = {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)),...},

I2 = {¬P(a), ¬Q(a), ¬R(a), ¬P(f(a)), ¬Q(f(a)), ¬R(f(a)), ...}, I3 = {P(a), Q(a), ¬R(a), P(f(a)), Q(f(a)), ¬R(f(a)),...}, è ò.ä.

Можно показать, что для любой интерпретации найдется соответствующая ей H-интерпретация.

Теорема 13.3. Множество дизъюнктов S невыполнимо тогда и только тогда, когда S ложно при всех H-интерпретациях в S.

Доказательство. Первая половина теоремы очевидна, так как по определению S невыполнимо тогда и только тогда, когда S ложно при всех интерпретациях на этой области. Чтобы доказать вторую половину теоремы, предположим, что S ложно при всех H-интерпре- тациях в S. Положим, что S выполнимо. Тогда существует такая интерпретация I на некоторой области D, что S истинно при I. Пусть I* есть H-интерпретация, соответствующая I. Тогда S истинно при I*. Это противоречит предположению, что S ложно при всех H-интерпретациях в S. Следовательно, S должно быть невыполнимо, что и требовалось доказать.

Таким образом, мы достигли цели, установленной в начале этого параграфа, т.е. нам необходимо рассматривать только интерпретации над эрбрановским универсумом, точнее, H-интерпретации, для проверки того, выполнимо множество дизъюнктов или нет. Поэтому впредь, упоминая интерпретацию, мы будем иметь в виду H-ин- терпретацию.

H-интерпретации можно представлять в виде семантических деревьев. Как будет видно впоследствии, нахождение доказательства невыполнимости множества дизъюнктов эквивалентно построению семантического дерева. Без потери общности можно рассматривать только бинарные семантические деревья.

Определение 13.8. Если A — атом, то говорят, что две литеры A и ¬A контрарны друг другу, и множество {A, ¬A} называют

контрарной парой.

Отметим, что дизъюнкт есть тавтология, если он содержит контрарную пару, так как A ¬A ≡ T, и множество дизъюнктов невыполнимо, если оно содержит два единичных контрарных дизъюнкта, так как A & ¬A ≡ F.

Определение 13.9. Пусть S — множество дизъюнктов и A — его эрбрановский базис. Семантическое (бинарное) дерево для S есть растущее вниз дерево T, в котором каждому ребру приписан атом из A или его отрицание таким образом, что из каждого

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

Обозначим через I(N) объединение всех литер, приписанных ребрам ветви, ведущей к узлу N. Тогда для каждого узла N I(N) не содержит контрарных пар.

Определение 13.10. Пусть A = {A1, A2, ..., An, ...} — эрбрановский базис множества S. Говорят, что семантическое дерево для S будет полным тогда и только тогда, когда для каждого i (i = 1, 2,...) и каждого конечного узла N семантического дерева (т. е. для узла, из которого не выходит никаких ребер) I(N) содержит либо Ai ëèáî ¬Ai. Таким образом, в полномсемантическом дереве каждая ветвь соответствует одной H-интерпретации.

Когда эрбрановский базис множества S бесконечен, всякое полное семантическое дерево для S будет тоже бесконечно. Полное семантическое дерево для S соответствует исчерпывающему перебору всех возможных интерпретаций для S. Если S невыполнимо, то S не сможет быть истинным в каждой из этих интерпретаций. Таким образом, мы можем остановить рост дерева из узла N, если I(N) опровергает S. Это порождает следующие определения.

Определение 13.11. Узел N называется опровергающим, если I(N) опровергает некоторый основной пример дизъюнкта в S, но для любого предшествующего узла N′ I(N′) не опровергает никакого основного примера дизъюнкта в S.

Определение 13.12. Говорят, что семантическое дерево T замкнуто тогда и только тогда, когда каждая ветвь T оканчивается опровергающим узлом.

Примеры.

1. Пусть S = {P, Q R, ¬P ¬Q, ¬P ¬R}.

Эрбрановский базис множества S есть A = {P, Q, R},

невыполнимое множество основных примеров: {¬P,

¬Q ¬R, P Q, P R}. Семантическое дерево для S

показано на рис. 13.1, замкнутое поддерево выделено более жирными линиями.

2. Пусть S = {P(x), ¬P(x)Q(f(x)), ¬Q(f(a))}. Эрбра-

новский базис A = {P(a), Q(a), P(f(a)), Q(f(a)),…}. Невыполнимое множество основных примеров: {¬P(a), P(a) ¬Q(f(a)), Q(f(a))}.

Рис. 13.2. Бесконечное семантическое дерево.

Семантическое дерево для S будет бесконечным (см. рис. 13.2); замкнутое поддерево выделено более жирными линиями.

13.5. Теорема Эрбрана

Процедура Эрбрана основывается на теореме 13.3, поэтому для проверки невыполнимости множества дизъюнктов S рассматриваются только интерпретации над эрбрановским универсумом. Если S ложно при всех интерпретациях над эрбрановским универсумом S, то можно заключить, что S невыполнимо. Так как обычно существует много, возможно, бесконечное число таких интерпретаций, они выбираются некоторым систематическим способом с использованием семантических деревьев.

Теорема 13.4 (теорема Эрбрана, вариант 1). Множество дизъюнктов S невыполнимо тогда и только тогда, когда любому полному семантическому дереву S соответствует конечное замкнутое семантическое дерево.

Доказательство. Допустим, что S невыполнимо. Пусть Т — полное семантическое дерево для S. Пусть для каждой ветви B дерева Т IB — множество всех литер, приписанных всем ребрам ветви B. Тогда IB есть интерпретация для S. Так как S невыполнимо, то IB должна опровергать основной пример С′ дизъюнкта С в S. Однако, так как С′ конечно, то на В должен существовать опровергающий узел NB (лежащий на конечном расстоянии от корня). Поскольку каждая ветвь Т имеет опровергающий узел, то существует замкнутое семантическое дерево Т′ для S. Далее, так как из каждого узла в Т′ выходит только конечное число ребер, то Т′ должно быть конечным (т.е. число узлов в Т′ конечно), иначе мы могли бы найти бесконечную ветвь, не содержащую опровергающих узлов. Таким образом, доказательство первой половины теоремы завершено.

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

S невыполнимо. Это завершает доказательство второй половины теоремы.

Теорема 13.5 (теорема Эрбрана, вариант 2). Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует конечное невыполнимое множество S′ основных примеров дизъюнктов S.

Доказательство. Предположим, что S невыполнимо. Пусть Т — полное семантическое дерево для S. Тогда по теореме Эрбрана (вариант 1) существует конечное замкнутое семантическое дерево Т′, соответствующее Т. Пусть S′ — множество всех основных примеров дизъюнктов, которые опровергаются во всех опровергающих узлах Т′. S′ конечно, так как в Т′ содержится конечное число опровергающих узлов. Так как S′ ложно в каждой интерпретации S′, то S′ невыполнимо.

Предположим, что существует конечное невыполнимое множество S′ основных примеров дизъюнктов в S. Так как каждая интерпретация I для S содержит интерпретацию I′ множества S′ и I′ опровергает S′, то I должна также опровергать S′. Однако S′ опровергается в каждой интерпретации I′. Следовательно, S′ опровергается в каждой интерпретации I множества S. Поэтому S опровергается в каждой интерпретации множества S′, значит, S невыполнимо.

Пример. Пусть S = {¬P(x) Q(f(x), x), P(g(b)), ¬Q(y, z)}. Это множество невыполнимо. Одно из невыполнимых множеств основных примеров дизъюнктов множества S есть S′ = = {¬P(g(b)) Q(f(g(b)), g(b)), P(g(b)), ¬Q(f(g(b)), g(b))}.

13.6. Метод резолюций

Далеко не всегда можно легко найти невыполнимое множество основных примеров дизъюнктов. Трудности заключаются в порождении основныхпримеровдизъюнктовипоискеопровергающихинтерпретаций. Поскольку множество дизъюнктов представляет собой конъюнктивную нормальнуюформу,тозадачапроверкиневыполнимостиэтогомножества эквивалентна задаче проверки ложности конъюнктивной нормальной формы,аэтозадачаэкспоненциальнойсложности.Послемногочисленных поисков более эффективных процедур, Дж. Робинсоном был предложен метод, названный методом резолюций.

Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество S пустой дизъюнкт . Если S содержит , то множество S невыполнимо, если нет, то надо проверить, может ли он быть получен из данного множества дизъюнктов. Иными словами, необходимо найти множество основных примеров, опровергающих исходное множество дизъюнктов. Эта процедура основана на правиле резолюций.

Правило резолюций Робинсона. Если для любых двух дизъюнктов С1 è Ñ2 существует литера L1 C1 и контрарная ей литера L2 C2 (L2 = ¬L1), то вычеркнув L1 èç Ñ1 è L2 èç Ñ2 и построив дизъюнкт из оставшихся литер, получим резольвенту С1 è Ñ2 :

C'1 C'2, ãäå C'1 = C1\L1, C'2 = C2\L2.

Теорема 13.6. Резольвента С есть логическое следование дизъюнктов С1 è Ñ2, содержащих контрарные литеры L и ¬L:

L Ñ′1, ¬L1 Ñ′2 |= C'1 C'2.

Доказательство. Предположим, что |L С′1| = T, |¬L Ñ′2| = T,

|C'1 C'2| = F. Тогда |C'1| = F, |C'2| = F. Åñëè |L Ñ′1| = T, òî |L | = T, íî |¬L Ñ′2| = T, следовательно, |L | = F. Полученное противоречие

доказывает теорему.

Правило резолюций является обобщением многих известных нам правил вывода. Например, правило силлогизма: A → B, B → C |= A → C может быть переписано в виде: ¬A B, ¬B C |= ¬A C, что соответствует правилу резолюций. Правило МР: A, A → B |= B может быть переписано в виде: A ¬A B |= B, что также соответствует правилу резолюций. Наконец, закон противоречия A & ¬A ≡ F равнозначен правилу: A, ¬A |= , согласно которому резольвента двух контрарных однолитерных дизъюнктов есть пустой дизъюнкт.

Определение 13.13. Резолютивный вывод из множества дизъюнктов S есть последовательность C1, C2,..., Ck, такая, что каждое Ci либо принадлежит S, либо является резольвентой предшествующих Ci. Если последний дизъюнкт Ck = , то множество дизъюнктов S является невыполнимым, а весь вывод называется опровержением S. Если Ck не является пустым дизъюнктом и дальнейшее применение правила резолюций невозможно, то множество S является выполнимым.

Пример. Рассмотрим пример 10.1. (см. главу 10). Необходимо проверить логическое следование в логике высказываний: P → S, S → R, P |= R. Составим множество дизъюнктов S, для чего каждую формулу приведем к КНФ, а от заключения R возьмем отрицание. Получим:

1.¬P S

2.¬S R

3.P

4.¬R

Правило резолюций — очень мощное средство логического доказательства. Можно показать [Чень, Ли, 1983] полноту метода резолюций, т.е. доказать, что множество дизъюнктов S невыполнимо тогда и тогда, когда существует резолютивный вывод пустого дизъюнкта из S.

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

Применение метода резолюций в логике предикатов усложняется тем, что дизъюнкты содержат термы, которые могут не совпадать в двух одинаковых литерах. Например, С1 = P(x) Q(x), C2 = ¬P(f(a)) V(a). В этих дизъюнктах нет контрарных литер, однако, если мы подставим f(a) вместо х в С1, то получим

Ñ1′ = P(f(a)) Q(f(a)); теперь литеры P(f(a)) и ¬P(f(a)) будут уже контрарны. Получим резольвенту Q(f(a)) V(a).

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

Определение 13.14. Подстановка — это конечное множество вида {t1/v1,…, tn/vn}, ãäå vi — переменная, ti — терм, отличный от vi, è âñå vi различны.

Определение 13.15. Пусть θ= {t1/v1,…, tn/vn} и E — выражение. Тогда Eθ— выражение, полученное из E заменой всех вхождений переменных vi (1 ≤ i ≤ n) на термы ti.

Определение 13.16. Пусть θ= {t1/v1,…, tn/vn}, λ= {u1/y1,…, uk/yk} – подстановки. Композиция подстановок θ°λполучается из множества {t1λ/v1,…, tnλ/vn, u1/y1,…, uk/yk} вычеркиванием всех элементов tjλ/vj, для которых tjλ= vj (тождественная подстановка), и всех элементов ui/yi, таких, что yi {v1,…, vn}.

Пример. Пусть θ= {t1/v1, t2/v2 } = {f(y)/x, z/y}, λ= {u1/y1, u2/y2, u3/y3} = {a/x, b/y, y/z}. Тогда θ°λ= {t1λ/v1, t2λ/v2 , u1/y1, u2/y2, u3/y3} = = {f(b)/x, y/y, a/x, b/y, y/z}. Òàê êàê t2λ/x2 = y/y, то y/y должно

быть вычеркнуто из множества θ°λ. Элементы a/x, b/y также должны быть вычеркнуты, так как подстановки для x и y уже определены.

Âрезультате получаем: θ°λ= {f(b)/x, y/z}.

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

Определение 13.17. Подстановка θназывается унификатором множества {E1,…, Em} тогда и только тогда, когда E1θ = …= Emθ. Множество {E1,…, Em} называется унифицируемым, если для него существует унификатор. Унификатор σдля множества выражений {E1,…, Em} называется наиболее общим унификатором, если для каждого унификатора θэтого множества существует такая подстановка λ, что θ = σ°λ.

Например, для двух дизъюнктов {P(a, y), P(x, f(b)} подстановка {a/x, f(b)/y} является наиболее общим унификатором.

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

Определение 13.18. Если две или более литер (с одинаковым знаком) дизъюнкта С имеют наиболее общий унификатор σ, òî Cσ называется склейкой С. Если Cσ — единичный дизъюнкт, то склейка называется единичной склейкой.

Пример. Пусть С = P(x) P(f(y)) ←Q(x). Тогда первая и вторая литеры имеют наиболее общий унификатор σ = {f(y)/x}. Следовательно, Cσ = P(f(y)) ←Q(f(y)) есть склейка С.

Определение 13.19. Пусть C1 è C2 — два дизъюнкта (называемые дизъюнктами-посылками), которые не имеют никаких общих переменных. Пусть L1 è ←L2 — две литеры в C1 è C2 соответственно. Если L1 è L2 имеют наиболее общий унификатор σ, òî

дизъюнкт (C1σ \ L1σ) (C2σ \ L2σ) называется (бинарной)

резольвентой C1 è C2. Литеры L1 è L2 называются отрезаемыми литерами.

Определение 13.20. Резольвентой дизъюнктов-посылок C1 è C2 является одна из следующих резольвент:

1)бинарная резольвента C1 è C2;

2)бинарная резольвента C1 и склейки C2;

3)бинарная резольвента C2 и склейки C1;

4)бинарная резольвента склейки C1 и склейки C2.

Пример. Пусть C1 = P(x) P(f(y)) R(g(y)) è C2 = ←P(f(g(a)))Q(b). Склейка C1 åñòü Ñ1' = P(f(y)) R(g(y)). Выполним подстановку g(a)/y. Бинарная резольвента С1' è C2 åñòü R(g(g(a))) Q(b).

Следовательно, R(g(g(a))) Q(b) есть резольвента C1 è C2.

13.8. Примеры использования метода резолюций

Пример 13.1. Завершим рассмотрение примера 12.1 главы 12. ССФ посылок мы получили в 13.3:

y((←D(y) L(à, y)) & P(à)), x y(←Q(y) ←L(x, y) ←P(x)).

Найдем отрицание от заключения G и приведем его к ПНФ; получим:

← y(D(y) → ←Q(y)) = y←(←D(y) ←Q(y)) = y(D(y) & Q(y)). Элиминируем квантор и получим ССФ: D(b) & Q(b). Построим резолютивный вывод:

1.←D(y) L(à, y)

2.P(à)

3.←Q(y) ←L(x, y) ←P(x)

4.D(b)

5.Q(b)

Пример 13.2. Посылка: «Каждый, кто хранит деньги, получает проценты». Заключение: «Если не существует процентов, то никто не хранит денег». Пусть S(x, y): «x хранит y», M(x): «x есть деньги», I(x): «x есть проценты» и E(x, y): «x получает y». Тогда посылка

записывается в виде: x( y(S(x, y) & M(y)) → y(I(y) & E(x, y))), а заключение: ←xI(x) → x y(S(x, y) → ←M(y)).

Приведем посылку к ССФ:

x( y(S(x, y) & M(y)) → y(I(y) & E(x, y))) =

=x(←y(S(x, y) & M(y)) y(I(y) & E(x, y))) =

=x( y(←S(x, y) ←M(y)) y(I(y) & E(x, y))) =

=x( z(I(z) & E(x, z))) y(←S(x, y) ←M(y)) =

=x z((I(z) & E(x, z)) y(←S(x, y) ←M(y))) =

=x z y ((I(z) & E(x, z)) (←S(x, y) ←M(y))) =

=x z y ((←S(x, y) ←M(y) I(z)) & (←S(x, y) ←M(y) E(x, z))). ССФ посылки:

x y ((←S(x, y) ←M(y) I(f(x)) & (←S(x, y) ←M(y) E(x, f(x))). В результате получим дизъюнкты:

1.←S(x, y) ←M(y) I(f(x)),

2.←S(x, y) ←M(y) E(x, f(x)).

Возьмем отрицание от заключения и приведем к ПНФ: ←(←xI(x) → x y(S(x, y) → ←M(y))) =

=←(←←xI(x) x y(←S(x, y) ←M(y))) =

=x←I(x) & ← x y(←S(x, y) ←M(y))) =

=z←I(z) & x y(S(x, y) & M(y)).

Поскольку полученная формула представляет собой конъюнкцию двух формул в ПНФ, можно каждую из них приводить к ССФ отдельно: z←I(z) & (S(a, b) & M(b)).

Из отрицания заключения получили дизъюнкты:

3.←I(z),

4.S(a, b),

5.M(b).

Логическое следование доказано.

Пример 13.3. Посылка: «Студенты есть граждане». Заключе- ние: «Голоса студентов есть голоса граждан.» Пусть S(x): «x — студент», C(x): «x — гражданин» и V(x, y): «x есть голос y». Тогда посылка и заключение запишутся следующим образом:

Стандартная форма посылки есть y(←S(y) C(y)). Отрицание заключения приведем к ССФ:

←( x( y(S(y) & V(x, y)) → z(C(z) & V(x, z)))) =

=←( x( y(←S(y) ←V(x, y)) z(C(z) & V(x, z)))) =

=←( x y z(←S(y) ←V(x, y) (C(z) & V(x, z)))) =

=x y z((S(y) & V(x, y)) & (←C(z) ←V(x, z)));

ÑÑÔ: z((S(b) & V(a, b)) & (←C(z) ←V(a, z))),

Запишем множество дизъюнктов и построим резолютивный вывод:

1.←S(y) C(y).

2.S(b),

3.V(a, b),

4.←C(z) ←V(a, z).

Пример 13.4. Проверим логичность утверждения Лосева А. Ф.1: «Вера в сущности своей и есть подлинное знание, и эти две сферы не только не разъединимы, но даже неразличимы».

Доказательство Лосева заключается в следующем. «Верующий верит в нечто. Вера свой предмет ясно отличает

от всякого другого предмета. Тогда этот предмет определен. Но если он определен, он обладает признаками, отличающими его от всякого другого. Это значит, что мы знаем этот предмет. Мы знаем вещь, если по признакам можем отличить ее от всякого другого. Следовательно, вера и есть знание.»

1 А. Ф. Лосев. Диалектика мифа. В кн. «Из ранних произведений». М.: Правда, 1990. (стр. 497).