ББКУДК 510.6
22.12
А18
Калягин В. А. — доктор физико-математических наук, профессор НИУ ВШЭ
Петренко А. К. — доктор технических наук, профессор,
заведующий отделом «Технологии программирования»
Института системного программирования РАН
Ре цензенты:
Захаров В. А. — доктор физико-математических наук,
профессор МГУ им. М. В. Ломоносова
На у чный р едак т ор:
А18 Дискретная математика. Формально-логические системы и языки. – М.:
ДМК Пресс, 2018. – 390 с.: ил.
Авдошин С. М., Набебин А. А.
ISBN 978-5-97060-622-3
Книга содержит основные сведения из формально-логических систем. Это функции алгебры
логики (булевы функции), теорема Поста о функциональной полноте, k-значные логики,
производные булевых функций, аксиоматические исчисления высказываний, предикатов,
секвенций, резолюций и язык программирования Пролог. Рассматриваются монадическая
логика, конечные автоматы и представимые ими языки, темпоральная логика, аксиоматический
язык программирования OBJ3.
В основу книги положен многолетний опыт преподавания авторами дисциплины «Дискретная
математика» на факультете бизнес-информатики, на факультете компьютерных наук
Национального исследовательского университета Высшая школа экономики и на факультете
автоматики и вычислительной техники Национального исследовательского университета
Московский энергетический институт.
Книга предназначена для студентов бакалавриата, обучающихся по направлениям 09.03.01
«Информатика и вычислительная техника», 09.03.02 «Информационные системы и технологии»,
09.03.03 «Прикладная информатика», 09.03.04 «Программная инженерия», а также для
ИТ-специалистов и разработчиков программных продуктов.
УДК 510.6
ББК 22.12
Все права защищены. Любая часть этой книги не может быть воспроизведена в кавлкой
бы то ни было форме и какими бы то ни было средствами без письменного разрешения
адельцев авторских прав.
ISBN 978-5-97060-622-3
© Авдошин С. М., Набебин А. А., 2018
© Оформление, издание, ДМК Пресс, 2018
Стр.3
Содержание
Предисловие .......................................................................................................................................... 9
Введение .................................................................................................................................................13
Часть I. АЛГЕБРА ЛОГИКИ И ПРЕДИКАТЫ ..................................................................27
Глава 1. Алгебра логики .................................................................................................................28
1.1. Функции алгебры логики ...........................................................................................................28
1.2. Формулы. Реализация функций формулами ......................................................................29
1.3. Равносильные преобразования формул .............................................................................31
1.4. Нормальные формы. Совершенные нормальные формы ............................................33
Совершенные нормальные формы ..........................................................................................34
1.5. Минимизация нормальных форм ...........................................................................................36
1.5.1. Алгоритм Куайна построения сокращенной ДНФ ..................................................38
1.5.2. Алгоритм построения сокращенной ДНФ с помощью КНФ ...............................39
1.5.3. Построение всех тупиковых ДНФ ..................................................................................41
1.5.4. Алгоритм минимизации функций в классе ДНФ .....................................................42
1.5.5. Алгоритм минимизации функций в классе КНФ .....................................................43
1.5.6. Алгоритм минимизации функций в классе нормальных форм .........................43
1.6. Минимизация частично определенных функций ............................................................45
1.6.1. Алгоритм минимизации частично определенных функций
в классе ДНФ .....................................................................................................................................46
1.6.2. Алгоритм минимизации частично определенных функций
в классе КНФ .....................................................................................................................................46
1.7. Двойственные функции. Принцип двойственности .........................................................49
1.8. Линейные функции .......................................................................................................................50
1.9. Монотонные функции ..................................................................................................................53
1.10. Теорема Поста о функциональной полноте .....................................................................55
1.11. Предполные классы ...................................................................................................................58
Глава 2. Функции k-значной логики .......................................................................................60
2.1. Функции и отношения .................................................................................................................60
2.2. Самодвойственные функции ....................................................................................................63
2.3. Монотонные функции ..................................................................................................................63
2.4. Линейные функции .......................................................................................................................64
2.5. Функции, сохраняющие разбиение .......................................................................................64
2.6. Классы типа ℂ .................................................................................................................................64
Стр.4
4 Содержание
2.7. Классы типа 𝔹 .................................................................................................................................65
2.8. Сравнение функций двузначной и многозначной логик ..............................................66
Глава 3. Производные булевой функции в синтезе логических схем ...............67
3.1. Производная булевой функции ...............................................................................................67
3.2. Синтез логических схем методом каскадов .......................................................................70
3.3. Разложение булевой функции в ряд .....................................................................................77
Глава 4. Синтез схем из функциональных элементов .................................................80
4.1. Схема из функциональных элементов .................................................................................80
4.2. Функции Шеннона ........................................................................................................................82
4.3. Элементарные методы синтеза схем ....................................................................................82
4.4. Синтез мультиплексоров ............................................................................................................84
4.5. Элементы функциональной декомпозиции .......................................................................86
4.6. Обнаружение неисправностей в схемах .............................................................................91
Глава 5. Аксиоматическое исчисление высказываний ...............................................94
5.1. Определение исчисления высказываний ...........................................................................94
5.2. Теорема дедукции в исчислении высказываний ............................................................98
5.3. Производные правила вывода .............................................................................................100
5.4. Тождественно истинные и доказуемые формулы .........................................................105
5.5. Разрешимость, непротиворечивость, полнота, независимость аксиом ................108
5.6. Формулировка исчисления высказываний с единственным правилом
вывода – правилом заключения ..................................................................................................111
Глава 6. Логика предикатов ......................................................................................................113
6.1. Предикаты, кванторы ................................................................................................................113
6.2. Общезначимость, выполнимость, невыполнимость, опровержимость
формул логики предикатов ............................................................................................................115
6.3. Равносильность формул ..........................................................................................................119
6.4. Нормальные формы ..................................................................................................................121
6.4.1. Префиксная нормальная форма .................................................................................121
6.4.2. Стандартная форма Сколема ........................................................................................122
6.5. Проблема разрешимости в логике предикатов .............................................................125
6.5.1. Проблема разрешимости $-формул ..........................................................................126
6.5.2. Проблема разрешимости ∀-формул ......................................................................... 127
6.5.3. Проблема разрешимости монадической логики ................................................128
6.6. Отношения ....................................................................................................................................130
6.7. Суперпозиция функций ............................................................................................................132
6.8. Операции Мальцева над функциями .................................................................................133
6.9. Алгебра отношений (реляционная алгебра) ....................................................................133
6.10. Алгебра отношений k-значной логики ............................................................................135
Стр.5
Содержание 5
Глава 7. Аксиоматическое исчисление предикатов ...................................................136
7.1. Определение исчисления предикатов ...............................................................................136
7.2. Теорема дедукции в исчислении предикатов .................................................................138
7.3. Непротиворечивость исчисления предикатов ................................................................141
7.4. Семантическая полнота исчисления предикатов относительно класса
общезначимых формул ....................................................................................................................142
7.4.1. Непротиворечивые расширения исчисления предикатов ...............................143
7.4.2. Формализмы G и Gk ...............................................................................................................................................................................................145
Глава 8. Исчисление секвенций .............................................................................................151
8.1. О правилах вывода в секвенциальном исчислении высказываний .....................151
8.2. Секвенциальное исчисление высказываний ..................................................................155
8.3. Секвенциальное исчисление предикатов .......................................................................158
Глава 9. Метод резолюций в логике предикатов и Пролог ..................................161
9.1. Метод резолюций в логике высказываний .....................................................................161
9.1.1. Семантическое дерево ....................................................................................................162
9.1.2. Правило резолюции .........................................................................................................164
9.2. Эрбрановы универсум, базис, интерпретация ............................................................... 167
9.3. Семантические деревья. Теорема Эрбрана .....................................................................170
9.4. Унификация ...................................................................................................................................174
9.5. Метод резолюций в логике предикатов ........................................................................... 177
9.6. Основы Пролога ..........................................................................................................................182
9.6.1. Унификация в Прологе ....................................................................................................189
9.6.2. Декларативный и операторный смысл Пролог-программы ............................191
9.6.3. Бэктрекинг и оператор отсечения ..............................................................................193
9.6.4. Объявление операторов .................................................................................................194
9.7. Примеры программ и вычислений в Прологе ................................................................196
9.7.1. Принадлежность элемента списку ..............................................................................196
9.7.2. Первый элемент в списке ...............................................................................................199
9.7.3. Последний элемент в списке ........................................................................................200
9.7.4. Следующий элемент в списке .......................................................................................201
9.7.5. Соединение списков .........................................................................................................204
9.7.6. Обращение списка ............................................................................................................205
9.7.7. Выравнивание списка.......................................................................................................206
9.7.8. Добавление элемента в начало списка ....................................................................206
9.7.9. Удаление первого вхождения данного элемента из списка ............................ 207
9.7.10. Удаление всех вхождений данного элемента из списка ................................ 207
9.7.11. Замена элемента в списке ...........................................................................................210
9.7.12. Быть подсписком в списке ...........................................................................................210
9.7.13. Включение множеств .....................................................................................................212
Стр.6
6 Содержание
9.7.14. Равенство множеств .......................................................................................................213
9.7.15. Объединение множеств ................................................................................................213
9.7.16. Пересечение множеств .................................................................................................215
9.7.17. Разность множеств ...........................................................................................................215
9.7.18. Декартово произведение множеств ........................................................................215
9.7.19. Множество всех подмножеств данного множества ..........................................216
9.7.20. Удаление всех повторов элементов в списке ......................................................216
9.7.21. Принадлежность множества списку подмножеств ............................................216
9.7.22. Удаление всех повторов подмножеств в данном списке множеств ...........216
9.7.23. Удаление повторов атомов в списке списков атомов ...................................... 217
9.7.24. Последовательное порождение нумерованных атомов ................................. 217
9.7.25. Программа построения сокращенной ДНФ по конъюнктивной
нормальной форме ...................................................................................................................... 217
9.7.26. Программа построения сокращенной ДНФ по конъюнктивной
нормальной форме без отрицаний .......................................................................................219
9.8. Некоторые встроенные предикаты Пролога ..................................................................220
9.8.1. Средства управления .......................................................................................................220
9.8.2. Классификация термов ...................................................................................................221
9.8.3. Унификация термов ..........................................................................................................221
9.8.4. Сравнение термов .............................................................................................................221
9.8.5. Арифметические функции .............................................................................................222
9.8.6. Арифметические предикаты .........................................................................................222
9.8.7. Обработка термов ..............................................................................................................223
9.8.8. Работа со стрингами .........................................................................................................223
9.8.9. Составление списков .......................................................................................................223
9.8.10. Взаимодействие с базой данных .............................................................................224
9.8.11. Стандартные ввод и вывод .........................................................................................225
9.8.12. Доступ к файлам ..............................................................................................................226
9.8.13. Стандартный доступ к файлам в Прологе .............................................................226
9.8.14. Движение в файле .......................................................................................................... 227
9.8.15. Исполнение системных функций ............................................................................. 227
9.8.16. Отладчик (Debugger) ...................................................................................................... 227
Часть II. МОНАДИЧЕСКАЯ ЛОГИКА И КОНЕЧНЫЕ АВТОМАТЫ ...........................230
Глава 10. Конечные автоматы ................................................................................................231
10.1. Автоматы Мили и Мура .........................................................................................................231
10.2. Источники ...................................................................................................................................235
10.3. Регулярные языки и регулярные выражения ...............................................................240
10.3.1. Операции Клини и регулярные языки ...................................................................240
10.3.2. Алгебра регулярных выражений Клини ................................................................242
10.4. Теоремы замкнутости для класса автоматно представимых языков .................243
Стр.7
Содержание 7
10.5. Минимизация числа состояний автомата с выходом ...............................................248
10.5.1. Склеивание неразличимых состояний ...................................................................250
10.5.2. Алгоритм минимизации автомата ............................................................................250
10.5.3. Алгоритм разбиения множества состояний на классы
неотличимых состояний .............................................................................................................254
10.5.4. Алгоритм проверки эквивалентности автоматов ..............................................255
Глава 11. Автоматы и сверхъязыки .....................................................................................257
11.1. Макроавтоматы......................................................................................................................... 257
11.2. Конкатенация языка и сверхъязыка ................................................................................259
11.3. Сверхитерация автоматных языков .................................................................................261
11.4. Детерминизация макроисточника ....................................................................................264
Глава 12. Проблема униформизации .................................................................................267
12.1. Языки и операторы ................................................................................................................. 267
12.2. Игры...............................................................................................................................................270
12.3. Стратегии .....................................................................................................................................273
12.4. Униформизация конечноавтоматных языков ..............................................................276
12.4.1. Порядковые векторы и порядковые стратегии ..................................................276
12.4.2. Теоремы о порядковых стратегиях ..........................................................................278
12.4.3. Пример построения выигрывающего автомата .................................................282
Глава 13. Монадическая логика натуральных чисел ................................................285
13.1. Монадическая логика ............................................................................................................285
13.2. Выразимость в монадической логике ............................................................................. 287
13.2.1. Макроисточники и монадическая логика ............................................................289
13.2.2. Регулярные языки и монадическая логика ..........................................................289
13.2.3. Общерегулярные языки и монадическая логика ..............................................290
13.3. Специальная префиксная форма ......................................................................................290
13.4. Синтез автомата по формуле монадической логики ................................................292
13.5. Алгоритмическая разрешимость монадической логики ..........................................294
Глава 14. Темпоральная логика ..............................................................................................296
14.1. Пропозициональная темпоральная логика ...................................................................296
14.2. Интерпретация формул ......................................................................................................... 297
14.3. Общезначимость, выполнимость, опровержимость, невыполнимость ..............299
14.4. Другие темпоральные операторы .....................................................................................302
14.5. Аксиоматическая система ....................................................................................................304
14.6. Спецификация свойств формулами .................................................................................305
14.7. Спецификация взаимодействия и параллелизма .......................................................306
Стр.8
8 Содержание
Глава 15. Аксиоматический язык программирования OBJ3 .................................310
15.1. Описание языка ........................................................................................................................310
15.2. Спецификация объекта..........................................................................................................311
15.3. Сорта и подсорта ......................................................................................................................312
15.4. Импорт модулей .......................................................................................................................312
15.5. Встроенные сорта ....................................................................................................................314
15.6. Декларация атрибутов ...........................................................................................................314
15.7. Приоритет ...................................................................................................................................315
15.8. Параметризованное программирование ......................................................................315
15.9. Теории ...........................................................................................................................................316
15.9.1. Программная спецификация FIELD алгебраического поля ..........................316
15.9.2. Программная спецификация PROPC пропозиционального
исчисления ....................................................................................................................................... 317
15.9.3. Программная спецификация SET-NAT множества натуральных
чисел ...................................................................................................................................................318
15.9.4. Программная спецификация obj WORDTREE дерева слов ............................319
15.9.5. Программная спецификация WORDSTACK словарого стека .........................320
15.9.6. View .......................................................................................................................................321
15.9.7. Инстанциация ...................................................................................................................321
15.9.8. Параметризованная теория линейного векторного пространства ............321
15.9.9. Параметризованный модуль obj ORD-PAIR пар вида
(натуральное число, слово) .......................................................................................................322
15.9.10. Параметризованный модуль SEQUENCE[X :: ELEMS] списков
натуральных чисел и списков слов........................................................................................323
Приложение 1. Логика высказываний и предикатов. Пролог .............................325
Приложение 2. Конечные автоматы ...................................................................................357
Приложение 3. Анализ конечных автоматов ................................................................364
Приложение 4. Синтез конечных автоматов .................................................................380
Литература ..........................................................................................................................................383
Обозначения ......................................................................................................................................386
Стр.9