Сергиевская И.М. МАТЕМАТИЧЕСКАЯ ЛОГИКА и теория алгоритмов

Министерство Российской Федерации по связи и информатизации
Поволжская государственная академия телекоммуникаций и информатики





И.М.Сергиевская




МАТЕМАТИЧЕСКАЯ ЛОГИКА
И ТЕОРИЯ АЛГОРИТМОВ
Учебное пособие

Рекомендовано УМО по образованию в области
телекоммуникаций в качестве учебного пособия
для студентов, обучающихся по направлению
подготовки дипломированных специалистов –
654400 (210400) Телекоммуникации






2004








Содержание.
13 REF _Ref103425366 \h \* MERGEFORMAT 14Введение.15
13 REF _Ref101956579 \h \* MERGEFORMAT 14Глава 1. Высказывания, формулы, тавтологии.15
13 REF _Ref101956630 \h \* MERGEFORMAT 14Отношения логической эквивалентности и логического следствия.15
13 REF _Ref103252321 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103252366 \h \* MERGEFORMAT 14Глава 2. Формальные теории.15
13 REF _Ref100762967 \h \* MERGEFORMAT 14Глава 3. Исчисление высказываний.15
13 REF _Ref100763006 \h \* MERGEFORMAT 14Построение вывода в логике высказываний.15
13 REF _Ref100763075 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref101610008 \h \* MERGEFORMAT 14Глава 4. Метод резолюций в логике высказываний.15
13 REF _Ref101610055 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103423939 \h \* MERGEFORMAT 14Глава 5. Предикаты.15
13 REF _Ref103423996 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103424047 \h \* MERGEFORMAT 14Глава 6. Исчисление предикатов.15
13 REF _Ref103424090 \h \* MERGEFORMAT 14Теория равенства.15
13 REF _Ref103424137 \h \* MERGEFORMAT 14Формальная арифметика.15
13 REF _Ref103424171 \h \* MERGEFORMAT 14Теория частично упорядоченных множеств.15
13 REF _Ref103424218 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103424282 \h \* MERGEFORMAT 14Глава 7. Алгоритмы.15
13 REF _Ref103424314 \h \* MERGEFORMAT 14Глава 8. Рекурсивные функции.15
13 REF _Ref103424423 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103424463 \h \* MERGEFORMAT 14Глава 9. Машины Тьюринга.15
13 REF _Ref103424513 \h \* MERGEFORMAT 14Операции с машинами Тьюринга.15
13 REF _Ref103424561 \h \* MERGEFORMAT 14Принцип двойственности.15
13 REF _Ref103424623 \h \* MERGEFORMAT 14Способы композиции машин Тьюринга.15
13 REF _Ref103424670 \h \* MERGEFORMAT 14Задачи.15
13 REF _Ref103424706 \h \* MERGEFORMAT 14Ответы и указания.15
13 REF _Ref103424732 \h \* MERGEFORMAT 14Литература.15


Введение.

Логикой называют науку о законах и формах мышления. Формальная логика изучает формы правильных рассуждений. Математическая логика – часть формальной логики – изучает формы рассуждений, принятые в математике.
В настоящее время значение математической логики в инженерном образовании возрастает в связи с необходимостью развития математического мышления, а также изучения дискретной или компьютерной математики. Математическая логика и теория алгоритмов являются основой курса дискретной математики, что нашло отражение в данном учебном пособии.
Учебное пособие адресовано студентам, обучающимся по направлениям 210300 – радиотехника, 230000 – информатика и вычислительная техника, и по специальностям: 210401 – физика и техника оптической связи, 210402 – средства связи с подвижными объектами, 210403 – защищенные системы связи, 210404 – многоканальные телекоммуникационные системы, 210405 – радиосвязь, радиовещание и телевидение, 210406 – сети связи и системы коммутации, и полностью соответствует действующему Государственному образовательному стандарту высшего профессионального образования и требованиям квалификационной характеристики выпускника. Теоретическая часть пособия основана на лекциях, читанных автором в Поволжской государственной академии телекоммуникаций и информатики.
Сейчас издается достаточно большое количество учебной литературы по дискретной математике. В этой литературе (в особенности, [13 REF _Ref103842159 \r \h \* MERGEFORMAT 14315], [13 REF _Ref103768444 \r \h \* MERGEFORMAT 141215], [13 REF _Ref103842224 \r \h \* MERGEFORMAT 141415]) уделяется внимание и математической логике, и теории алгоритмов. Тем не менее, и указанные пособия, и задачники, в частности, [13 REF _Ref103842263 \r \h \* MERGEFORMAT 14215] и [13 REF _Ref103842293 \r \h \* MERGEFORMAT 14615], ориентированы все же на математиков, а не на студентов инженерных специальностей (исключениями являются, пожалуй, только [13 REF _Ref103842335 \r \h \* MERGEFORMAT 14115], [13 REF _Ref103842359 \r \h \* MERGEFORMAT 14815], [13 REF _Ref103842391 \r \h \* MERGEFORMAT 141315], на идеях которых основывался автор). Поэтому в настоящем пособии приведено достаточно много задач, причем решения многих задач подробно разобраны.
Предполагается, что студент, начинающий работу с данным учебным пособием, знаком с основными понятиями теории множеств и отношений, а также с аппаратом булевых функций.
Автор выражает благодарность рецензентам – доктору технических наук, профессору В.К.Трофимову и доктору физико-математических наук, профессору В.Е.Воскресенскому, а также доцентам Самарского государственного университета Е.Я.Гореловой, И.С.Фролову и И.А.Шведовой за содержательные консультации и внимание к работе.

В 13 REF _Ref104648548 \h 14Содержание.15






Глава 1. Высказывания, формулы, тавтологии.

Определение. Высказыванием называется утверждение, которое является истинным или ложным (но не одновременно).

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

Пример. “Москва – столица России” – истинное высказывание.
“5 –четное число” – ложное высказывание.
“13 EMBED Equation.3 1415” – не высказывание (неизвестно, какие значения принимает 13 EMBED Equation.3 1415).
“Студент второго курса” не высказывание (не является утверждением).

Высказывания бывают элементарные и составные.
Элементарные высказывания не могут быть выражены через другие высказывания. Составные высказывания можно выразить с помощью элементарных высказываний.

Пример. “Число 22 четное” – элементарное высказывание.
“Число 22 четное и делится на 11” – составное высказывание.

Высказывания обозначают заглавными буквами латинского алфавита: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, Эти буквы называют логическими атомами.
При фиксированном множестве букв 13 EMBED Equation.3 1415 интерпретацией называется функция 13 EMBED Equation.3 1415, которая отображает множество 13 EMBED Equation.3 1415 во множество истинностных (логических) значений 13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415.
Истинностные значения истина и ложь сокращенно обозначаются и, л или T, F, или 1,0. Мы будем использовать обозначения 1 и 0. В определенной интерпретации буквы принимают значения 1 или 0.
К высказываниям и буквам можно применять известные из курса дискретной математики логические связки или логические операции. При этом получаются формулы (формы). Формулы становятся высказываниями при подстановке всех значений букв.
Таблицы истинности основных логических операций.

13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

0
0
1
0
0
1
1

0
1
1
0
1
1
0

1
0
0
0
1
0
0

1
1
0
1
1
1
1


Более строго формула определяется так.

Определение. 1) Всякая буква есть формула.
Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 - формулы, то формулами являются также 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Символ является формулой тогда и только тогда, когда это следует из 1) и 2).

В классической логике формулы принято заключать в круглые скобки, но в мы этого делать не будем. Для всякой формулы можно построить таблицу истинности.
Значение формулы 13 EMBED Equation.3 1415 в заданной интерпретации 13 EMBED Equation.3 1415 обозначают 13 EMBED Equation.3 1415 (или 13 EMBED Equation.3 1415, или 13 EMBED Equation.3 1415).
Часть формулы, которая сама является формулой, называется подформулой данной формулы.

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

Другими словами, тавтология – это тождественно истинная формула.
Установить, является ли формула тавтологией, можно:
по таблице истинности,
используя свойства логических операций.
Из курса дискретной математики известны основные логические эквивалентности (свойства логических операций), которые являются примерами тавтологий.
Коммутативность: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Ассоциативность:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
3. Дистрибутивность:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Идемпотентность: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Закон двойного отрицания: 13 EMBED Equation.3 1415.
Закон исключения третьего: 13 EMBED Equation.3 1415.
Закон противоречия: 13 EMBED Equation.3 1415.
Законы де Моргана:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Свойства операций с логическими константами:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Здесь 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – любые буквы.

Примеры. 1. Доказать, что формула 13 EMBED Equation.3 1415 является тавтологией.
Доказательство. Допустим, что при некоторых значениях букв (то есть в некоторой интерпретации)
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Приходим к противоречию, которое доказывает, что исходная формула – тавтология.

2. Доказать, что формула 13 EMBED Equation.3 1415 является тавтологией.
Доказательство. Эквиваленция истинна, если левая и правая части принимают одинаковые значения на некотором наборе значений букв.
Допустим, что при некоторых значениях букв
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Следовательно, исходная формула – тавтология.

3. Доказать, что формула 13 EMBED Equation.3 1415 является тавтологией.
Доказательство. Допустим, что при некоторых значениях букв
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Следовательно, исходная формула – тавтология.

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

Теорема. Пусть формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – тавтологии. Тогда формула 13 EMBED Equation.3 1415 – тавтология.
Доказательство. Пусть 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 – буквы в формулах 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415. В теории булевых функций было доказано, что все булевы функции, а, следовательно, и формулы, можно считать зависящими от одного и того же количества букв. Рассмотрим некоторый набор значений 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. Подставим данный набор значений в формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 вместо соответствующих букв. Формулы являются тавтологиями по условию теоремы, следовательно, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 141513 EMBED Equation.3 1415. По таблице истинности импликации получаем, что 13 EMBED Equation.3 1415. Поскольку набор значений 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 был произволен, формула 13 EMBED Equation.3 1415 – тавтология, что и требовалось доказать.

Теорема. Пусть формула 13 EMBED Equation.3 1415 – тавтология, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 – буквы в формуле 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 – любые формулы. Тогда новая формула 13 EMBED Equation.3 1415 – тавтология.
Доказательство аналогично доказательству предыдущей теоремы.

В 13 REF _Ref104648548 \h 14Содержание.15





Отношения логической эквивалентности и логического следствия.

Определение. Формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 называются логически эквивалентными тогда и только тогда, когда формула 13 EMBED Equation.3 1415 – тавтология.

Замечание. Формула 13 EMBED Equation.3 1415 – тавтология, если таблицы истинности формул 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 совпадают.

Пример. По законам де Моргана, логически эквивалентны формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415, а также формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.

Теорема. Отношение логической эквивалентности является отношением эквивалентности.
Рефлексивность, симметричность и транзитивность данного отношения следуют из замечания.

Справедливы правило подстановки и правило замены.

Пусть 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – формулы, содержащие букву 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – формулы, полученные из формул 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 соответственно подстановкой вместо буквы 13 EMBED Equation.3 1415 формулы 13 EMBED Equation.3 1415.

Правило подстановки. Если формула 13 EMBED Equation.3 1415 логически эквивалентна формуле 13 EMBED Equation.3 1415, то формула 13 EMBED Equation.3 1415 логически эквивалентна формуле 13 EMBED Equation.3 1415.

Пусть 13 EMBED Equation.3 1415 – формула, в которой выделена некоторая подформула 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – формула, полученная из формулы 13 EMBED Equation.3 1415 заменой 13 EMBED Equation.3 1415 на некоторую формулу 13 EMBED Equation.3 1415.

Правило замены. Если формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 логически эквивалентны, то логически эквивалентны и формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.

Доказательства правил подстановки и замены основано на сравнении таблиц истинности соответствующих формул.

Пример. Известна тавтология 13 EMBED Equation.3 1415 (проверьте самостоятельно). По правилу подстановки, формула 13 EMBED Equation.3 1415 логически эквивалентна формуле 13 EMBED Equation.3 1415. По правилу замены, примененному к закону двойного отрицания, получаем, что формула 13 EMBED Equation.3 1415 логически эквивалентна формуле 13 EMBED Equation.3 1415. Следовательно, по свойству транзитивности, формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 логически эквивалентны.

Определение. Говорят, что формула 13 EMBED Equation.3 1415 логически влечет формулу 13 EMBED Equation.3 1415 (из формулы 13 EMBED Equation.3 1415 логически следует формула 13 EMBED Equation.3 1415), если формула 13 EMBED Equation.3 1415 является тавтологией.

Теорема. Отношение логического следствия является отношением предпорядка, то есть рефлексивным и транзитивным отношением.

Пример. Формула 13 EMBED Equation.3 1415 логически влечет формулу 13 EMBED Equation.3 1415. В самом деле, в примере 1 предыдущего пункта было доказано, что формула 13 EMBED Equation.3 1415 является тавтологией.

В 13 REF _Ref104648548 \h 14Содержание.15





Задачи.

1. Установить, является ли предложение высказыванием, и если является, истинно оно или ложно.
Волга впадает в Каспийское море.
Студент второго курса.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Существует человек, который не старше своего отца.
13 EMBED Equation.3 1415.
Марс есть спутник Земли.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Который час?

2. Установить, является ли предложение высказыванием, и если является, истинно оно или ложно.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
13 EMBED Equation.3 141513 EMBED Equation.3 1415.

3. Среди следующих высказываний выделить элементарные и составные. В составных высказываниях обозначить элементарные высказывания буквами и записать с помощью логических символов.
Число 6 является делителем числа 36.
Число 225 делится нацело на 5.
Число 225 делится нацело на 5 и не делится на 10.
Если 81 делится нацело на 9, то 81 делится на 3.
16 кратно 2.
18 кратно 2 и 3.
13 EMBED Equation.3 1415.
Число 39 имеет 2 простых делителя.
Двузначное число 19 простое.
Корнями уравнения 13 EMBED Equation.3 1415 являются числа 2 и 3.

4. Пусть 13 EMBED Equation.3 1415 обозначает высказывание “Я увлекаюсь горным туризмом”, а 13 EMBED Equation.3 1415 обозначает высказывание “Я изучаю программирование”. Дайте словесную формулировку следующих высказываний:
13 EMBED Equation.3 1415 ; 2) 13 EMBED Equation.3 1415; 3) 13 EMBED Equation.3 1415; 4) 13 EMBED Equation.3 1415; 5) 13 EMBED Equation.3 1415; 6) 13 EMBED Equation.3 1415;
7) 13 EMBED Equation.3 1415; 8) 13 EMBED Equation.3 1415; 9) 13 EMBED Equation.3 1415; 10) 13 EMBED Equation.3 1415.

5. Проверить, является ли формула тавтологией, без построения таблицы истинности.
1) 13 EMBED Equation.3 1415.
6) 13 EMBED Equation.3 1415.

2) 13 EMBED Equation.3 1415.
7) 13 EMBED Equation.3 1415.

3) 13 EMBED Equation.3 1415.
8) 13 EMBED Equation.3 1415.

4) 13 EMBED Equation.3 1415.
9) 13 EMBED Equation.3 1415.

5) 13 EMBED Equation.3 1415.
10) 13 EMBED Equation.3 1415.


6. Доказать, что формула является тавтологией, без построения таблицы истинности. Во всех формулах выделить всевозможные подформулы.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

Доказать, что формулы логически эквивалентны.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.

Доказать, что первая формула логически влечет вторую формулу.
13 EMBED Equation.3 1415; 13 EMBED Equation.3 14
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
9. Доказать теорему о том, что отношение логической эквивалентности является отношением эквивалентности.

10. Доказать теорему о том, что отношение логического следования является отношением предпорядка.

В 13 REF _Ref103424706 \h 14Ответы и указания.15
В 13 REF _Ref104648548 \h 14Содержание.15





Глава 2. Формальные теории.

Одним из основных понятий математической логики является понятие формальной теории или исчисления. Это понятие было первоначально разработано для формализации логики и теории доказательств. Формальная теория является эффективным механизмом получения новых теорем. Кроме того, аппарат формальной теории позволяет решать задачи, связанные с математическим моделированием различных явлений и процессов.

Формальная теория считается заданной, если известны следующие четыре составляющих:

Алфавит – конечное или счетное множество символов.

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

Аксиомы – выделенное из множества формул специальное подмножество. Множество аксиом может быть конечным или бесконечным. Бесконечное множество аксиом задается с помощью конечного множества схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Различают два вида аксиом: логические (общие для класса формальных теорий) и собственные (определяющие содержание конкретной теории).

Правила вывода – множество отношений (как правило, конечное) на множестве формул, позволяющие из аксиом получать теоремы формальной теории.

Обратите внимание, что здесь аксиомы – это необязательно утверждения, не требующие доказательства.

Определение. Выводом формальной теории называется последовательность формул 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, в которой все формулы – либо аксиомы, либо получаются из предыдущих по правилам вывода.

Говорят, что формула 13 EMBED Equation.3 1415 выводима из множества формул 13 EMBED Equation.3 1415 (обозначение: 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415), если существует вывод 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415, и есть три возможности:
13 EMBED Equation.3 1415;
13 EMBED Equation.3 1415 - аксиома;
13 EMBED Equation.3 1415 получаются из предыдущих формул по правилам вывода.
Формулы из множества 13 EMBED Equation.3 1415 называются посылками или гипотезами вывода.
Примеры выводов мы рассмотрим в определенных формальных теориях.
В частном случае, когда 13 EMBED Equation.3 1415, имеет место обозначение:
·13 EMBED Equation.3 1415, и формула 13 EMBED Equation.3 1415 называется выводимой в данной теории (или теоремой данной теории). Иногда значок
· записывается так:
·13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – обозначение данной теории.

В 13 REF _Ref104648548 \h 14Содержание.15






Глава 3. Исчисление высказываний.

Исчисление высказываний (теория L) определяется следующими компонентами.

1. Алфавит составляют:
Пропозициональные буквы (от англ. proposition – высказывание) – заглавные буквы латинского алфавита (иногда с индексами – натуральными числами): 13 EMBED Equation.3 1415,13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,13 EMBED Equation.3 1415,13 EMBED Equation.3 1415,
Логические связки: 13 EMBED Equation.3 1415.
Скобки: (, ).

Иногда в исчислении высказываний допускаются формулы с другими логическими связками, но при этом учитывается, как они выражаются через инверсию и импликацию. Так, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. Такие записи являются удобными сокращениями.

2. Формулы определяются так же, как в главе 1.

Определение. 1) Всякая пропозициональная буква есть формула.
Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – формулы, то формулами являются также 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Символ является формулой тогда и только тогда, когда это следует из 1) и 2).

3. Аксиомы задаются тремя схемами аксиом:
А1. 13 EMBED Equation.3 1415.
А2. 13 EMBED Equation.3 1415.
А3. 13 EMBED Equation.3 1415.

Существуют исчисления высказываний с другим набором логических связок и другими схемами аксиом, но в данном пособии они не рассматриваются. Желающие могут ознакомиться с ними в [13 REF _Ref103768444 \r \h \* MERGEFORMAT 141215].

4. Правило вывода Modus ponens (сокращенно MP) – правило отделения (лат.).
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.

Здесь 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – любые формулы. Таким образом, множество аксиом исчисления высказываний, заданное тремя схемами аксиом, бесконечно. Множество правил вывода задано одной схемой, и также бесконечно.

Теорема. Все теоремы исчисления высказываний – тавтологии.
Доказательство. Докажем сначала, что аксиомы А1 – А3 являются тавтологиями.
Предположим, что
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Полученное противоречие доказывает, что аксиома А1 – тавтология.
Предположим, что
13 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415 13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Полученное противоречие доказывает, что аксиома А2 – тавтология.
Предположим, что
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Полученное противоречие доказывает, что аксиома А3 – тавтология.
Таким образом, все аксиомы исчисления высказываний представляют собой тавтологии. Теоремы выводятся по правилу вывода MP, следовательно, по ранее полученным результатам (см. 13 REF _Ref104031008 \h 14Глава 1. Высказывания, формулы, тавтологии.15), также являются тавтологиями, что и требовалось доказать.

Следствие. Исчисление высказываний непротиворечиво.
Доказательство. Предположим противное, то есть в исчислении есть теоремы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415. По доказанной теореме, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 являются тавтологиями (тождественно истинными формулами), следовательно, формула 13 EMBED Equation.3 1415 одновременно является тождественно истинной и тождественно ложной, что является противоречием.

Лемма.
·13 EMBED Equation.3 1415.
Доказательство. Построим вывод формулы 13 EMBED Equation.3 1415.
1. 13 EMBED Equation.3 1415. А1 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415.
2. 13 EMBED Equation.3 1415. А1 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415.
3. 13 EMBED Equation.3 1415
А2 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415, а вместо 13 EMBED Equation.3 1415 –13 EMBED Equation.3 1415.
4. 13 EMBED Equation.3 1415. МР 2,3.
5. 13 EMBED Equation.3 1415. МР 1,4.
Что и требовалось доказать.

Теорема дедукции. Пусть 13 EMBED Equation.3 1415 – множество формул, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – формулы. Тогда 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
В частности, если 13 EMBED Equation.3 1415, то если 13 EMBED Equation.3 1415
·13 EMBED Equation.3 141513 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Доказательство. Пусть 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, – вывод из 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415. Методом математической индукции докажем, что 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Проверим, что утверждение 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415 справедливо при 13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Для 13 EMBED Equation.3 1415 возможны три варианта: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – аксиома, 13 EMBED Equation.3 1415.
а) Пусть 13 EMBED Equation.3 1415 или 13 EMBED Equation.3 1415 – аксиома. Построим вывод:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. А1 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415, вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. МР 1, 2.
Таким образом, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
б) Пусть 13 EMBED Equation.3 1415. По лемме,
·13 EMBED Equation.3 141513 EMBED Equation.3 1415. Таким образом, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Пусть утверждение 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415 верно при 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. Докажем утверждение для 13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Для формулы 13 EMBED Equation.3 1415 есть следующие возможности: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – аксиома, 13 EMBED Equation.3 1415, которые рассматриваются аналогично предыдущему пункту, и новая возможность: 13 EMBED Equation.3 1415 получается из предыдущих формул 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, по правилу Modus ponens. Последний случай рассмотрим подробно.
Среди формул 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 есть формулы (может быть, и не одна) вида 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, такие, что имеет место формула 13 EMBED Equation.3 1415 (которая также присутствует в выводе), поэтому и возможно применение правила Modus ponens.
По предположению индукции, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Построим вывод:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. А2 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415, вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. МР 2, 3.
13 EMBED Equation.3 1415.
Таким образом, доказано, что 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, следовательно, по методу математической индукции, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415. Теорема доказана.

Справедлива и обратная теорема.

Теорема. 13 EMBED Equation.3 1415
·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Доказательство. Построим вывод:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. По условию теоремы, эта формула выводима из 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. МР 2, 3.
Теорема доказана.

На основании теоремы дедукции получена теорема о полноте исчисления высказываний. Доказательство этой теоремы довольно громоздко, поэтому желающие могут ознакомиться с ним в [13 REF _Ref103768444 \r \h \* MERGEFORMAT 141215].

Теорема о полноте. Всякая тавтология является теоремой исчисления высказываний.

Следствие. Множество всех теорем исчисления высказываний совпадает с множеством всех тавтологий.

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

В 13 REF _Ref104648548 \h 14Содержание.15






Построение вывода в логике высказываний.

Пример. Докажем, что выводима формула 13 EMBED Equation.3 1415. Сокращенно это записывается так:
·13 EMBED Equation.3 1415.
По теореме, обратной теореме дедукции, посылку можно перенести в левую часть:
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Проделаем эту операцию еще раз:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Таким образом, нам нужно доказать, что из формул 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 выводима формула 13 EMBED Equation.3 1415. Составим вывод формулы 13 EMBED Equation.3 1415. В каждой строке вывода записывается только одна формула. В правой части страницы удобно указывать комментарий, – что собой эта формула представляет. Возможны варианты:
гипотеза,
аксиома (может быть, с какими-то подстановками),
ранее доказанная теорема,
формула получена из предыдущих формул по правилу Modus ponens.
Вначале мы запишем гипотезы.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
Формулу 13 EMBED Equation.3 1415 удобно получить из аксиомы А3. Поэтому запишем эту аксиому:
3. 13 EMBED Equation.3 1415 А3.
К формулам 1 и 3 можно применить правило вывода Modus ponens (что мы и отметим в комментарии). Порядок номеров формул существенен (первой указывается посылка).
4. 13 EMBED Equation.3 1415. МР 1, 3.
Посылку в формуле 4 можно получить из аксиомы А1, если заменить 13 EMBED Equation.3 1415 на 13 EMBED Equation.3 1415:
13 EMBED Equation.3 1415. А1 с подстановкой вместо 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415.
Далее дважды применяем правило Modus ponens:
13 EMBED Equation.3 1415. МР 2, 5.
13 EMBED Equation.3 1415. МР 6, 4.
Вывод построен, и применением теоремы дедукции мы доказали выводимость первоначальной формулы.
Отметим, что вывод может быть неединственным, в частности, формулы могут быть записаны в другом порядке. Решение данной задачи может быть оформлено следующим образом:

·13 EMBED Equation.3 1415.
По теореме, обратной теореме дедукции,
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415. А1, 13 EMBED Equation.3 1415: 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. МР 2, 3.
13 EMBED Equation.3 1415. А3.
13 EMBED Equation.3 1415. МР 1, 5.
13 EMBED Equation.3 1415. МР 4, 6.

Пример. Данный пример более прост, но достаточно показателен. Обратите внимание, что здесь не используются ни аксиомы, ни теоремы. Доказательство теоремы
·13 EMBED Equation.3 1415 строится только на основании правила МР.
По теореме, обратной теореме дедукции,
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415. MP 3,2.
13 EMBED Equation.3 1415. MP 4,1.

В 13 REF _Ref104648548 \h 14Содержание.15





Задачи.

Указать, какие из следующих выражений являются формулами исчисления высказываний.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

2. Какая из приведенных ниже записей является выводом формулы 13 EMBED Equation.3 1415 в исчислении высказываний?
По теореме, обратной теореме дедукции,
·13 EMBED Equation.3 1415 равносильно 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415. MP 2,1.
По теореме, обратной теореме дедукции,
·13 EMBED Equation.3 1415 равносильно 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415. MP 3,1.
13 EMBED Equation.3 1415. MP 2,4.
По теореме, обратной теореме дедукции,
·13 EMBED Equation.3 1415 равносильно 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415 – гипотеза.
13 EMBED Equation.3 1415. MP 2,1.
13 EMBED Equation.3 1415. MP 2,4.

3. Построить вывод формулы.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

В 13 REF _Ref103424706 \h 14Ответы и указания.15
В 13 REF _Ref104648548 \h 14Содержание.15








Глава 4. Метод резолюций в логике высказываний.

Метод резолюций – это метод автоматического доказательства теорем – основы логического программирования. Это алгоритм, проверяющий отношение выводимости 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415. В общем случае алгоритм автоматического доказательства теорем не существует, но для формальных теорий с несложной структурой (таких как исчисление высказываний, исчисление предикатов с одним одноместным предикатом) подобные алгоритмы известны.
Вообще говоря, в построенном в главе 3 исчислении высказываний (благодаря полноте исчисления) проверка выводимости формулы состоит в проверке того, является ли формула тавтологией или нет. Это можно легко установить по таблицам истинности. Но этот метод не обеспечивает построения вывода формулы.
Метод резолюций – классический алгоритм автоматического доказательства теорем. Для простоты изложения рассмотрим его для исчисления высказываний. Для любого множества формул 13 EMBED Equation.3 1415 и любой формулы 13 EMBED Equation.3 1415 метод дает утвердительный ответ, если 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, и дает отрицательный ответ, если неверно, что 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.

Теорема о доказательстве от противного. Если 13 EMBED Equation.3 1415,13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – тождественно ложная формула, то 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Доказательство. Доказательство проведем для частного случая, когда 13 EMBED Equation.3 1415 представляет собой одну формулу. По теореме дедукции, 13 EMBED Equation.3 1415,13 EMBED Equation.3 1415
·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415 – тавтология. Преобразуем правую часть равносильности, учитывая, что формула 13 EMBED Equation.3 1415 тождественно ложна.
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 1415 – тавтология ( 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415, что и требовалось доказать.

Как правило, в качестве формулы 13 EMBED Equation.3 1415 используют пустую формулу (, которая не имеет никакого значения ни в какой интерпретации, и, по определению, является противоречием.
Метод резолюций использует специальную форму формул, которая называется предложением.

Определение. Предложением называется дизъюнкция формул вида 13 EMBED Equation.3 1415 или 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – атом (буква).

Любая формула исчисления высказываний может быть преобразована в предложение следующей последовательностью действий:
Замена импликации по формуле: 13 EMBED Equation.3 1415 (проверьте самостоятельно). В результате в формуле остаются связки: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Преобразование выражений с инверсиями по закону двойного отрицания: 13 EMBED Equation.3 1415, законам де Моргана: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. В результате инверсии остаются только перед буквами.
Приведение формулы к конъюнктивной нормальной форме с помощью дистрибутивных законов:
13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415.
Преобразование конъюнктивной нормальной формы во множество предложений: 13 EMBED Equation.3 1415.

Напомню, что связки 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 используются здесь для удобства записи.

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

Без доказательства приведем следующую теорему.

Теорема. Если из формулы 13 EMBED Equation.3 1415 получено множество 13 EMBED Equation.3 1415 предложений, то формула 13 EMBED Equation.3 1415 тождественно ложна тогда и только тогда, когда множество 13 EMBED Equation.3 1415 невыполнимо.

До сих пор мы пользовались только одним правилом вывода – Modus ponens. В других исчислениях высказываний имеют место и другие правила вывода.

Правило резолюций. Даны предложения: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – пропозициональная буква, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – предложения (в частности, пустые или содержащие только одну букву или ее отрицание). Правило резолюций формулируется так: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415
·13 EMBED Equation.3 141513 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 называются резольвируемыми предложениями, а 13 EMBED Equation.3 141513 EMBED Equation.3 1415 – резольвентой.
Правило резолюций будем обозначать 13 EMBED Equation.3 1415.

Теорема. Резольвента логически следует из резольвируемых предложений.
Доказательство. В вышеприведенных обозначениях, нам нужно доказать, что 13 EMBED Equation.3 1415 – тавтология (по теореме дедукции).
Предположим, что 13 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
Полученное противоречие доказывает утверждение теоремы.

Правило резолюций применяется в опровержении методом резолюций – алгоритме, устанавливающем выводимость 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
Запишем 13 EMBED Equation.3 1415. Каждая формула из множества 13 EMBED Equation.3 1415 и формула 13 EMBED Equation.3 1415 независимо преобразуются во множество предложений. В этом множестве нужно найти резольвируемые предложения и применить к ним правило резолюций. Резольвенты добавляются во множество предложений до тех пор, пока не будет получено пустое предложение. Возможны два случая:
Среди множества предложений нет резольвируемых. Вывод: теорема опровергнута, и формула 13 EMBED Equation.3 1415 не выводима из множества формул 13 EMBED Equation.3 1415.
Получено пустое предложение. Теорема доказана. Имеет место выводимость 13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.

Примеры. 1. Методом резолюций доказать теорему
·13 EMBED Equation.3 1415.
Доказательство. Запишем инверсию исходной формулы:
13 EMBED Equation.3 1415.
Заменим все импликации по соответствующей формуле:
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Применим закон двойного отрицания и закон де Моргана:
13 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
Получаем предложения: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. Резольвируем их:
13 EMBED Equation.3 1415 – предложение.
13 EMBED Equation.3 1415 – предложение.
13 EMBED Equation.3 1415 – предложение.
(. 13 EMBED Equation.3 1415 1, 2.

2. Методом резолюций доказать теорему

·13 EMBED Equation.3 1415.
Доказательство. Запишем инверсию исходной формулы:
13 EMBED Equation.3 1415.
Заменим все импликации по соответствующей формуле:
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Применим закон двойного отрицания и закон де Моргана:
13 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Получаем предложения: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 – предложение.
13 EMBED Equation.3 1415 – предложение.
13 EMBED Equation.3 1415 – предложение.
13 EMBED Equation.3 1415. 13 EMBED Equation.3 1415 1, 3.
(. 13 EMBED Equation.3 1415 2, 4.

В 13 REF _Ref104648548 \h 14Содержание.15




Задачи.

Методом резолюций доказать теоремы:

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 141513 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.

·13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.

·13 EMBED Equation.3 141513 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

·13 EMBED Equation.3 1415.

В 13 REF _Ref104648548 \h 14Содержание.15







Глава 5. Предикаты.

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

Определение. n-местным предикатом на множестве 13 EMBED Equation.3 1415 называется 13 EMBED Equation.3 1415-местная функция из множества13 EMBED Equation.3 1415 во множество 13 EMBED Equation.3 1415.

Примеры. 1. Предикат 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415 – одноместный.
2. Предикат 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415 – двуместный.

Если 13 EMBED Equation.3 1415, то 13 EMBED Equation.3 1415-местный предикат представляет собой 13 EMBED Equation.3 1415-местную булеву функцию.
Нульместный предикат представляет собой высказывание.
Для каждого предиката 13 EMBED Equation.3 1415 областью истинности называется множество 13 EMBED Equation.3 1415, на котором предикат принимает значение 1.

Примеры. 1. Для предиката 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415 область истинности 13 EMBED Equation.3 1415.
2. Для предиката 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415 область истинности 13 EMBED Equation.3 1415.

Поскольку множество значений любого предиката лежит во множестве 13 EMBED Equation.3 1415, то с предикатами можно производить все операции алгебры логики, и все известные свойства логических операций обобщаются для предикатов. Рассмотрим эти свойства (для удобства в свойствах записываются одноместные предикаты):
Коммутативность:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
2. Ассоциативность:
13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415.
3. Дистрибутивность:
13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415.
Идемпотентность: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Закон двойного отрицания: 13 EMBED Equation.3 1415.
Закон исключения третьего: 13 EMBED Equation.3 1415.
Закон противоречия: 13 EMBED Equation.3 1415.
Законы де Моргана:
13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415.
Свойства операций с логическими константами:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Здесь 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – любые предикаты.

В то же время, для предикатов определены операции специального вида, которые называются кванторами.
Пусть дан 13 EMBED Equation.3 1415-местный предикат 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415, означающий, что для набора 13 EMBED Equation.3 1415 выполнено свойство 13 EMBED Equation.3 1415, и пусть 13 EMBED Equation.3 1415 – одна из переменных. Тогда запись 13 EMBED Equation.3 1415 означает, что для всех значений переменной 13 EMBED Equation.3 1415 свойство 13 EMBED Equation.3 1415 выполнено. Символ 13 EMBED Equation.3 1415 называется квантором всеобщности (общности). Предикат 13 EMBED Equation.3 1415 является (13 EMBED Equation.3 1415)-местным. Он зависит от переменных 13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415. Если дан одноместный предикат 13 EMBED Equation.3 1415, то утверждение 13 EMBED Equation.3 1415 представляет собой нульместный предикат, то есть истинное или ложное высказывание.

Пример. На множестве 13 EMBED Equation.3 1415 дан предикат 13 EMBED Equation.3 1415. Высказывание 13 EMBED Equation.3 1415 ложно.

Пусть дан 13 EMBED Equation.3 1415-местный предикат 13 EMBED Equation.3 1415 на множестве 13 EMBED Equation.3 1415, означающий, что для набора 13 EMBED Equation.3 1415выполнено свойство 13 EMBED Equation.3 1415, и пусть 13 EMBED Equation.3 1415 – одна из переменных. Тогда запись 13 EMBED Equation.3 1415 означает, что существует значение переменной 13 EMBED Equation.3 1415, такое, что выполняется свойство 13 EMBED Equation.3 1415. Символ 13 EMBED Equation.3 1415 называется квантором существования. Предикат 13 EMBED Equation.3 1415 является (13 EMBED Equation.3 1415)-местным. Если дан одноместный предикат 13 EMBED Equation.3 1415, то утверждение 13 EMBED Equation.3 1415 представляет собой нульместный предикат, то есть истинное или ложное высказывание.

Пример. На множестве 13 EMBED Equation.3 1415 дан предикат 13 EMBED Equation.3 1415. Высказывание 13 EMBED Equation.3 1415 истинно.

Отметим, что запись 13 EMBED Equation.3 1415 (13 EMBED Equation.3 1415) не подразумевает, что в формуле 13 EMBED Equation.3 1415 есть переменная 13 EMBED Equation.3 1415.
Пусть дана запись 13 EMBED Equation.3 1415 (или 13 EMBED Equation.3 1415). Переменная 13 EMBED Equation.3 1415 называется переменной в кванторе, а 13 EMBED Equation.3 1415 – областью действия квантора.
Имеют место эквивалентности:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

Отметим, что список переменных в предикате 13 EMBED Equation.3 1415 мы будем указывать не всегда.

Предикат называется тождественно истинным (тождественно ложным), если при всех возможных значениях переменных он принимает значение 1(0).

Теорема. Пусть 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415-местный предикат, 13 EMBED Equation.3 1415 – переменная в предикате. Тогда предикат 13 EMBED Equation.3 141513 EMBED Equation.3 1415 является тождественно истинным.
Доказательство. Возьмем произвольный набор значений 13 EMBED Equation.3 1415 переменных 13 EMBED Equation.3 1415. Подставим этот набор в предикат 13 EMBED Equation.3 141513 EMBED Equation.3 1415. Получим высказывание:
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Покажем, что это высказывание истинно. Возможны два случая.
13 EMBED Equation.3 1415, следовательно 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Соотношение выполнено при любых значениях 13 EMBED Equation.3 1415, следовательно, и при значении 13 EMBED Equation.3 1415. При подстановке этого значения получаем:
13 EMBED Equation.3 1415.
Следовательно, по свойству импликации получаем, что 13 EMBED Equation.3 1415, что и требовалось доказать.

Теорема. Пусть 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415-местный предикат, 13 EMBED Equation.3 1415 – переменная в предикате. Тогда предикат 13 EMBED Equation.3 141513 EMBED Equation.3 1415 является тождественно истинным.
Доказательство аналогично доказательству предыдущей теоремы.

Предикат называется выполнимым, если при некоторых значениях переменных он принимает значение 1.

Пример. Найти значение высказывания 13 EMBED Equation.3 1415. Предикат 13 EMBED Equation.3 1415 определен на множестве 13 EMBED Equation.3 1415.
Решение. Пусть 13 EMBED Equation.3 1415. Эквивалентность имеет место тогда и только тогда, когда для некоторого 13 EMBED Equation.3 1415 13 EMBED Equation.3 1415. Это означает, что для некоторого 13 EMBED Equation.3 1415 предикат 13 EMBED Equation.3 1415 является тождественно истинным относительно 13 EMBED Equation.3 1415, то есть для некоторого 13 EMBED Equation.3 1415 и для произвольного 13 EMBED Equation.3 1415 13 EMBED Equation.3 1415. Последнее равносильно тому, что предикат 13 EMBED Equation.3 1415 выполним. Предикат действительно является выполнимым, поскольку он определен на множестве натуральных чисел. Таким образом, поскольку все переходы были равносильными, исходное высказывание истинно.

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

Справедливы эквивалентности:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Разноименные кванторы можно переставлять только следующим образом:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Обратные формулы неверны.

Пример. Очевидно, что высказывание 13 EMBED Equation.3 1415 (13 EMBED Equation.3 1415) истинно. Поменяем кванторы местами. Получим высказывание 13 EMBED Equation.3 1415, которое является ложным.

Выражения с кванторами можно преобразовывать следующим образом:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Докажем первую эквивалентность. Пусть предикаты 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 одновременно тождественно истинны. Тогда тождественно истинным будет и предикат 13 EMBED Equation.3 1415, следовательно, истинными будут высказывания 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, а также 13 EMBED Equation.3 1415.
Пусть теперь хотя бы один из предикатов (например, 13 EMBED Equation.3 1415) не является тождественно истинным. Тогда (по свойствам конъюнкции) тождественно истинным не будет и предикат 13 EMBED Equation.3 1415, следовательно, ложным будет высказывание 13 EMBED Equation.3 1415. Высказывания 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 также будут ложными.
Таким образом, обе части эквивалентности одновременно истинны или ложны, и эквивалентность доказана.

Замечание. Формула 13 EMBED Equation.3 1415 не эквивалентна формуле 13 EMBED Equation.3 1415.
Доказательство. Рассмотрим обе формулы на множестве 13 EMBED Equation.3 1415. Пусть предикат 13 EMBED Equation.3 1415, а предикат 13 EMBED Equation.3 1415. Оба предиката не являются тождественно истинными. Предикат 13 EMBED Equation.3 1415 – тождественно истинный, и высказывание 13 EMBED Equation.3 1415 истинно. Высказывания 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 ложны, следовательно, ложно и высказывание 13 EMBED Equation.3 1415. Таким образом, построен пример, когда формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 принимают различные значения.

Тем не менее, справедливы эквивалентности:
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 1415.

Аналогично, формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 не эквивалентны. Но справедливы эквивалентности:
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
Имеют место формулы:
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Здесь 13 EMBED Equation.3 1415 не содержит переменной 13 EMBED Equation.3 1415.

Определение. Предикатная формула находится в приведенной форме, если в ней использованы только кванторные операции, а также операции инверсии, конъюнкции, дизъюнкции, причем инверсия относится только к предикатным буквам.
Определение. Предикатная формула находится в предваренной форме (предваренной нормальной форме), если она имеет вид 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 - кванторы всеобщности или существования, а формула 13 EMBED Equation.3 1415 находится в приведенной форме и не содержит кванторов.

Пример. Записать формулу
13 EMBED Equation.3 1415
в предваренной нормальной форме.
Решение. 13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
Полученная формула записана в приведенной форме. Для того чтобы квантор всеобщности можно было вынести за скобки, переобозначим переменные и выполним преобразования:
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.

Рассмотрим предикат 13 EMBED Equation.3 1415, определенный на конечном множестве 13 EMBED Equation.3 1415. Если предикат 13 EMBED Equation.3 1415 является тождественно истинным, то истинными будут высказывания 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415. При этом истинными будут высказывания 13 EMBED Equation.3 1415 и конъюнкция 13 EMBED Equation.3 141513 EMBED Equation.3 1415 13 EMBED Equation.3 1415.
Если же хотя бы для одного элемента 13 EMBED Equation.3 1415 13 EMBED Equation.3 1415 будет ложно, то ложными будут высказывания 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 141513 EMBED Equation.3 1415 13 EMBED Equation.3 1415.
Таким образом, имеет место эквивалентность 13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415 13 EMBED Equation.3 1415.
Справедлива и аналогичная эквивалентность
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415 13 EMBED Equation.3 141513 EMBED Equation.3 1415.

Пример. Найти предикат, логически эквивалентный предикату 13 EMBED Equation.3 1415, но не содержащий кванторов. Предикаты 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 определены на множестве 13 EMBED Equation.3 1415.
Решение. 13 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 1415

С помощью предикатов можно записывать различные математические утверждения.

Пример. Покажем, как можно записать утверждение: “числовая последовательность 13 EMBED Equation.3 1415 имеет пределом число 13 EMBED Equation.3 1415 (13 EMBED Equation.3 1415)”.
Решение. Запишем данное утверждение с помощью кванторов и обозначим его 13 EMBED Equation.3 1415:
13 EMBED Equation.3 1415.
Запишем инверсию данного высказывания:
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
По известным формулам, инверсия импликации преобразуется следующим образом:
13 EMBED Equation.3 1415.
Отсюда получаем:
13 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
Утверждение 13 EMBED Equation.3 1415 означает, что 13 EMBED Equation.3 1415, то есть число 13 EMBED Equation.3 1415 не является пределом числовой последовательности 13 EMBED Equation.3 1415.

В 13 REF _Ref104648548 \h 14Содержание.15



Задачи.

Среди следующих предложений выделить предикаты, и для каждого предиката установить местность и область истинности, если 13 EMBED Equation.3 1415. Для двуместных предикатов изобразить область истинности графически.
13 EMBED Equation.3 1415.
При 13 EMBED Equation.3 1415 выполняется равенство 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Однозначное число 13 EMBED Equation.3 1415 является простым.
13 EMBED Equation.3 1415.

Определить значение высказывания, полученного из трехместного предиката на множестве 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
13 EMBED Equation.
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·Записать инверсию формулы в предваренной нормальной форме.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
9) 13 EMBED Equation.3 141513 EMBED Equation.3 1415.
10) 13 EMBED Equation.3 1415.

Записать формулу в приведенной форме, если это необходимо, а затем преобразовать к предваренной форме.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
Найти предикат, не содержащий кванторов, логически эквивалентный данному предикату. Предикаты 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 определены на множестве 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

6. Записать с помощью кванторов следующие утверждения и их отрицания.
Функция 13 EMBED Equation.3 1415 возрастает на интервале 13 EMBED Equation.3 1415.
Функция 13 EMBED Equation.3 1415 непрерывна на интервале 13 EMBED Equation.3 1415.
Множество 13 EMBED Equation.3 1415 является собственным подмножеством множества 13 EMBED Equation.3 1415.
Точка 13 EMBED Equation.3 1415 является точкой экстремума функции 13 EMBED Equation.3 1415.
Функция 13 EMBED Equation.3 1415 достигает наибольшего значения на отрезке 13 EMBED Equation.3 1415 в точке 13 EMBED Equation.3 1415.
Функция 13 EMBED Equation.3 1415 дифференцируема в точке 13 EMBED Equation.3 1415.
Бинарное отношение 13 EMBED Equation.3 1415 является симметричным.
Функция 13 EMBED Equation.3 1415 ограничена на множестве 13 EMBED Equation.3 1415.
Булева функция 13 EMBED Equation.3 1415 самодвойственна.
Множества 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 не пересекаются.

7. Доказать эквивалентность
13 EMBED Equation.3 1415.

8. Доказать, что не эквивалентны формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415.

В 13 REF _Ref103424706 \h 14Ответы и указания.15
В 13 REF _Ref104648548 \h 14Содержание.15





Глава 6. Исчисление предикатов.

Рассмотрим построение теории первого порядка.
Компонентами теории первого порядка являются следующие.

1. Алфавит составляют:
Предметные константы – буквы начала латинского алфавита с натуральными индексами: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, Предметные символы – это имена (обозначения) предметов.
Предметные переменные – буквы конца латинского алфавита с натуральными индексами: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,
Функциональные буквы – строчные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер функциональной буквы): 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,
Предикатные буквы – заглавные буквы латинского алфавита с натуральными индексами (верхний индекс указывает число переменных, нижний – номер предикатной буквы): 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,... (индексы можно не указывать).
Логические связки: 13 EMBED Equation.3 1415.
Квантор всеобщности 13 EMBED Equation.3 1415.
Синтаксические символы – скобки (, ) и запятая.

2. Формула определяется несколькими этапами. Вначале вводится понятие терма.

Определение. 1) Предметные константы и предметные переменные есть термы.
2) Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, – термы, 13 EMBED Equation.3 1415 – функциональная буква, то 13 EMBED Equation.3 1415 – терм.
3) Символ является термом тогда и только тогда, когда это следует из 1) и 2).

Примеры. 1. Пусть 13 EMBED Equation.3 1415 – предметная переменная, 13 EMBED Equation.3 1415 – предметная константа, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – функциональные буквы. Тогда 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – термы.
2. Пусть 13 EMBED Equation.3 1415 – предметная переменная, 13 EMBED Equation.3 1415 – предметная константа, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – функциональные буквы. Тогда 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – термы. Здесь символы 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 имеют только формальный смысл и не интерпретируются как обозначения тригонометрических функций.

Определение. Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415, – термы, 13 EMBED Equation.3 1415 – предикатная буква, то символ 13 EMBED Equation.3 1415 называется элементарной формулой.

Другими словами, элементарная формула образуется при применении предикатной буквы к термам.

Примеры. 1. В условиях первого примера, если 13 EMBED Equation.3 1415 – предикатная буква, то 13 EMBED Equation.3 1415 – элементарная формула.
2. В условиях второго примера, если 13 EMBED Equation.3 1415 – предикатная буква, то 13 EMBED Equation.3 141513 EMBED Equation.3 1415 – элементарная формула.

Теперь определим формулу логики предикатов.

Определение. 1) Всякая элементарная формула есть формула.
2) Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – формулы, то формулами являются также символы 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
3) Символ является формулой тогда и только тогда, когда это следует из 1) и 2).

Примеры. 1. В условиях первого примера, 13 EMBED Equation.3 1415 – формула.
2. В условиях второго примера, 13 EMBED Equation.3 1415 – формула.

В теории первого порядка, как и в исчислении высказываний, допускаются формулы с другими логическими связками, а также допускается использование квантора существования. Известна формула (см. 13 REF _Ref103423939 \h 14Глава 5. Предикаты.15).
Здесь мы ненадолго отвлечемся от построения теории первого порядка и рассмотрим некоторые понятия, связанные с формулами.

Определение. Пусть 13 EMBED Equation.3 1415 – формула, 13 EMBED Equation.3 1415 – переменная, которая входит в формулу 13 EMBED Equation.3 1415 (один или несколько раз). Вхождение 13 EMBED Equation.3 1415 в формулу 13 EMBED Equation.3 1415 называется связанным, если либо 13 EMBED Equation.3 1415 – переменная в кванторе (13 EMBED Equation.3 1415), либо 13 EMBED Equation.3 1415 находится в области действия квантора 13 EMBED Equation.3 1415. Если вхождение 13 EMBED Equation.3 1415 в 13 EMBED Equation.3 1415 не связано, то оно называется свободным.

Пример. В формуле 13 EMBED Equation.3 1415 вхождения обеих переменных свободные.
В формуле 13 EMBED Equation.3 1415 вхождения переменной 13 EMBED Equation.3 1415 в посылку связаны, а вхождение в следствие свободно. Вхождение переменной 13 EMBED Equation.3 1415 свободно, так как отсутствует квантор 13 EMBED Equation.3 1415.
В формуле 13 EMBED Equation.3 1415 вхождения обеих переменных связаны.

Пусть 13 EMBED Equation.3 1415 – формула, 13 EMBED Equation.3 1415 – переменная в формуле 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – терм. Введем обозначение 13 EMBED Equation.3 1415. Тогда 13 EMBED Equation.3 1415 – результат подстановки 13 EMBED Equation.3 1415 вместо всех свободных вхождений 13 EMBED Equation.3 1415 в формулу 13 EMBED Equation.3 1415.

Пример. Рассмотрим подстановку 13 EMBED Equation.3 1415 вместо всех свободных вхождений 13 EMBED Equation.3 1415 в формулы из предыдущего примера.
В формуле 13 EMBED Equation.3 1415 вхождение 13 EMBED Equation.3 1415 свободное, следовательно, получаем 13 EMBED Equation.3 1415.
В формуле 13 EMBED Equation.3 1415 вхождения переменной 13 EMBED Equation.3 1415 в посылку связаны, а вхождение в следствие свободно. Получаем: 13 EMBED Equation.3 1415.
В формуле 13 EMBED Equation.3 1415 вхождения обеих переменных связаны, поэтому осуществить подстановку 13 EMBED Equation.3 1415 невозможно.

Определение. Терм 13 EMBED Equation.3 1415 называется свободным для переменной 13 EMBED Equation.3 1415 в формуле 13 EMBED Equation.3 1415 тогда и только тогда, когда никакое свободное вхождение 13 EMBED Equation.3 1415 в формулу 13 EMBED Equation.3 1415 не лежит в области действия квантора 13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – переменная в терме 13 EMBED Equation.3 1415.

Пример. Рассмотрим формулу 13 EMBED Equation.3 1415 и терм 13 EMBED Equation.3 1415. 13 EMBED Equation.3 1415 не свободен для переменной 13 EMBED Equation.3 1415 в данной формуле, так как 13 EMBED Equation.3 1415 лежит в области действия квантора, тем более 13 EMBED Equation.3 1415 не свободен для переменной 13 EMBED Equation.3 1415.
Пусть теперь дан терм 13 EMBED Equation.3 1415. 13 EMBED Equation.3 1415 свободен для переменной 13 EMBED Equation.3 1415.

Уточним понятие интерпретации для множества формул 13 EMBED Equation.3 1415 теории первого порядка.

Определение. Интерпретацией множества формул 13 EMBED Equation.3 1415 называется область интерпретации 13 EMBED Equation.3 1415 и заданное на ней соответствие, которое каждой предикатной букве 13 EMBED Equation.3 1415 ставит в соответствие 13 EMBED Equation.3 1415-местный предикат на 13 EMBED Equation.3 1415, каждой функциональной букве 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415-местную функцию на 13 EMBED Equation.3 1415, каждой предметной константе 13 EMBED Equation.3 1415 – элемент множества 13 EMBED Equation.3 1415.

При интерпретации формулы превращаются в предикаты на множестве 13 EMBED Equation.3 1415. Если формула не имеет свободных переменных, то после интерпретации она превращается в высказывание.

Пример. На множестве 13 EMBED Equation.3 1415 рассмотрим формулу 13 EMBED Equation.3 1415. Интерпретируем эту формулу следующим образом: 13 EMBED Equation.3 1415. Тогда мы получим предикат 13 EMBED Equation.3 1415.
Рассмотрим теперь формулу 13 EMBED Equation.3 1415. При интерпретации она превращается в истинное высказывание 13 EMBED Equation.3 1415.

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

Определение. Формула называется общезначимой (логически общезначимой), если она истинна в любой интерпретации.

Определение. Формулы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 называются логически эквивалентными тогда и только тогда, когда формула 13 EMBED Equation.3 1415 логически общезначима.

Справедлива теорема, аналогичная теореме из логики высказываний.

Теорема. Отношение логической эквивалентности является отношением эквивалентности.

Определение. Говорят, что формула 13 EMBED Equation.3 1415 логически влечет формулу 13 EMBED Equation.3 1415 (из формулы 13 EMBED Equation.3 1415 логически следует формула 13 EMBED Equation.3 1415), если формула 13 EMBED Equation.3 1415 является логически общезначимой.

Теорема. Отношение логического следствия является отношением предпорядка.

Определение. Формула называется противоречивой, если она ложна в любой интерпретации.

Теорема. Пусть 13 EMBED Equation.3 1415 – формула, 13 EMBED Equation.3 1415 – переменная в формуле 13 EMBED Equation.3 1415, терм 13 EMBED Equation.3 1415 свободен для переменной 13 EMBED Equation.3 1415 в формуле 13 EMBED Equation.3 1415. Тогда формула 13 EMBED Equation.3 1415 общезначима.
Доказательство. Пусть имеется некоторая интерпретация исходной формулы, то есть множество 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – предикат на 13 EMBED Equation.3 1415. Покажем, что 13 EMBED Equation.3 1415 – тождественно истинный предикат. Возьмем произвольный набор значений 13 EMBED Equation.3 1415 переменных 13 EMBED Equation.3 1415. Подставим этот набор в предикат. Получим высказывание:
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Покажем, что это высказывание истинно. Возможны два случая.
13 EMBED Equation.3 1415, следовательно 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Соотношение выполнено при любых значениях 13 EMBED Equation.3 1415. Подставим этот набор значений в терм 13 EMBED Equation.3 1415: 13 EMBED Equation.3 1415. Подставим последнее выражение в предикат 13 EMBED Equation.3 1415. Получим:
13 EMBED Equation.3 1415.
Но, поскольку терм 13 EMBED Equation.3 1415 свободен для переменной 13 EMBED Equation.3 1415 в формуле 13 EMBED Equation.3 1415, получаем:
13 EMBED Equation.3 141513 EMBED Equation.3 1415
Следовательно, по свойству импликации получаем, что 13 EMBED Equation.3 1415, что и требовалось доказать.

Теорема. Пусть 13 EMBED Equation.3 1415 не является свободной переменной в формуле 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – некоторая формула. Тогда формула 13 EMBED Equation.3 1415 общезначима.
Доказательство аналогично доказательству предыдущей теоремы.

Теперь мы можем вернуться к построению теории первого порядка.

3. Аксиомы теории первого порядка делятся на два класса:
Логические аксиомы:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, где терм 13 EMBED Equation.3 1415 свободен для переменной 13 EMBED Equation.3 1415 в формуле 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415, где 13 EMBED Equation.3 1415 – несвободная переменная в формуле 13 EMBED Equation.3 1415.
Отметим, что аксиомы 1) – 3) – тавтологии, 4) и 5) – общезначимые формулы.
Собственные аксиомы.
У каждой теории первого порядка свои собственные аксиомы.

4. Правила вывода.
Modus ponens (МР).
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.
2) Правило обобщения Gen.
13 EMBED Equation.3 1415
·13 EMBED Equation.3 1415.

Определение. Теория первого порядка без собственных аксиом называется исчислением предикатов первого порядка (или чистым исчислением предикатов).

Без доказательства приведем теоремы.

Теорема. Всякая теорема исчисления предикатов логически общезначима, то есть исчисление предикатов непротиворечиво.

Теорема о полноте. Всякая логически общезначимая формула является теоремой исчисления предикатов.

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

Теория равенства.

Теория равенства – теория первого порядка с предикатной буквой 13 EMBED Equation.3 1415.
Собственные аксиомы следующие:
1) 13 EMBED Equation.3 1415.
2) 13 EMBED Equation.3 1415.
Здесь 13 EMBED Equation.3 1415 – произвольная предикатная буква.

Формальная арифметика.

Формальная арифметика – теория первого порядка со следующими специальными символами.
Предметная константа 0.
Двуместные функциональные буквы 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415, одноместная функциональная буква 13 EMBED Equation.3 1415.
Двуместная предикатная буква 13 EMBED Equation.3 1415.
Собственные аксиомы следующие:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Здесь 13 EMBED Equation.3 1415 – произвольная предикатная буква.

Теория частично упорядоченных множеств.

Теория частично упорядоченных множеств – это теория первого порядка с двумя предикатными буквами 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415.
Собственные аксиомы следующие:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
Моделью данной теории является частично упорядоченное множество.

Для теорий первого порядка справедлива следующая теорема.

Теорема Гёделя о неполноте. Во всякой достаточно богатой теории первого порядка (в частности, во всякой теории, включающей формальную арифметику), существует такая истинная формула 13 EMBED Equation.3 1415, что ни 13 EMBED Equation.3 1415, ни 13 EMBED Equation.3 1415 не являются выводимыми в данной теории.

В 13 REF _Ref104648548 \h 14Содержание.15





Задачи.

Укажите, какие из следующих выражений являются формулами исчисления предикатов. В каждой формуле укажите свободные и связанные вхождения переменных:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

Пусть 13 EMBED Equation.3 1415 – натуральное число. Даны следующие утверждения.
13 EMBED Equation.3 1415 – “число 13 EMBED Equation.3 1415 кратно 5”;
13 EMBED Equation.3 1415 – “число 13 EMBED Equation.3 1415 кратно 2”;
13 EMBED Equation.3 1415 – “число 13 EMBED Equation.3 1415 кратно 4”;
13 EMBED Equation.3 1415 – “число 13 EMBED Equation.3 1415 кратно 10”;
13 EMBED Equation.3 1415 – “число 13 EMBED Equation.3 1415 кратно 20”.
Укажите, какие из следующих высказываний истинны, какие ложны.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

Записать утверждения с помощью следующих обозначений: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – человек, 13 EMBED Equation.3 1415 – преподаватель Иванов, 13 EMBED Equation.3 1415 – студент, 13 EMBED Equation.3 1415 – школьник, 13 EMBED Equation.3 1415 – отличник, 13 EMBED Equation.3 1415 – староста, 13 EMBED Equation.3 1415 – преподаватель, 13 EMBED Equation.3 1415 – работающий, 13 EMBED Equation.3 1415 – член профсоюза, 13 EMBED Equation.3 1415 – молодой, 13 EMBED Equation.3 1415 – старый, 13 EMBED Equation.3 1415 – справедливый, 13 EMBED Equation.3 1415 – девушка, 13 EMBED Equation.3 1415 – 13 EMBED Equation.3 1415 боится13 EMBED Equation.3 1415.
Некоторые школьники и студенты – отличники.
Все старосты отличники и работают.
Все преподаватели и студенты являются членами профсоюза.
Не все молодые преподаватели справедливы.
Некоторые молодые и все старые преподаватели справедливы.
Все студенты и некоторые преподаватели молоды.
Среди работающих студентов есть отличники.
Некоторые студенты боятся преподавателя Иванова.
Никто из студенток не боится преподавателя Иванова.
Среди студенток-старост есть отличницы.

4. Построить систему собственных аксиом для следующих систем:
Линейное векторное пространство.
Группа (алгебраическая).
Метрическое пространство.
Семья.
Студенческая группа.

В 13 REF _Ref104648548 \h 14Содержание.15



Глава 7. Алгоритмы.

Понятие алгоритма в настоящее время широко используется, тем не менее, строго это понятие не определено.
В математике алгоритм означает точное предписание, которое задает вычислительный процесс, начинающийся с исходных данных и направленный на получение полностью определенного исходными данными результата (см., например, [13 REF _Ref103842713 \r \h \* MERGEFORMAT 14915]).

Примерами алгоритмов являются:

Правила выполнения сложения и умножения натуральных чисел. Исходными данными являются пары натуральных чисел, результатом – натуральное число.

Правило отыскания корней квадратного уравнения с действительными коэффициентами. Исходными данными являются коэффициенты уравнения 13 EMBED Equation.3 1415, результатом – два (может быть, равных) корня квадратного уравнения (если результат ищется в комплексных числах). Если результат обязательно должен быть действительным числом, то при 13 EMBED Equation.3 1415 результат получен не будет.

Правило отыскания производной многочлена степени n. Исходными данными являются коэффициенты многочлена, результатом – коэффициенты производной многочлена.

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

Алгоритм должен удовлетворять следующим требованиям.

Массовость алгоритма. Алгоритм применяется к исходным данным, которые выбираются из потенциально бесконечного множества.

Дискретность алгоритма. Для размещения данных необходима однородная и дискретная, то есть организованная в виде одинакового количества ячеек, память.

Элементарность шагов алгоритма. Закон получения последующей системы величин из предшествующей системы должен быть простым.

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

Результативность алгоритма. После конечного числа шагов работа должна быть остановлена с указанием того, что считать результатом.

Можно выделить семь параметров, характеризующих алгоритм:
совокупность возможных исходных данных;
совокупность возможных результатов;
совокупность возможных промежуточных результатов;
правило начала;
правило непосредственной переработки;
правило окончания;
правило извлечения результата.
Мы рассмотрим элементы теории алгоритмов – рекурсивные функции и машины Тьюринга.

В 13 REF _Ref104648548 \h 14Содержание.15




Глава 8. Рекурсивные функции.

Рекурсивные функции очень хорошо иллюстрируют понятие алгоритма. Если рассуждать упрощенно, то для рекурсивной функции должен существовать алгоритм, вычисляющей ее значения. Вообще говоря, большая часть известных числовых функций являются рекурсивными.
Полезно вспомнить, как определяются элементарные функции. Вначале рассматривается несколько классов функций: алгебраические, тригонометрические, показательные, логарифмические. Элементарная функция определяется как суперпозиция (или сложная функция) этих функций.
Рекурсивные функции строятся аналогичным образом.
Обратите внимание, что все функции в данном параграфе определены на множестве 13 EMBED Equation.3 1415. Если это необходимо, в обозначении функции верхний индекс указывает число переменных. Так, функция 13 EMBED Equation.3 1415 зависит от 13 EMBED Equation.3 1415 переменных. Таким образом, 13 EMBED Equation.3 1415.
Рассмотрим вначале примитивно-рекурсивные функции.

Простейшие примитивно-рекурсивные функции задаются следующим образом.

Функция следования задается формулой: 13 EMBED Equation.3 1415 (или 13 EMBED Equation.3 1415).

Функция аннулирования задается формулой: 13 EMBED Equation.3 1415.

Функция тождества определяется следующим образом: 13 EMBED Equation.3 1415, то есть эта функция произвольному 13 EMBED Equation.3 1415-мерному вектору сопоставляет его 13 EMBED Equation.3 1415-ю координату.

Из простейших примитивно-рекурсивных функций можно получить примитивно-рекурсивные функции с помощью следующих двух операторов.

Оператор суперпозиции. Пусть 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 – примитивно-рекурсивные функции. Тогда функция
13 EMBED Equation.3 1415
получена с помощью оператора суперпозиции.
Оператор суперпозиции – это оператор построения сложной функции. Если мы умеем вычислять функции 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415, то значения функции 13 EMBED Equation.3 1415 могут быть получены последовательным вычислением значений функций 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 на некотором наборе значений 13 EMBED Equation.3 1415 переменных 13 EMBED Equation.3 1415, и вычислением значения функции 13 EMBED Equation.3 1415 на наборе значений 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415

Пример. Функция 13 EMBED Equation.3 1415 получается суперпозицией функций 0(x) и s(x): 13 EMBED Equation.3 1415. Аналогичным образом можно получить функции вида 13 EMBED Equation.3 1415 для всех значений n.

Оператор примитивной рекурсии из известных примитивно-рекурсивных функций 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 позволяет строить новую функцию 13 EMBED Equation.3 1415. Так,
13 EMBED Equation.3 141513 EMBED Equation.3 1415,
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
Тогда функция 13 EMBED Equation.3 1415 получена с помощью оператора примитивной рекурсии, что выражается обозначением 13 EMBED Equation.3 1415.

Таким образом, сначала (при фиксированных значениях 13 EMBED Equation.3 1415) определяется значение функции 13 EMBED Equation.3 1415 при 13 EMBED Equation.3 1415, а затем каждое следующее значение функции (зависящее от 13 EMBED Equation.3 1415) выражается через предыдущее значение (зависящее от 13 EMBED Equation.3 1415).
Пусть 13 EMBED Equation.3 1415. Тогда функция 13 EMBED Equation.3 1415 есть постоянная. Обозначим ее следующим образом: 13 EMBED Equation.3 1415. Функция 13 EMBED Equation.3 1415 зависит от двух переменных. Обозначим ее так: 13 EMBED Equation.3 1415. Тогда
13 EMBED Equation.3 1415,
13 EMBED Equation.3 141513 EMBED Equation.3 1415.

Для произвольного 13 EMBED Equation.3 1415 получаем (обозначения 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, , 13 EMBED Equation.3 1415 вводятся в предположении, что набор 13 EMBED Equation.3 1415 фиксирован):
13 EMBED Equation.3 141513 EMBED Equation.3 1415,
13 EMBED Equation.3 141513 EMBED Equation.3 1415,
13 EMBED Equation.3 141513 EMBED Equation.3 1415,
. . . . . . . . . . . . . . . . . .
13 EMBED Equation.3 141513 EMBED Equation.3 1415.
. . . . . . . . . . . . . . . . . .

Пример. Даны функции 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415. Определим функцию 13 EMBED Equation.3 1415, полученную из данных функций по схеме примитивной рекурсии.
Решение. Найдем значения функции 13 EMBED Equation.3 1415.
13 EMBED Equation.3 141513 EMBED Equation.3 1415,
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415;
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415;
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.
Можно предположить, что 13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Докажем последнюю формулу методом математической индукции по переменной 13 EMBED Equation.3 1415.
Проверим формулу при 13 EMBED Equation.3 1415.
13 EMBED Equation.3 141513 EMBED Equation.3 1415, то есть при 13 EMBED Equation.3 1415 формула верна.
Допустим, что предположение индукции верно при 13 EMBED Equation.3 1415, то есть, верна формула 13 EMBED Equation.3 141513 EMBED Equation.3 1415.
Докажем, что предположение индукции верно при 13 EMBED Equation.3 1415, то есть, верна формула 13 EMBED Equation.3 141513 EMBED Equation.3 1415. Выразим 13 EMBED Equation.3 1415 с помощью схемы примитивной рекурсии.
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415.
Таким образом, на основании метода математической индукции формула 13 EMBED Equation.3 141513 EMBED Equation.3 1415 доказана для всех 13 EMBED Equation.3 1415.
Теперь строго определим примитивно-рекурсивные функции.

Определение. 1) Простейшие примитивно-рекурсивные функции примитивно-рекурсивны.
Примитивно-рекурсивными являются функции, полученные из примитивно-рекурсивных функций с помощью операторов суперпозиции и (или) примитивной рекурсии.
Функция является примитивно-рекурсивной тогда и только тогда, когда это следует из 1) и 2).

Пример. Покажем, что функция 13 EMBED Equation.3 1415 примитивно-рекурсивна.
Доказательство. 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, следовательно, функция 13 EMBED Equation.3 1415 должна зависеть от одной переменной, а функция 13 EMBED Equation.3 1415 – от трех. Пользуясь заданием функции, найдем ее значения:
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
то есть 13 EMBED Equation.3 1415.
Таким образом, функция 13 EMBED Equation.3 1415 получена по схеме примитивной рекурсии (13 EMBED Equation.3 1415) из примитивно-рекурсивных функций, следовательно, сама является примитивно-рекурсивной.

Примитивно-рекурсивными, в частности, являются следующие функции: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 13 EMBED Equation.3 1415

Операция минимизации по 13 EMBED Equation.3 1415-ой переменной функции 13 EMBED Equation.3 1415 обозначается следующим образом: 13 EMBED Equation.3 1415, и определяется так.
Рассмотрим уравнение относительно 13 EMBED Equation.3 1415:
13 EMBED Equation.3 1415. (1)
Это уравнение решается подбором, вместо переменной 13 EMBED Equation.3 1415 последовательно подставляются 0,1,2, При этом возможны случаи.
На некотором шаге левая часть соотношения (1) не определена. Следовательно, на наборе 13 EMBED Equation.3 1415 операция минимизации не определена.
На каждом шаге левая часть соотношения (1) определена, но равенство не выполняется ни при каких значениях 13 EMBED Equation.3 1415. Следовательно, на наборе 13 EMBED Equation.3 1415 операция минимизации не определена.
Левая часть соотношения (1) определена при 13 EMBED Equation.3 1415, но при 13 EMBED Equation.3 1415 равенство не выполняется, а при 13 EMBED Equation.3 1415 выполняется. В этом случае число 13 EMBED Equation.3 1415 считается значением операции минимизации на наборе 13 EMBED Equation.3 1415.

Пример. [13 REF _Ref103842391 \r \h \* MERGEFORMAT 141315]. Найти функции, получаемые из данной числовой функции 13 EMBED Equation.3 1415 с помощью оператора минимизации по каждой ее переменной.
Решение. Минимизируем функцию по переменной 13 EMBED Equation.3 1415. Рассмотрим уравнение
13 EMBED Equation.3 1415. (2)
Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, то при подстановке 13 EMBED Equation.3 1415 получаем верное равенство.
Если 13 EMBED Equation.3 1415, то левая часть равенства (2) не определена.
Если 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415, то при подстановке 13 EMBED Equation.3 1415 в левой части равенства (2) появляется выражение 13 EMBED Equation.3 1415, не имеющее смысла, и в этом случае операция минимизации не определена.
Если 13 EMBED Equation.3 1415, то получаем равенство 13 EMBED Equation.3 1415. Оно имеет смысл при 13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415, что рассмотрено в первом пункте, и при 13 EMBED Equation.3 1415, то есть 13 EMBED Equation.3 1415. При 13 EMBED Equation.3 1415 равенство не имеет смысла.
Таким образом,
13 EMBED Equation.3 1415
Минимизируем функцию по переменной 13 EMBED Equation.3 1415. Рассмотрим уравнение
13 EMBED Equation.3 1415.
Это уравнение на самом первом шаге, при подстановке вместо 13 EMBED Equation.3 1415 нуля теряет смысл, значит, операция минимизации по второй переменной 13 EMBED Equation.3 1415 нигде не определена.
Минимизируем функцию по переменной 13 EMBED Equation.3 1415. Рассмотрим уравнение
13 EMBED Equation.3 1415. (3)
Если левая часть соотношения (3) имеет смысл и равенство (3) выполнено, то оно выполнено и при подстановке в это соотношение переменной 13 EMBED Equation.3 1415 на первом шаге, то есть при 13 EMBED Equation.3 1415. В остальных случаях значение операции минимизации не определено.
13 EMBED Equation.3 1415

Определение. Частично-рекурсивной функцией называется числовая функция, получаемая за конечное число шагов из простейших примитивно-рекурсивных функций с помощью операторов суперпозиции, примитивной рекурсии и минимизации.

Определение. Числовая функция называется общерекурсивной, если она частично-рекурсивна и всюду определена.

Определение. Функция 13 EMBED Equation.3 1415 называется эффективно вычислимой, если существует алгоритм, позволяющий вычислить ее значения.

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

Тезис Черча. Каждая интуитивно вычислимая функция является частично-рекурсивной.

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

В 13 REF _Ref104648548 \h 14Содержание.15





Задачи.

Определить функцию 13 EMBED Equation.3 1415, полученную из функций 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 по схеме примитивной рекурсии.
13 EMBED Equation.3 1415, –
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·Доказать, что следующие функции примитивно-рекурсивны.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415.

3. Записать схему примитивной рекурсии для произвольных примитивно-рекурсивных функций при
13 EMBED Equation.3 1415;
13 EMBED Equation.3 1415;
13 EMBED Equation.3 1415.

4. Найти функции, получаемые из данной числовой функции 13 EMBED Equation.3 1415 с помощью оператора минимизации по каждой ее переменной.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415.

В 13 REF _Ref103424706 \h 14Ответы и указания.15
В 13 REF _Ref104648548 \h 14Содержание.15








Глава 9. Машины Тьюринга.

Машина Тьюринга – это модель алгоритма, которая иллюстрирует процессы, происходящие при реализации алгоритма. Машина Тьюринга является гипотетической машиной. Ее составляют следующие компоненты.

Управляющее устройство, которое в каждый данный момент времени может находиться в одном и только одном из некоторого множества состояний. Состояния обозначаются буквами так называемого внутреннего алфавита 13 EMBED Equation.3 1415. Состояние 13 EMBED Equation.3 1415, как правило, считают начальным состоянием, а состояние 13 EMBED Equation.3 1415 – конечным (заключительным). Во внутренний алфавит включают также символы сдвига : 13 EMBED Equation.3 1415 – вправо, 13 EMBED Equation.3 1415 – влево, 13 EMBED Equation.3 1415 – на месте.

Лента, разделенная на ячейки и предполающаяся потенциально бесконечной в обе стороны (имеется в виду, что в каждый момент времени лента содержит конечное число ячеек, но при необходимости число ячеек можно увеличивать). В каждой ячейке может быть записан один и только один символ некоторого внешнего алфавита 13 EMBED Equation.3 1415. Символ 13 EMBED Equation.3 1415 принято считать пустым символом. Он обозначает пустую ячейку. По умолчанию, во всех ячейках, в которых не записаны символы 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415,, 13 EMBED Equation.3 1415, записан символ 13 EMBED Equation.3 1415. В данной главе в качестве внешнего алфавита мы будем рассматривать алфавит 13 EMBED Equation.3 1415, 0 соответствует пустому символу.

Считывающая и пишущая головка, которая в каждый данный момент времени обозревает одну ячейку.


13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

13 EMBED Equation.3 1415


13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
Рис. 1

Так, на рис. 1 считывающая головка обозревает ячейку ленты, в которой записан символ 13 EMBED Equation.3 1415. Управляющее устройство находится в состоянии 13 EMBED Equation.3 1415 (начальном состоянии). В зависимости от состояния управляющего устройства головка либо оставляет обозреваемый символ без изменения, либо записывает на его место любой другой символ внешнего алфавита, либо стирает обозреваемый символ. Далее головка либо остается на месте, либо передвигается на одну ячейку вправо или влево, при этом управляющее устройство переходит в некоторое новое состояние (состояние может и не меняться).

Каждое перемещение головки и изменение состояния управляющего устройства можно определить командой, которая обычно записывается в виде:
13 EMBED Equation.3 1415.
Здесь:
13 EMBED Equation.3 1415 – состояние, в котором управляющее устройство находится в данный момент,
13 EMBED Equation.3 1415 - символ, обозреваемый головкой,
13 EMBED Equation.3 1415 – состояние, в которое управляющее устройство переходит в зависимости от состояния 13 EMBED Equation.3 1415 и обозреваемого символа 13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415 – новый символ, который записывается в ячейку, и зависящий от 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415,
13 EMBED Equation.3 1415 – символ сдвига, указывающий направление движения головки (он также зависит от 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415).
Список команд для машины Тьюринга называется программой. Существует взаимно однозначное соответствие между машинами Тьюринга и программами.
Вид ленты в каждый момент времени может быть определен конфигурацией вида:
13 EMBED Equation.3 1415.
Головкой в данный момент обозревается символ 13 EMBED Equation.3 1415, записанный в конфигурации первым справа от символа 13 EMBED Equation.3 1415. Первый и последний символы в данной конфигурации – непустые. Считается, что остальные символы на ленте, не записанные в конфигурацию – пустые. Имеется в виду, что в данный момент времени на ленте записано слово 13 EMBED Equation.3 1415.
Конфигурация, соответствующая началу работы машины, называется начальной. Если в процессе работы машина достигает заключительного состояния, то соответствующая конфигурация называется заключительной. Машина может прекратить работу и в случае, когда в программе отсутствует команда для некоторого состояния и некоторого символа.
Если машина Тьюринга 13 EMBED Equation.3 1415, начав работу на некотором слове 13 EMBED Equation.3 1415, останавливается через некоторое число шагов, то считается, что она применима к слову 13 EMBED Equation.3 1415. Результатом применения машины к слову является слово 13 EMBED Equation.3 1415, которое соответствует заключительной конфигурации. Если же машина, начав работу на слове 13 EMBED Equation.3 1415, никогда не останавливается, то говорят, что она не применима к слову 13 EMBED Equation.3 1415.

Пример. Пусть машина Тьюринга задана программой:
13 EMBED Equation.3 1415.
Рассмотрим записанные в последовательных n ячейках n единиц.
Пусть, например, начальная конфигурация имеет вид:
13 EMBED Equation.3 1415.
Сокращенно эту конфигурацию можно записать так:
13 EMBED Equation.3 1415.
Вообще, записанные подряд n единиц обозначаются 13 EMBED Equation.3 1415, а записанные подряд m нулей – 13 EMBED Equation.3 1415.
Тогда в каждом такте машина Тьюринга будет оставлять обозреваемую единицу на месте и сдвигаться вправо на одну ячейку. Процесс будет продолжаться до тех пор, пока управляющая головка не выйдет на пустую ячейку (0). Здесь, согласно программе, в ячейку будет вписана единица, и машина остановится. В результате на ленте будет записано n+1 единиц. Если условиться, что исходное слово выражает число n, то можно считать, что машина вычисляет функцию 13 EMBED Equation.3 1415.

Пример. Дана машина Тьюринга:
13 EMBED Equation.3 1415.
Выяснить, применима ли машина к слову 13 EMBED Equation.3 1415:
а)13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.
Если применима, то выписать результат 13 EMBED Equation.3 1415 применения машины 13 EMBED Equation.3 1415 к слову13 EMBED Equation.3 1415. Предполагается, что в начальный момент времени головка машины обозревает самую левую единицу слова.
Решение. а) Применяя машину 13 EMBED Equation.3 1415 к слову13 EMBED Equation.3 1415, получаем последовательность конфигураций:
1) 13 EMBED Equation.3 1415.
3) 13 EMBED Equation.3 1415.

2) 13 EMBED Equation.3 1415.
4) 13 EMBED Equation.3 1415.

Вид второй конфигурации обусловлен тем, что символ 0 считается пустым символом и может не записываться.
Поскольку команда вида 13 EMBED Equation.3 1415 в программе отсутствует, то последняя конфигурация является заключительной. Следовательно, машина 13 EMBED Equation.3 1415 к слову 13 EMBED Equation.3 1415 применима, и 13 EMBED Equation.3 1415. (Нули слева и справа от слова не записываются).

б) Получаем конфигурации:
1) 13 EMBED Equation.3 1415.
6) 13 EMBED Equation.3 1415.

2) 13 EMBED Equation.3 1415.
7) 13 EMBED Equation.3 1415.

3) 13 EMBED Equation.3 1415.
8) 13 EMBED Equation.3 1415.

4) 13 EMBED Equation.3 1415.
9) 13 EMBED Equation.3 1415.

5) 13 EMBED Equation.3 1415.
. . . . . .

Процесс продолжается неограниченно, головка смещается по ленте вправо до бесконечности, следовательно, машина 13 EMBED Equation.3 1415 к слову 13 EMBED Equation.3 1415 неприменима.
Вид конфигурации 8) обусловлен тем, что символ 0 (пустой символ) находится справа от последней единицы слова по умолчанию.

Машины Тьюринга 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 называются эквивалентными, если:
13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 либо обе применимы, либо обе неприменимы к каждому исходному слову 13 EMBED Equation.3 1415;
если обе машины применимы к слову 13 EMBED Equation.3 1415, то 13 EMBED Equation.3 141513 EMBED Equation.3 1415.

Программу для машины Тьюринга можно задать не только с помощью последовательности команд, но и в виде таблицы. Так, в последнем примере программа может быть задана в виде:


13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

0
13 EMBED Equation.3 1415
-

1
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415


При табличной записи командой иногда называют выражение 13 EMBED Equation.3 1415.
Имеет место следующий тезис.

Тезис Тьюринга. Всякий алгоритм может быть реализован соответствующей машиной Тьюринга.

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

В 13 REF _Ref104648548 \h 14Содержание.15




Операции с машинами Тьюринга.

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

Принцип двойственности.

Пусть Т – произвольная программа (машина Тьюринга). Обозначим Т* программу, которая получается из Т заменой (во всех командах) R на L и наоборот. Программа Т* называется двойственной к Т.

Пример. Машина Тьюринга в произвольной записи, начиная с любой ячейки, двигаясь вправо, находит первый нуль. Соответствующая программа имеет вид:
13 EMBED Equation.3 1415.
Возможны три случая.
В начальный момент головка машины обозревает нуль. Машина останавливается.
В начальный момент головка машины обозревает единицу, и справа от начальной ячейки есть хотя бы один нуль. Машина переместит головку через массив единиц вправо и остановится перед первым нулем.
В начальный момент головка машины обозревает единицу, и справа от начальной ячейки запись состоит только из единиц. Машина будет перемещать головку через массив единиц вправо, не останавливаясь.
В программе заменим символ R на L. Получим программу:
13 EMBED Equation.3 1415.
Данная программа будет двойственной к предыдушей. Непосредственной проверкой можно убедиться, что головка машины, двигаясь влево, будет отыскивать первый нуль.

Очевидно, что (Т*)*=Т, то есть понятие двойственности является взаимным. Машины Тьюринга, соответствующие двойственным программам, будем называть двойственными машинами Тьюринга.
Из примера было видно, что двойственные машины функционируют симметричным образом. Так, пусть в начальный момент времени имеется конфигурация
13 EMBED Equation.3 1415,
и машина Т в момент времени t переработает ее в конфигурацию
13 EMBED Equation.3 1415.
В то же время, двойственная машина Т* конфигурацию
13 EMBED Equation.3 1415
(симметричную первой конфигурации относительно 13 EMBED Equation.3 1415) в момент времени t переработает в конфигурацию
13 EMBED Equation.3 1415,
симметричную второй конфигурации относительно 13 EMBED Equation.3 1415.

В 13 REF _Ref104648548 \h 14Содержание.15



Способы композиции машин Тьюринга.

Последовательное подключение одной машины Тьюринга к другой. Пусть 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 – две машины Тьюринга над алфавитом {0,1}, множества состояний машин не пересекаются. Перенумеруем 0,1,,l-1 все команды с 13 EMBED Equation.3 1415 программы 13 EMBED Equation.3 1415. Пусть p(x) – предикат на множестве {0,1,,l-1}. Последовательное подключение 13 EMBED Equation.3 1415 к 13 EMBED Equation.3 1415 (относительно предиката p(x)) – это машина Тьюринга 13 EMBED Equation.3 1415, которая получается следующим образом. Первая половина таблицы для 13 EMBED Equation.3 1415 совпадает с таблицей 13 EMBED Equation.3 1415 для тех клеток, в которых нет команды с 13 EMBED Equation.3 1415.
Если p(n)=1, то в клетке n – команда 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415 – номер строки (0 или 1), где находится клетка n, 13 EMBED Equation.3 1415 – начальное состояние 13 EMBED Equation.3 1415.
Если p(n)=0, то в клетке n – команда с 13 EMBED Equation.3 1415. Вторая половина таблицы Т полностью совпадает с таблицей 13 EMBED Equation.3 1415.


13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415
13 EMBED Equation.3 141513 EMBED Equation.3 141513 EMBED Equation.3 1415

0



1




В частном случае, если 13 EMBED Equation.3 1415 – начальное состояние машины 13 EMBED Equation.3 1415, а 13 EMBED Equation.3 1415 – начальное состояние 13 EMBED Equation.3 1415, заменим в программе 13 EMBED Equation.3 1415 состояние 13 EMBED Equation.3 1415 на состояние 13 EMBED Equation.3 1415, и полученную программу объединим с программой 13 EMBED Equation.3 1415. В результате мы получим программу для машины 13 EMBED Equation.3 1415, которая является композицией машин 13 EMBED Equation.3 1415и 13 EMBED Equation.3 1415 по паре состояний (13 EMBED Equation.3 1415,13 EMBED Equation.3 1415).

Итерация машины Тьюринга. Пусть 13 EMBED Equation.3 1415 – машина Тьюринга над алфавитом {0,1}. Перенумеруем 0,1,,l-1 все команды с 13 EMBED Equation.3 1415 программы 13 EMBED Equation.3 1415. Пусть p(x) – предикат на множестве {0,1,,l-1}. Итерация машины Тьюринга 13 EMBED Equation.3 1415 относительно предиката p(x) – это машина Тьюринга Т, которая получается следующим образом. Таблица Т совпадает с таблицей 13 EMBED Equation.3 1415 для тех клеток, в которых нет команды не с 13 EMBED Equation.3 1415.
Если p(n)=1, то в клетке n – команда 13 EMBED Equation.3 1415, a – номер строки, где находится клетка n, 13 EMBED Equation.3 1415 – начальное состояние 13 EMBED Equation.3 1415.
Если p(n)=0, то в клетке n – команда с 13 EMBED Equation.3 1415.
Действительно, имеет место итерация, т.е. многократная работа машины 13 EMBED Equation.3 1415.
В частном случае, если 13 EMBED Equation.3 1415 – заключительное состояние машины 13 EMBED Equation.3 1415, а 13 EMBED Equation.3 1415 – любое состояние машины 13 EMBED Equation.3 1415, не являющееся заключительным, то заменим в программе 13 EMBED Equation.3 1415 состояние 13 EMBED Equation.3 1415 на состояние 13 EMBED Equation.3 1415. В результате мы получим программу для машины Т, которая является итерацией машины 13 EMBED Equation.3 1415 по паре состояний (13 EMBED Equation.3 1415,13 EMBED Equation.3 1415).
Отметим, что начальных и заключительных состояний может быть несколько.

В 13 REF _Ref104648548 \h 14Содержание.15





Задачи.

По заданной машине Тьюринга 13 EMBED Equation.3 1415 и начальной конфигурации 13 EMBED Equation.3 1415 найти заключительную конфигурацию:
13 EMBED Equation.3 1415; 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415; 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415; 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415;13 EMBED Equation.3 1415.
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
· Выяснить, применима ли машина Тьюринга 13 EMBED Equation.3 1415 к слову 13 EMBED Equation.3 1415. Если применима, то записать результат 13 EMBED Equation.3 1415 применения машины 13 EMBED Equation.3 1415 к слову13 EMBED Equation.3 1415. Предполагается, что в начальный момент времени головка машины обозревает самую левую единицу слова.
1) 13 EMBED Equation.3 1415; а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.
2) 13 EMBED Equation.3 1415; а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415; а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.
4) 13 EMBED Equation.3 1415; а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.
5) 13 EMBED Equation.3 1415; а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.

3. Построить в алфавите {0,1} машину Тьюринга, обладающую свойствами:
машина имеет одно состояние, одну команду и применима к любому слову в алфавите {0,1};
машина имеет одно состояние, две команды, не применима ни к какому слову в алфавите {0,1}, и в процессе работы головка обозревает бесконечное множество ячеек;
машина имеет две команды, не применима ни к какому слову в алфавите {0,1}, и в процессе работы головка обозревает одну ячейку.
Предполагается, что в начальный момент времени головка машины обозревает самый левый символ слова.

4. По словесному описанию машины Тьюринга построить ее программу (в алфавите {0,1}).
Начав работу с первой единицы массива из единиц, машина “сдвигает” его на две ячейки вправо, не изменяя остального содержимого ленты, и останавливается на последней единице перенесенного массива.
Начав двигаться влево от произвольной ячейки, головка находит первую при таком перемещении ячейку с единицей (если такая встретится на пути) и, сделав один шаг вправо, останавливается на соседней ячейке. Содержимое ленты не меняется.
Машина начинает работу с самой левой непустой ячейки и отыскивает нуль, примыкающий с левой стороны к первому справа массиву из трех единиц, окаймленному нулями. Головка останавливается на первой единице найденного массива (если такой есть). Содержимое ленты не меняется.
Головка машины, начав работу с произвольной ячейки, содержащей единицу, двигается влево до тех пор, пока не пройдет подряд пять нулей. Головка останавливается на первой ячейке слева за этими пятью нулями, напечатав в ней единицу. Остальное содержимое ленты не меняется.
При заданном 13 EMBED Equation.3 1415 головка машины, начав работу с произвольной ячейки и двигаясь вправо, записывает подряд 13 EMBED Equation.3 1415 нулей и останавливается на последнем из них.
Головка машины, двигаясь вправо от какой-либо пустой ячейки, находит первый при таком перемещении массив, содержащий не менее семи единиц, стирает в нем первые семь единиц и останавливается на самой правой из ячеек, в которых были стерты единицы. Остальное содержимое ленты не меняется.
При заданном значении n головка машины из n записанных единиц оставляет на ленте 13 EMBED Equation.3 1415 единицы, так же записанных подряд, если 13 EMBED Equation.3 1415, и работает вечно, если 13 EMBED Equation.3 1415 или 13 EMBED Equation.3 1415.
Машина реализует алгоритм вычисления функции 13 EMBED Equation.3 1415, считая, что число n представляется записанными подряд n единицами, и массив из n единиц уже найден.
Машина реализует алгоритм вычисления функции 13 EMBED Equation.3 1415, считая, что число n представляется записанными подряд n единицами, и массив из n единиц уже найден.
Машина реализует алгоритм вычисления функции 13 EMBED Equation.3 1415
Считается, что число n представляется записанными подряд n единицами, и массив из n единиц уже найден.
Показать, что для всякой машины Тьюринга существует эквивалентная ей машина, в программе которой отсутствуют заключительные состояния.
Показать, что для всякой машины Тьюринга существует эквивалентная ей машина, в программе которой отсутствует символ E.

5. Для машин Тьюринга из задачи 1 построить двойственные машины.

6. Построить композицию 13 EMBED Equation.3 1415 машин Тьюринга 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415 по паре состояний (13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415) и найти результат применения композиции 13 EMBED Equation.3 1415 к слову 13 EMBED Equation.3 1415.
1)

13 EMBED Equation.3 1415
13 EMBED Equation.3 1415


13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

13 EMBED Equation.3 1415:
0
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
, 13 EMBED Equation.3 1415:
0
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415


1
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

1
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.

3)

13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

13 EMBED Equation.3 1415:
0
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415


1
13 EMBED Equation.3
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.

7. Найти результат применения итерации машины 13 EMBED Equation.3 1415 по паре состояний (13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415) к слову 13 EMBED Equation.3 1415(заключительными состояниями являются 13 EMBED Equation.3 1415 и 13 EMBED Equation.3 1415).



13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415

13 EMBED Equation.3 1415:
0
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415


1
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
13 EMBED Equation.3 1415
-
-

а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.




13 EMBED Equation.3 1415
13 EMBED Equati
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·–
·
·
·
·
·
·
·
·
·
а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415.

В 13 REF _Ref103424706 \h 14Ответы и указания.15
В 13 REF _Ref104648548 \h 14Содержание.15






Ответы и указания.

13 REF _Ref104031611 \h 14Глава 1. Высказывания, формулы, тавтологии.15 2. 2), 5), 8), 10) – истинные высказывания. 1), 4), 7) – ложные высказывания. 3), 6) высказываниями не являются. 3. Обратите внимание, что 7) – составное высказывание. 5. Не являются тавтологиями: 2), 3), 5). Вернуться в 13 REF _Ref104031651 \h 14Задачи.15
13 REF _Ref100762967 \h 14Глава 3. Исчисление высказываний.15 1. 1), 2), 5), 7), 8), 9) – формулы исчисления высказываний. 3), 4), 6), 10) формулами исчисления высказываний не являются. 2. 2). 3. 5) Применить лемму. 6), 7), 9) – применить результат 5). 8), 10), 11), 12) – применить результат 9). Вернуться в 13 REF _Ref100763075 \h 14Задачи.15
13 REF _Ref103423939 \h 14Глава 5. Предикаты.15 1. 1)13 EMBED Equation.3 1415. 3) 13 EMBED Equation.3 1415. 5) 13 EMBED Equation.3 1415. 7) 13 EMBED Equation.3 1415. 8) 13 EMBED Equation.3 1415. 9) 13 EMBED Equation.3 1415. 10) 13 EMBED Equation.3 1415. 2. 1), 3), 4), 6), 7), 9), 10). 1. 2), 5), 8). 0. 3. 7) Воспользоваться формулой 13 EMBED Equation.3 1415.
4. 1)13 EMBED Equation.3 1415.
2) 13 EMBED Equation.3 1415. 3) 13 EMBED Equation.3 1415.
4) 13 EMBED Equation.3 1415. 5) 13 EMBED Equation.3 1415.
6) 13 EMBED Equation.3 1415. 7) 13 EMBED Equation.3 1415.
8) 13 EMBED Equation.3 1415.
9) 13 EMBED Equation.3 1415.
10) 13 EMBED Equation.3 1415. 8. Можно привести такой пример: 13 EMBED Equation.3 1415, 13 EMBED Equation.3 1415. Предикаты рассматриваются на множестве 13 EMBED Equation.3 1415. Вернуться в 13 REF _Ref103423996 \h 14Задачи.15
13 REF _Ref103424314 \h 14Глава 8. Рекурсивные функции.15 1. 1) 13 EMBED Equation.3 1415. 2) 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415 4) 13 EMBED Equation.3 1415. 5) 13 EMBED Equation.3 1415. 6) 13 EMBED Equation.3 1415. 7) 13 EMBED Equation.3 1415.
8) 13 EMBED Equation.3 1415 9) 13 EMBED Equation.3 1415
10)13 EMBED Equation.3 1415 Вернуться в 13 REF _Ref104974680 \h 14Задачи.15
13 REF _Ref103424463 \h 14Глава 9. Машины Тьюринга.15 1. 1) 13 EMBED Equation.3 1415. 2) 13 EMBED Equation.3 1415. 3) 13 EMBED Equation.3 1415. 4) 13 EMBED Equation.3 1415. 5) 13 EMBED Equation.3 1415. 6) 13 EMBED Equation.3 1415. 7) 13 EMBED Equation.3 1415. 8) 13 EMBED Equation.3 1415. 9) 13 EMBED Equation.3 1415.
13 EMBED Equation.3 1415. 2. 1) а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415. 2) а) Неприменима;
б) 13 EMBED Equation.3 1415. 3) а); б) Неприменима. 4) а) 13 EMBED Equation.3 1415; б) Неприменима. 5) а) Неприменима; б) 13 EMBED Equation.3 1415. 6. 1) а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415. 2) а) 13 EMBED Equation.3 1415;
б) 13 EMBED Equation.3 1415. 3) а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415. 7. 1) а) 13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415. 2) а)13 EMBED Equation.3 1415; б) 13 EMBED Equation.3 1415. Вернуться в 13 REF _Ref103424670 \h 14Задачи.15

В 13 REF _Ref104648548 \h 14Содержание.15





Литература.

Бочкарева О.В. Учебное пособие по математике (специальные главы). М., Радио и связь, 2001.
Гаврилов Г.П., Сапоженко А.А. Задачи и упражнения по курсу дискретной математики. М., Наука, 1992.
Горбатов В.А. Фундаментальные основы дискретной математики. М., Наука, 2000.
Кузнецов О.П., Адельсон-Вельский Г.М. Дискретная математика для инженеров. М., Энергоатомиздат, 1988.
Кук Д., Бейз Г. Компьютерная математика. М., Наука,1990.
Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. М., ФИЗМАТЛИТ, 2001.
Логинов Б.М. Введение в дискретную математику. Калуга, 1998.
Лихтарников Л.М., Сукачева Т.Г. Математическая логика. Курс лекций. Задачник-практикум и решения. СПб, Лань, 1999.
Математическая энциклопедия. Т. 1. М., Советская Энциклопедия, 1977.
Мендельсон Э. Введение в математическую логику. М., Наука, 1984.
Непейвода Н.Н. Прикладная логика. Новосибирск, Изд-во Новосибирского университета, 2000.
Новиков Ф.А. Дискретная математика для программистов. СПб, Питер, 2000.
Тишин В.В. Теория алгоритмов, предикаты. Самара, 2001.
Фролов И.С. Элементы математической логики. Самара, Самарский университет, 2001.
Яблонский С.В. Введение в дискретную математику. М., Высшая школа, 2001.

В 13 REF _Ref104648548 \h 14Содержание.15


13PAGE 1412915


13PAGE 1413115








Root EntryEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation NativeEquation Native

Приложенные файлы

  • doc 371037
    Размер файла: 3 MB Загрузок: 0

Добавить комментарий