Министерство образования Российской Федерации
Санкт-Петербургский государственный электротехнический
университет “ЛЭТИ”
РАБОЧАЯ ПРОГРАММА
дисциплины
МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ
Для подготовки дипломированных специалистов по направлению
654600 – “Информатика и вычислительная техника” по специальностям:
220100 – “Вычислительные машины, комплексы, системы и сети”
220300 – “Системы автоматизированного проектирования»
на открытом факультете
Санкт-Петербург
2002
Санкт-Петербургский государственный электротехнический
университет “ЛЭТИ”
“УТВЕРЖДАЮ”
Проректор по учебной работе
проф. ___________
“_____”_______________2002 г.
РАБОЧАЯ ПРОГРАММА
дисциплины
МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ
Для подготовки дипломированных специалистов по направлению
654600 – “Информатика и вычислительная техника” по специальностям:
220100 – “Вычислительные машины, комплексы, системы и сети”
220300 – “Системы автоматизированного проектирования»
на открытом факультете
Факультет компьютерных технологий и информатики
Кафедра вычислительной техники
Курс – 3
Семестр – 5
Лекции | 34 ч. | Экзамен | семестр | |
5 | ||||
Курсовая работа | 17 ч. |
Аудиторные занятия | 51 ч. |
| |
Самостоятельные занятия | 59 ч. | ||
Всего часов | 110 ч. |
|
2002
Рабочая программа обсуждена на заседании кафедры вычислительной техники “____”_______________ 2002 г., протокол № ______.
Рабочая программа согласована с рабочими программами изученных ранее дисциплин:
1) Дискретная математика
Цели и задачи дисциплины:
Цель дисциплины – ознакомление с основными понятиями и методами математической логики и теории алгоритмов с ориентацией на их использование в практической информатике и вычислительной технике.
Требования к уровню освоения дисциплины
В результате изучения дисциплины студенты должны:
1. Знать основные понятия и методы математической логики и теории алгоритмов, используемые в информатике и вычислительной технике.
2. Уметь использовать их для построения несложных логических моделей предметных областей, реализации логического вывода и оценки вычислительной сложности алгоритмов
3. Иметь представление о направлениях развития данной дисциплины и перспективах ее использования в информатике и вычислительной технике.
Содержание рабочей программы
ВВЕДЕНИЕ
Предмет курса, его связь с другими дисциплинами учебного плана, значение в подготовке специалистов по направлению "Информатика и вычислительная техника" и инженеров-системотехников по специальности 220100 – “Вычислительные машины, комплексы, системы и сети”. Обзор литературы по курсу.
Раздел 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Тема 1. Основы логики высказываний
Язык логики высказываний. Синтаксис языка: алфавит и правила построения формул. Семантика языка, интерпретация формул. Свойства формул: общезначимость, выполнимость, противоречивость.
Методы анализа выполнимости и общезначимости формул: семантическое дерево, тривиальный алгоритм, алгоритм Квайна, алгоритм редукции, алгебраический подход. Алгоритм преобразования формул в КНФ. Базовый алгоритм проверки общезначимости КНФ, модификация Девиса-Патнема.
Тема 2. Вывод в логике высказываний
Понятие логического следования, проблема дедукции. Принцип дедукции. Правило резолюций, метод резолюций. Стратегии метода резолюций.
Раздел 2. ЛОГИКА ПРЕДИКАТОВ
Тема 3. Язык логики предикатов
Синтаксис языка логики предикатов: алфавит, термы, атомы, правила построения формул. Свободные и связанные вхождения переменных, замкнутые формулы. Семантика языка логики предикатов, интерпретация формул.
Тема 4. Логический вывод в логике предикатов
Предваренная, сколемовская и клаузальная формы. Алгоритм получения клаузальной формы. Метод резолюций в логике предикатов. Теорема Робинсона. Подстановка, композиция подстановок, унификатор. Алгоритм построения наиболее общего унификатора. Хорновские дизъюнкты и метод резолюций на хорновских дизъюнктах. Принцип логического программирования.
Раздел 3. ФОРМАЛЬНЫЕ (АКСИОМАТИЧЕСКИЕ) СИСТЕМЫ
Тема 5. Основы теории формальных систем
Понятия формальной системы и формального вывода. Исчисление высказываний как формальная система, множественность аксиоматизаций. Теорема дедукции. Связь выводимости и истинности формул в логике высказываний. Исчисление предикатов как формальная система. Примеры формального вывода.
Тема 6. Метатеория формальных систем
Основные свойства формальных систем: непротиворечивость, полнота, разрешимость. Теоремы о неполноте формальных систем, смысл и значение теорем Геделя для практической информатики.
Раздел 4. ТЕОРИЯ АЛГОРИТМОВ
Тема 7. Алгоритмические системы. Алгоритмически разрешимые и неразрешимые задачи
Понятие алгоритмической системы. Частично-рекурсивные функции, тезис Черча.
Машины Тьюринга, тезис Тьюринга. Рекурсивные и рекурсивно-перечислимые множества и языки. Алгоритмически разрешимые и неразрешимые задачи. Проблема остановки, проблема пустой ленты, метод сведения.
Тема 8. Сложность алгоритмов
Меры сложности алгоритмов: временная и емкостная сложность. Асимптотическая сложность, порядок сложности. Сложность в среднем и в худшем случае.
Языки и задачи. Легко - и трудноразрешимые задачи, классы задач P и NP. NP-полные задачи. Недетерминированная машина Тьюринга (НМТ). Сложность моделирования НМТ с помощью ДМТ. Примеры NP-полных задач. Полиномиальная сводимость и полиномиальная трансформируемость. Теорема Кука. Примеры практически значимых NP-полных задач. Задача 3-выполнимости, доказательство NP-полноты методом сведения.
Тема 9. Алгоритмическая логика
Алгоритмическая логика Хоара. Предусловие и постусловие алгоритма. Тройки Хоара. Формальная постановка задачи верификации. Понятие слабейшего предусловия и его основные свойства. Верификация операторов присваивания и их последовательностей.
ЗАКЛЮЧЕНИЕ
Перспективы развития методов математической логики для решения задач спецификации и верификации программно-аппаратных средств, создания систем искусственного интеллекта и Семантического Web.
Перечень практических занятий
№ | Наименование темы занятия | Номер темы программы |
1 | Язык логики высказываний, анализ свойств логических формул. Преобразование формул в КНФ. | 1 |
2 | Метод резолюций в логике высказываний. Сравнение эффективности различных стратегий. | 2 |
3 | Язык логики предикатов. Преобразование формул в предваренную форму. | 4 |
4 | Преобразование формул логики предикатов в сколемовскую и клаузальную формы. | 4 |
5 | Метод резолюций в логике предикатов. Унификация атомов, построение наиболее общего унификатора. | 4 |
6 | Примеры логического программирования, реализация логического вывода на хорновских дизъюнктах. | 4 |
7 | Примеры формального вывода в логических исчислениях | 5 |
8 | Оценка сложности алгоритмов | 8 |
Цели и содержание курсовой работы
Цель курсовой работы – получение практических навыков алгоритмизации и программной реализации логического вывода с использованием метода резолюций, а также теоретической и экспериментальной оценки сложности построенных алгоритмов. Таким образом, курсовая работа направлена на практическое закрепление ключевых теоретических вопросов данной дисциплины как в части логики, так и в части теории алгоритмов. Содержание курсовой работы включает:
1. Разработку укрупненного алгоритма метода резолюций для заданного набора стратегий и детализированных алгоритмов отдельных процедур.
2. Теоретическую оценку сложности разработанных алгоритмов.
3. Разработку и отладку программы, экспериментальное исследование сложности алгоритмов.
Распределение учебных часов по темам и видам занятий
№ темы | Название разделов и тем | Объем учебных часов | Семестр | |||||
Лекции | Лабор. занятия | Практ. занятия | Аудит. занятия | Самост. Работа | Всего | |||
ВВЕДЕНИЕ | 1 | 1 | 1 | 3 | ||||
Раздел 1. ЛОГИКА ВЫСКАЗЫВАНИЙ | ||||||||
1 | Основы логики высказываний | 2 | 2 | 4 | 2 | 6 | 3 | |
2 | Вывод в логике высказываний | 5 | 2 | 7 | 4 | 11 | 3 | |
Раздел 2. ЛОГИКА ПРЕДИКАТОВ | ||||||||
3 | Язык логики предикатов | 4 | 4 | 2 | 6 | 3 | ||
4 | Логический вывод в логике предикатов | 6 | 8 | 14 | 6 | 20 | 3 | |
Раздел 3. ФОРМАЛЬНЫЕ (АКСИОМАТИЧЕСКИЕ) СИСТЕМЫ | ||||||||
5 | Основы теории формальных систем | 6 | 2 | 8 | 2 | 10 | 3 | |
6 | Метатеория формальных систем | 4 | 4 | 4 | 8 | 3 | ||
Раздел 4. ТЕОРИЯ АЛГОРИТМОВ | 3 | |||||||
7 | Алгоритмические системы. Алгоритмически разрешимые и неразрешимые задачи. | 6 | 6 | 6 | 12 | 3 | ||
8 | Сложность алгоритмов | 8 | 2 | 10 | 4 | 14 | ||
9 | Алгоритмическая логика | 4 | 4 | 4 | 8 | |||
ЗАКЛЮЧЕНИЕ | 2 | 2 | 1 | 3 | 3 | |||
Курсовая работа | 16 | 30 | 46 | |||||
ИТОГО: | 48 | 16 | 80 | 65 | 145 |
ЛИТЕРАТУРА
Основная
№ | Название, библиографическое описание | Л | Пз | Кр | К-во экз. в библ. (на каф.) | Гриф |
1 | , Адельсон-Вельский математика для инженера. – М.: Энергоатомиздат, 1988 | 5 | 5 | 5 | 79(0) | |
2 | Исследование вычислительной сложности алгоритмов логического вывода: Методические указания к курсовой работе по дисциплине "Математическая логика и теория алгоритмов"/ Сост.: M. Г. Пантелеев, ; ГЭТУ. СПб., 1997. | 5 | 5 | 5 | 20(60) | |
3 | Логический вывод и сложность алгоритмов: Методические указания к практическим занятиям по дисциплине "Математическая логика и теория алгоритмов"/ Сост.: M. Г. Пантелеев, ; ГЭТУ. СПб., 1998. | 5 | 5 | 5 | 24(60) | |
4 | Логика в решении проблем. – М.: Наука, 1990 | 5 | 5 | 5 | 36(0) | |
5 | и др. Логический подход к искусственному интеллекту. - М.: Мир, 1990.3 | 5 | 5 | 5 | 26(0) |
Дополнительная
№ | Название, библиографическое описание | К-во экз. в библ. (на каф.) |
1 | Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. - М.: Мир, 1979. | 11(0) |
2 | Вычислительные машины и трудно решаемые задачи. - М.: Мир, 1982. | 15()) |
3 | Введение в математическую логику. - М.: Наука, 1971 | |
4 | Ли Р. Математическая логика и автоматическое доказательство теорем. - М.: Наука, 1983. |
Автор | |
к. т.н., доцент | |
Рецензент | |
к. т.н., доцент кафедры МО ЭВМ | |
Зав. кафедрой вычислительной техники | |
д. т.н., профессор | |
Декан факультета | |
компьютерных технологий и информатики | |
д. т.н., профессор | |
Программа согласована: | |
Зав. кафедрой вычислительной техники | |
д. т.н., профессор | |
Декан открытого факультета | |
к. т.н., профессор | |
Зав. отделом учебной литературы | |
Руководитель методического отдела | |
к. т.н., доцент |
