Читать онлайн «Дискретный анализ. Формальные системы и алгоритмы»

Ю. И. Журавлёв, Ю. А. Флёров, М. Н. Вялый ДИСКРЕТНЫЙ АНАЛИЗ. ФОРМАЛЬНЫЕ СИСТЕМЫ И АЛГОРИТМЫ Рекомендовано Учебно-методическим объединением высших учебных заведений Российской Федерации по образованию в области прикладных математики и физики в качестве учебного пособия по направлению «Прикладные математика и физика» Москва 2010 УДК 510. 51 ББК 22. 12 Ж 91 Серия «Естественные науки. Математика. Информатика» Ответственный секретарь серии Лобанов А. И. Рецензенты: Докт. физ. -мат. наук, проф. В. К. Леонтьев (ВЦ РАН) Кафедра высшей математики МГУТУ Ю. И. Журавлёв и др. Ж 91 Дискретный анализ. Формальные системы и алго- ритмы: Учебное пособие. / Ю. И. Журавлёв, Ю. А. Флёров, М. Н. Вялый – М: ООО Контакт Плюс, 2010. – 336 с. : ил. ISBN 978–5–86567–092–1 Эта книга является учебным пособием по математиче- ской логике и теории алгоритмов. Она написана на основе материалов курса «Дискретный анализ», читаемого многие годы для студентов факультета управления и прикладной математики Московского физико-технического института. Для студентов, специализирующихся на прикладной математике. УДК 510. 51 ББК 22. 14 c Ю. И. Журавлёв, 2010 c В. А. Музыченко, ISBN 978–5–86567–092–1 дизайн обложек серии, 2007 Оглавление Введение 7 1. Исчисление высказываний 14 1. 1. Определение формальной системы ИВ 15 1. 1. 1. Алфавит . . . . . . . . . . . . . . 15 1. 1. 2. Формулы . . . . . . . . . . . . . . 16 1. 1. 3. О структуре формул . . . . . . . 18 1. 1. 4. Сокращения при записи формул 23 1. 1. 5. Аксиомы . . . . . . . . . . . . . . 24 1. 1. 6. Правило вывода . . . . . . . . . . 24 1. 1. 7. Выводы и выводимые формулы 25 1. 2. Исчисление высказываний и булевы функции . . . . . . . . . . . . . . . . . . 28 1. 3. Непротиворечивость ИВ . . . . . . . . . 31 1. 4. Теорема дедукции . . . . . . . . . . . . . 34 1. 5. Теорема о полноте . . . . . . . . . . . . 39 1. 5. 1. Первое доказательство . . . . . . 40 1. 5. 2. Второе доказательство . . . . . . 44 1. 5. 3. Критерий условной выводимости 48 1. 6. Независимость аксиом ИВ . . . . . . . . 51 1. 7. Другие аксиоматизации . . . . . . . . . 57 1. 8. Метод резолюций . . . . . . . . . . . . . 60 1. 8. 1. КНФ . . . . . . . . . . . . . . . . 61 1. 8. 2. Резолютивный вывод . . . . . . . 63 4 Оглавление 1. 8. 3. Синтаксическое дерево и допу- стимое дерево . . . . . . . . . . . 66 1. 8. 4. Сравнение метода резолюций и ИВ . . . . . . . . . . . . . . . . . 68 2. Интуиционистское исчисление 71 2. 1.