Математическая логика и теория алгоритмов (120

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

13)xB(x) → C x(B(x) → C);

14)xB(x) → C x(B(x) → C).

Если формула A может содержать свободную переменную x, то

15)xA(x) xB(x) x(A(x) B(x));

16)xA(x) xB(x) x(A(x) B(x));

17)xA(x) xB(x) x y(A(x) B(y));

18)xA(x) xB(x) x y(A(x) B(y)).

Может показаться, что утверждение 17 следует записать какxA(x) xB(x) x(A(x) B(x)). Чтобы убедиться, что это неверно, рассмотрим следующую интерпретацию: область интерпретации – непустое множество D, в котором есть такие непустые подмножества DA и DB, что DA ∩ DB = . Тогда формулаxA(x) xB(x) истинна, а формула x(A(x) B(x)) ложна.

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

Запись математических утверждений. Язык логики предикатов удобен для записи математических утверждений. Он дает возможность кратко выражать логические связи между понятиями, формулировать определения, теоремы и доказательства.

Пример 2.5. Функция называется четной, если область еe определения симметрична относительно начала координат и для каждого элемента x из области определения M выполняется равенство f(x) = f(−x).

Это определение можно выразить, используя ЯП, следующим образом: x M((−x M) (f(x) = f(−x))), здесь применен предикат P(x) = (−x M) (f(x) = f(−x)).

Математические утверждения часто формулируются в виде условных предложений типа: «Любой элемент x из множества M, который обладает свойством P(x), также обладает свойством Q(x)». На языке логики предикатов это соответствует формуле

x M(P(x) → Q(x)).

Ложность такого утверждения следует из истинности его отрицания:

¬( x M(P(x) → Q(x))) ≡ x M¬(P(x) → Q(x)) ≡

22

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

≡ x M¬(¬P(x) Q(x)) ≡ x M(P(x) ¬Q(x)).

Таким образом, для доказательства ложности приведенного утверждения достаточно показать, что существует элемент x, который обладает свойством P(x), но не обладает свойством Q(x).

Пример 2.6. Пусть M множество функций f, определенных в окрестности точки x0, P(f) означает, что функция дифференцируема в точке x0, Q(f) означает, что функция непрерывна в точке x0.

Рассмотрим утверждение: «Функция, непрерывная в точке x0, дифференцируема в этой точке: f M(Q(f) → P(f))». Покажем, что оно ложно. Как объяснялось выше, для этого достаточно доказать истинность утверждения f M(Q(f)¬P(f)) (т. е. существует функция непрерывная, но не дифференцируемая в точке x0). В качестве такой функции можно взять функцию f(x) = |x| в окрестности точки x0 = 0.

Любому утверждению вида

а) x M(P(x) → Q(x)) — прямое утверждение;

можно поставить в соответствие еще три логические схемыутверждения:

б) x M(Q(x) → P(x)) — обратное утверждение;

в) x M(¬P(x) → ¬Q(x)) — противоположное утверждение;

г) x M(¬Q(x) → ¬P(x)) — обратное к противоположному утверждение.

Прямое и обратное утверждения в общем случае не равносильны. Но прямое и обратное к противоположному, а также обратное и противоположное утверждения равносильны всегда:

x M(P(x) → Q(x)) ≡ x M(¬P(x) Q(x)) ≡

≡ x M(¬¬Q(x) ¬P(x)) ≡ x M(¬Q(x) → ¬P(x)).

Таким образом,

(а) ≡ (г).

Пример 2.7. Прямое утверждение: f M(P(f) → Q(f)), любая функция, дифференцируемая в точке x0, непрерывна в этой точке (верно).

Обратное утверждение: f M(Q(f) → P(f)), любая функция, непрерывная в точке x0, дифференцируема в этой точке (неверно, f = |x| в точке x0 = 0).

23

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

Противоположное утверждение: f M(¬P(f) → ¬Q(f)), любая функция, не дифференцируемая в точке x0, разрывна в этой точке (неверно, f = |x| в точке x0 = 0).

Обратное противоположному утверждение: f M(¬Q(f) → → ¬P(f)), любая функция, разрывная в точке x0, недифференцируема в этой точке (верно).

2.3. Метод резолюций в языке предикатов

Доказать общезначимость формулы оценкой при всех возможных интерпретациях практически невозможно. В 1936 г. американский математик А. Чeрч¨ доказал, что не существует общей разрешающей процедуры, алгоритма, проверяющего общезначимость формул в логике предикатов. Тем не менее существует метод поиска доказательства, который может подтвердить, что формула общезначима, если она на самом деле общезначима, — метод резолюций. Если же данная формула не общезначима, то указанный метод поиска, вообще говоря, не даeт результата (алгоритм работает вечно). Этот метод будет изложен далее. Метод уже применялся в ЯВ; как мы увидим, его реализация в случае ЯП существенно сложнее.

Предваренная нормальная форма. Предваренной формой называется формула вида

Q1x1Q2x2 ...QnxnM,

где Qi — либо квантор , либо квантор ; M — формула, не содержащая кванторов. Если M есть дизъюнкция атомарных формул (возможно, с отрицаниями), то говорят, что формула имеет предваренную ДНФ; аналогично определяется предваренная КНФ.

Любую формулу логики предикатов можно привести к предваренной нормальной форме следующим образом:

а) сделать формулу чистой, если она не была таковой, переименовав связанные переменные;

б) исключить связки →, ↔, выразив их через , , ¬; в) перенести все отрицания ¬ к атомарным формулам, исполь-

зовав эквивалентности 3, 4; г) перенести все кванторы влево, использовав эквивалентно-

сти 7—18.

24

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

Пример 2.8. Пусть α = x yP2(x,y) ¬( x yQ2(x,y)).

Перенесем ¬ к атомарной формуле, используя эквивалентности 3, 4; получим x yP2(x,y) x(¬yQ2(x,y)), x yP2(x,y)

x y¬Q2(x,y). Перенесем x влево, используя эквивалентность 15, получим x( yP2(x,y) y¬Q2(x,y)); перенесем (на второе место после x) квантор , используя эквивалентность 17, получим

x y z(P2(x,y) ¬Q2(x,z)).

Пример 2.9. Пусть α = xP1(x) xQ1(x). Переименуем x в подформуле xQ1(x), так как одна и та же переменная входит в разные кванторные приставки; получим xP1(x) yQ1(y).

Перенесем кванторы влево, используя эквивалентности 7 и 9, получим x(P1(x) yQ1(y)), x y(P1(x) Q1(y)).

Скулемовская форма. Приведение формулы к cкулемовской форме. Пусть имеем формулу α в предваренной КНФ либо ДНФ. Построим новую формулу β, которая не будет содержать кванторов . Процедура перехода от α к β называется скулемовским преобразованием, а сама форма формулы β — скулемовской

(СКНФ). Исключение квантора существования выполняем следующим образом:

а) если формула α начинается с xi, то удаляем эту кванторную приставку, а в оставшейся части заменяем xi константной буквой a, не встречавшейся в α;

б) если формула α начинается с xi1 ... xik xr, то удаляем

xr, а в оставшейся формуле заменяем xr на fk(xi1,...,xik ), где fk – функциональный символ, не встречающийся в α.

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

истинной. Можно взять, например, f1(x) = х + 0,1, что приведет к формуле x(|x − (х + 0,1)| < 0,2); ясно, что она истинна.

25

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

Имея формулу α, мы всегда можем привести еe к предварeнной КНФ и затем к скулемовской предваренной КИФ (СПКНФ). Именно эта форма будет применяться далее.

Логическое следование в языке предиктов. Формула β называется логическим следствием формул α1,..., αn, если в любой интерпретации, в которой истинны α1,..., αn, также истинна β.

В этом случае пишут: α1,..., αn|= β.

Так же как в ЯВ, доказывается, что это логическое следование

где F — формула, ложная в любой интерпретации. Это, в свою

очередь, равносильно тому, что α1 ... αn ¬β = F.

Для проверки утверждения (2.1) запишем формулу α1,...,

αn, ¬β в краткой СПКНФ. Подчеркнeм, что для каждой формулы при исключении кванторов существования используются разные константные и функциональные символы. Пусть D1,...,Dn — все дизъюнкты, входящие в бескванторные части этих СПКНФ. Тогда утверждение (2.1) равносильно формуле

по умолчанию предполагается, что перед Di стоят кванторы всеобщности.

Применение метода резолюций в языке предиктов. Пусть имеем формулы α θ и β ¬θ, где α, β, θ — формулы из ЯП. Тогда, как и в ЯВ, имеем α θ, β ¬θ|= α β. Формула α β есть резолюция формул α θ и β ¬θ. В этом случае пишут α β = res(α θ, β ¬θ). Говорят, что θ и ¬θ — контрарные по

Пусть теперь даны формулы α θ и β σ, обладающие следующим свойством: можно подобрать такую подстановку S1 ( т. е. замену некоторых свободно входящих переменных термами) для первой формулы и такую подстановку S2 для второй, что подформулы θ и σ превратятся в результате этих подстановок в контрарную пару. К формулам, полученным из α θ и β σ указанными

26

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

подстановками, прим´еним описанную выше резолюцию. Получим формулу S1 α S2 β; еe также называют резолюцией формул μ, ρ (можно также назвать резолюцией с предварительными подстановками) и обозначают через res(μ, ρ).

Метод резолюций для проверки соотношения (2.2) используется следующим образом. Предположим, что из дизъюнктов D1,...,Dn можно выбрать пару Di,Dj, к которой применима резолюция (возможно, с предварительными подстановками). Дизъюнкт, полученный как результат резолюции, присоединяется к исходному набору дизъюнктов (если, разумеется, он не совпадает ни с одним из дизъюнктов исходного набора). С полученным (расширенным) набором дизъюнктов поступим аналогичным образом. Повторяя эту процедуру (до тех пор, пока это возможно), приходим к цепочке дизъюнктов, обладающей следующим свойством: каждый элемент цепочки либо принадлежит набору D1,...,Dn, либо получается как резолюция некоторой пары предшествующих дизъюнктов. Такую цепочку называют резолютивной.

Здесь возможен один из следующих трeх исходов.

а) на некотором шаге получаем пустой дизъюнкт F; в этом случае логическое следование (2.2) имеет место (разумеется, на этом шаге процедура построения резолюций прекращается);

б) с некоторого шага мы не получаем новых дизъюнктов, а среди полученных дизъюнктов нет пустого дизъюнкта; в этом случае логическое следование (2.2) не имеет места;

в) описанная процедура длится вечно; в этом случае алгоритм не дает ответа на вопрос о том, имеет ли место логическое следование (2.2).

Таким образом, проверка логического следования α1,...,

..., αn|= β методом резолюций сводится к следующим шагам.

1.Приводим формулы α1,..., αn,¬β к СКНФ и выписываем

все дизъюнкты D1,...,Dn, встречающиеся в бескванторных частях этих СКНФ.

2. По набору D1,...,Dn строим резолютивную цепочку. Если она привела к случаю а), то логическое следование имеет место; в случае б) оно не имеет места; в случае в) вопрос не решeн.

Унификация формул. Вернемся к вопросу о построении резолюции (с предварительными подстановками) для формул α θ и β σ. Предположим, что формулы θ и σ имеют вид соответственно Pk(t1,...,tk) и ¬Pk(s1,...,sk). Задача состоит в подборе

27

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

подстановок, приводящих формулы Pk(t1,...,tk) и Pk(s1,...,sk) к одной и той же формуле (разумеется, такие подстановки не все-

гда существуют). Для решения этой задачи следует просмотреть цепочки (t1,...,tk) и (s1,...,sk) слева направо (терм за термом) до тех пор, пока не обнаружится первое рассогласование (т. е. несовпадение пары термов в формулах). Предположим, что рассогласование состоит в следующем: один из указанных несовпадающих термов есть переменная (например, буква x), а второй — некоторый терм t, не содержащий букву x. В этом случае произведeм

подстановку t|x в обеих формулах Pk(t1,...,tk) и Pk(s1,...,sk). Таким образом, упомянутое «рассогласование» устранено.

Новые формулы «обрабатываем» аналогичным образом. Продолжая эту работу, либо получим одинаковые формулы, либо на некотором шаге рассогласование окажется неустранимым. В пер-

вом случае говорят, что пара Pk(t1,...,tk),Pk(s1,...,sk) унифицирована (результат унификации есть новая формула); во втором

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

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

согласование {g1(x),f1(a)}; оно неустранимо, и, следовательно, эта пара не унифицируема.

Пример 2.16. Выясним, верно ли логическое следствие F1,

1)x y(P1(x) (¬D1(y) L2(x,y))),x = a,P1(a) (¬D1(y)

L2(a,y));

2)x y(¬P1(x) ¬Q1(y) ¬L2(x,y));

3)x(D1(x) Q1(x)),x = b,(D1(b) Q1(b).

Опустив кванторы , выпишем все дизъюнкты, входящие в полученные формулы, и проверим соотношение:

P1(a);(¬D1(y) L2(a,y)));(¬P1(x) ¬Q1(y) ¬L2(x,y)); D1(b);Q1(b)|= F;

D1 = P1(a);

D2 = ¬D1(y) L2(a,y)1;

D3 = ¬P1(x) ¬Q1(y) ¬L2(x,y)1; D4 = D1(b);

D5 = Q1(b).

Построим резолютивную цепочку:

Следовательно, F1,F2|= G.

Так же, как и в ЯВ, следует придерживаться стратегии очищения:

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

б) если появились дизъюнкты, один из которых есть часть другого, то «больший»´ дизъюнкт можно отбросить;

в) если в дизъюнктах встречаются атомарные формулы вида Pk, но нет атомарных формул вида ¬Pk (или наоборот), то все такие дизъюнкты можно удалить.

29

Copyright ОАО «ЦКБ «БИБКОМ» & ООО «Aгентство Kнига-Cервис»

Пример 2.17. Пусть F1 : x y(T2(x,y) (P1(x) → Q1(x))

(¬P1(x) R1(x));

F2 : x(P1(x) S1(x));

G: x(¬T2(x,x) S1(x) R1(x)).

Проверим, имеет ли место логическое следование F1, F2|= G. Имеем:

¬G: x(T2(x,x) (¬S1(x) ¬R1(x)).

Приведем к СПКНФ формулы F1, F2, ¬G:

1)x y(T2(x,y) (¬P1(x) Q1(x)) (¬P1(x) R1(x))), следовательно, x(T2(x,f(x)) (¬P1(x) Q1(x)) (¬P1(x) R1(x)));

2)P1(a) S1(a);

3)x(T2(x,x) (¬S1(x) ¬R1(x))).

Выпишем все дизъюнкты, встречающиеся в этих СПКНФ:

D1 = T2(x,f(x)); D2 = ¬P1(x) Q1(x); D3 = ¬P1(x) R1(x); D4 = T2(x,x); D5 = ¬S1(x) ¬R1(x); D6 = P1(a); D7 = S1(a). Требуется выяснить, верно ли логическое следование D1, D2, D3,

D4, D5, D6, D7|= F.

Удаляем D1 и D4, в них cимволы T входят неконтрарно. Далее получим

D8 = res(D3|x=a,D6) = R1(a); D9 = res(D5|x=a,D8) = ¬S1(a); D10 = res(D7,D9) = F.

Следовательно, F1, F2|= G.

3. ТЕОРИЯ АЛГОРИТМОВ

3.1. Алгоритмы

Задать алгоритм (для решения некоторого набора задач) означает задать конечную цепочку команд, называемую программой. Мы заносим в программу одну из этих задач и выполняем команды последовательно (начиная с первой). Предполагается, что каждая команда выполняется без труда. Если после выполнения некоторой команды работа закончилась (тогда говорят, что программа работает конечное время), полученный на этом шагу результат и будет

30