WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

   Добро пожаловать!


Министерство образования Российской Федерации Санкт-Петербургский государственный электротехнический университет “ЛЭТИ” РАБОЧАЯ ПРОГРАММА дисциплины МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ Для подготовки дипломированных специалистов по направлению 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 Язык логики высказываний, анализ свойств логических формул. Преобразование формул в КНФ.

2 Метод резолюций в логике высказываний. Сравнение эффективности различных стратегий.

3 Язык логики предикатов. Преобразование формул в предваренную форму.

4 Преобразование формул логики предикатов в сколемовскую и клаузальную формы.

5 Метод резолюций в логике предикатов. Унификация атомов, построение наиболее общего унификатора.

6 Примеры логического программирования, реализация логического вывода на хорновских дизъюнктах.

7 Примеры формального вывода в логических исчислениях 8 Оценка сложности алгоритмов Цели и содержание курсовой работы Цель курсовой работы – получение практических навыков алгоритмизации и программной реализации логического вывода с использованием метода резолюций, а также теоретической и экспериментальной оценки сложности построенных алгоритмов. Таким образом, курсовая работа направлена на практическое закрепление ключевых теоретических вопросов данной дисциплины как в части логики, так и в части теории алгоритмов.

Содержание курсовой работы включает:

1. Разработку укрупненного алгоритма метода резолюций для заданного набора стратегий и детализированных алгоритмов отдельных процедур.

2. Теоретическую оценку сложности разработанных алгоритмов.

3. Разработку и отладку программы, экспериментальное исследование сложности алгоритмов.

Распределение учебных часов по темам и видам занятий Объем учебных часов № Семестр Название разделов и тем Лекции Лабор. Практ. Аудит. Самост. Всего темы занятия занятия занятия Работа ВВЕДЕНИЕ 1 1 1 Раздел 1. ЛОГИКА ВЫСКАЗЫВАНИЙ 1 Основы логики высказываний 2 2 4 2 6 2 Вывод в логике высказываний 5 2 7 4 11 Раздел 2. ЛОГИКА ПРЕДИКАТОВ 3 Язык логики предикатов 4 4 2 6 4 Логический вывод в логике предикатов 6 8 14 6 20 Раздел 3. ФОРМАЛЬНЫЕ (АКСИОМАТИЧЕСКИЕ) СИСТЕМЫ 5 Основы теории формальных систем 6 2 8 2 10 6 Метатеория формальных систем 4 4 4 8 Раздел 4. ТЕОРИЯ АЛГОРИТМОВ 7 Алгоритмические системы. 6 6 6 12 Алгоритмически разрешимые и неразрешимые задачи.

8 Сложность алгоритмов 8 2 10 4 9 Алгоритмическая логика 4 4 4 ЗАКЛЮЧЕНИЕ 2 2 1 3 Курсовая работа 16 30 48 16 80 65 ИТОГО:

ЛИТЕРАТУРА Основная К-во экз.

Л Пз Кр в библ. Гриф Название, библиографическое описание № (на каф.) 1 Кузнецов О.П., Адельсон-Вельский Г.М. Дискретная 5 5 5 79(0) математика для инженера. – М.: Энергоатомиздат, 2 Исследование вычислительной сложности алгоритмов логического вывода: Методические указания к курсовой работе по дисциплине "Математическая логика и теория 5 5 20(60) алгоритмов"/ Сост.: M.Г. Пантелеев, А.С. Календарев;

ГЭТУ. СПб., 1997.

3 Логический вывод и сложность алгоритмов: Методические указания к практическим занятиям по дисциплине 5 5 24(60) "Математическая логика и теория алгоритмов"/ Сост.: M.Г.

Пантелеев, А.С. Календарев; ГЭТУ. СПб., 1998.

4 Ковальски Р. Логика в решении проблем. – М.: Наука, 5 5 5 36(0) 5 Тейз А. и др. Логический подход к искусственному 5 5 5 26(0) интеллекту. - М.: Мир, 1990.Дополнительная К-во экз. в библ. (на № Название, библиографическое описание каф.) 1 Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных 11(0) алгоритмов. - М.: Мир, 1979.

2 Гэри М., Джонсон Д. Вычислительные машины и трудно решаемые задачи. - М.: 15()) Мир, 1982.

3 Мендельсон Э. Введение в математическую логику. - М.: Наука, 4 Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. - М.: Наука, 1983.

Автор Пантелеев М.Г.

к.т.н., доцент Рецензент Ивановский С.А.

к.т.н., доцент кафедры МО ЭВМ Зав. кафедрой вычислительной техники Пузанков Д.В.

д.т.н., профессор Декан факультета компьютерных технологий и информатики Герасимов И.В.

д.т.н., профессор Программа согласована:

Зав. кафедрой вычислительной техники Пузанков Д.В.

д.т.н., профессор Декан открытого факультета к.т.н., профессор Кузьмин Н.Н.

Зав. отделом учебной литературы Киселева Т.В.

Руководитель методического отдела к.т.н., доцент Марасина Л.А.











© 2011 www.dissers.ru - «Бесплатная электронная библиотека»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.