zhChinese    enEnglish
  ПМ-ПУ  » Образование  » Программы курсов » Математическая логика и теория алгоритмов

Математическая логика и теория алгоритмов

Общий курс

Составитель: д.ф.-м.н., проф. И.Л. Братчиков

Цели и задачи курса.
Его место в учебном процессе.

Цели и задачи данного курса определяются той ролью, которую играет математическая логика в современных математике и информатике. В первую очередь очевидно большое значение, которое имеет математическая логика в основаниях математики. Строгое, математически точное построение логических исчислений, решение проблемы дедукции, аксиоматические системы и доказательство теорем в их рамках прививают учащимся навыки работы с математическими объектами, математическую строгость мышления, совершенно необходимую для исследовательской работы в области математики и других точных наук. В то же время быстрое развитие вычислительной техники способствует расширению как круга задач, решаемых с помощью математической логики, так и методов, применяемых для их решения. Это в первую очередь относится к задачам искусственного интеллекта, решение которых немыслимо без привлечения методов математической логики. Сказанное в полной мере относится и к теории алгоритмов, тесно связанной с математической логикой. Таким образом, знание основ математической логики и теории алгоритмов совершенно необходимо преподавателям математики и информатики высших и средних учебных заведений.

Содержание данного курса несколько изменено по сравнению с традиционными курсами математической логики, читаемыми на математических факультетах. В связи с быстрым развитием методов и средств логического программирования и фундаментальным значением, которое приобретает математическая логика для дальнейшего развития информатики в целом, большее внимание, чем обычно, уделено тем аспектам, которые особенно актуальны для информатики. Этим объясняется включение в курс метода резолюций, который лежит в основе логического программирования - относительно нового направления в программировании, с помощью которого решается большинство задач искусственного интеллекта. В то же время из-за недостатка часов в программу не включены теоремы Геделя, сокращено рассмотрение аксиоматических систем.

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

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

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

В число основных задач курса следует включить:

  1. Знакомство с основными методами логических рассуждений - дедукцией, индукцией, аналогией. Рассмотрение методов решения задач логического характера.
  2. Изучение классических логических исчислений - исчисления высказываний, исчисления предикатов.
  3. Освоение метода резолюций как основного метода решения проблемы дедукции в исчислениях высказываний и предикатов.
  4. Знакомство с основами логического программирования.
  5. Изучение основных свойств аксиоматических систем и ознакомление с методами формальных доказательств в рамках этих систем.
  6. Изучение машин Тьюринга и разработанных на ее основе важнейших классов алгоритмов.

[Наверх]

После окончания курса студенты должны знать и уметь.

Студенты должны знать:
  1. Место математической логики среди других математических дисциплин; задачи, решаемые в рамках математической логики.
  2. Определение исчисления высказываний (ИВ) и основных понятий этого исчисления.
  3. Методы преобразования произвольных формул ИВ в дизъюнктивные и конъюнктивные нормальные формы.
  4. Проблему дедукции и ее решение методами прямой и обратной дедукции.
  5. Метод резолюций для ИВ и его роль в решении проблемы дедукции.
  6. Определение исчисления предикатов (ИП) и основных понятий этого исчисления.
  7. Методы преобразования произвольных формул ИП в клаузальные формы.
  8. Эрбранов универсум и его роль в доказательстве свойств формул ИП.
  9. Подстановки и унификацию литер в ИП.
  10. Метод резолюций для ИП и его роль в решении проблемы дедукции.
  11. Проблематику искусственного интеллекта и способы представления баз знаний средствами ИП.
  12. Понятие о логическом программировании.
  13. Определение, свойства аксиоматических систем и приемы работы с ними.
  14. Определение и классы машин Тьюринга и их роль в теории алгоритмов.
Студенты должны уметь:
  1. Формулировать задачи логического характера в рамках ИВ и ИП.
  2. Выполнять преобразования логических формул с использованием схем тождественных преобразований.
  3. Проводить исследование логических формул для доказательства их свойств.
  4. Применять метод резолюций для решения проблемы дедукции в ИВ и ИП.
  5. Описывать базы знаний средствами логических исчислений.
  6. Проводить доказательства в рамках аксиоматических систем.
  7. Формулировать и решать задачи, пользуясь соответствующими классами машин Тьюринга.

По остальным вопросам программы необходимо иметь общее представление и уметь пользоваться литературой.

Ключевые понятия, которые должны быть усвоены: дедукция, индукция, аналогия, силлогизм, высказывание, предикат, логическое исчисление, логическая формула, интерпретация логических формул, общезначимость, выполнимость и невыполнимость логических формул, тождественные преобразования, дизъюнктивные и конъюнктивные нормальные формы, клаузальные формы, Эрбранов универсум, дизъюнкт, дизъюнкт Хорна, резолюция, унификация, унификатор, база знаний, аксиоматическая система, машина Тьюринга, распознаватель, преобразователь, линейно-ограниченный автомат, конечный автомат.

[Наверх]

Содержание курса.

Раздел 1. Введение.
Понятие информационно-логических систем и их место в математике и информатике. Роль математической логики, как теоретической основы математики. Влияние математической логики на развитие информатики. Понятие искусственного интеллекта.
Примеры задач, решаемых рассуждениями. Необходимость формализации рассуждений. Дедукция, силлогизм, индукция, математическая индукция.
Основные математические понятия, необходимые для изложения основ математической логики.
Раздел 2. Исчисление высказываний.
2.1. Формулы исчисления высказываний и их интерпретация.
Понятие высказывания. Синтаксис исчисления высказываний (ИВ). Интерпретация формул в ИВ. Общезначимые, выполнимые и невыполнимые формулы. Тривиальный алгоритм проверки выполнимости формул. Алгоритм Куайна.
2.2. Алгебраический подход к ИВ.
Алгебра логики и эквивалентные преобразования. Некоторые приложения алгебры логики.
2.3. Нормальные формы.
Дизъюнктивные и конъюнктивные нормальные формы в ИВ (ДНФ и КНФ). Методы построения ДНФ и КНФ, эквивалентных произвольным формулам ИВ: с помощью таблиц истинности, с помощью эквивалентных преобразований. Алгоритм Девиса-Патнема для проверки выполнимости нормальных форм.
2.4. Метод резолюций в ИВ.
Проблема дедукции и ее значение в математической логике и информатике. Прямая и обратная дедукции. Теорема Робинсона и правило резолюций. Метод резолюций для решения проблемы дедукции. Дизъюнкты Хорна. Метод резолюций для дизъюнктов Хорна. Оценка трудоемкости метода.
Раздел 3. Исчисление предикатов (первого порядка).
3.1. Понятие предиката.
Ограниченность ИВ. Примеры рассуждений, не формализуемых в рамках ИВ. Понятие предиката и примеры его использования в рассуждениях.
3.2. Синтаксис и семантика формул исчисления предикатов.
Синтаксис исчисления предикатов (ИП). Семантика формул в ИП. Кванторы и типы вхождения переменных в формулы. Интерпретация формул в ИП. Примеры интерпретаций. Общезначимые, выполнимые и невыполнимые формулы. Схемы общезначимых формул, используемых для эквивалентных преобразований.
3.3. Клаузальные формы.
Подстановка и конкретизация в ИП. Универсальное и экзистенциональное замыкания. Предваренные и нормальные формы. Сколемовские и клаузальные формы. Алгоритм преобразования произвольной формулы ИП в клаузальную форму.
3.4. Эрбранова интерпретация.
Эрбранов универсум множества дизъюнктов. Основные выражения и эрбранов базис. Н-интерпретация. Теорема о невыполнимости множества дизъюнктов. Следствия теоремы.
3.5. Метод резолюций в ИП.
Проблема дедукции в ИП. Фундаментальная резолюция. Унификация с помощью подстановки. Алгоритм унификации. Метод резолюций для ИП. Дизъюнкты Хорна и решение проблемы дедукции методом резолюций в ИП. Примеры применения метода резолюций для решения проблемы дедукции. Связь ИП с системами представления знаний в задачах искусственного интеллекта.
Раздел 4. Аксиоматические системы.
4.1. Определение аксиоматических систем.
Определение и свойства аксиоматических систем (АС). Области применения АС.
4.2. АС с правилом вывода Modus Ponens.
Ас исчисления высказываний (с правилом вывода М.Р.). Полнота и минимальность АС. Примеры доказательства теорем. Теорема Эрбрана-Тарского и ее использование для упрощения доказательств.
4.3. АС натурального вывода.
Определение и особенности АС натурального вывода. Правила вывода. Примеры доказательства теорем.
4.4. Теории первого порядка.
Понятие о теориях первого порядка. Примеры теорий и их использования.
Раздел 5. Основы теории алгоритмов.
5.1. Понятие алгоритма.
Неформальное определение алгоритма. Примеры алгоритмов. Основные свойства алгоритмов. Роль алгоритмов в информатике. Парадигма процедурного программирования.
5.2. Алгоритмические проблемы.
Проблема разрешимости. Примеры неразрешимых проблем. Понятие вычислимости и вычислительные процедуры.
5.3. Машины Тьюринга.
Определение машины Тьюринга. Примеры машин Тьюринга. Тезис Черча-Тьюринга. Проблема остановки для машины Тьюринга.
5.4. Машины Тьюринга с разрешимой проблемой остановки.
Линейно-ограниченные автоматы. Проблема остановки для линейно-ограниченных автоматов. Машина Тьюринга как распознаватель формальных языков. Двухленточные машины Тьюринга. Автоматы с магазинной памятью. Конечные автоматы. Синтаксический анализ языков с помощью автоматов с магазинной памятью и конечных автоматов.
Раздел 6. Заключение.
Обзор приложений математической логики в информатике. Парадигма логического программирования. Язык Пролог как реализация метода резолюций для решения задач искусственного интеллекта.

[Наверх]

Рекомендуемый перечень практических занятий.

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

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

[Наверх]

Темы практических занятий.

  1. Решение задач логического характера методом логических рассуждений.
  2. Работа с формулами ИВ и их интерпретацией. Задачи на алгебраическую интерпретацию формул ИВ и ее применение для исследования контактных схем.
  3. Преобразование формул ИВ к ДНФ и КНФ.
  4. Применение метода резолюций для решения проблемы дедукции в ИВ.
  5. Работа с формулами ИП и их интерпретацией.
  6. Преобразование формул ИП к клаузальным формам.
  7. Задачи на эрбранов универсум множеств дизъюнктов и доказательство свойств множеств дизъюнктов.
  8. Задачи на подстановки и унификаторы. Применение алгоритма вычисления наиболее общих унификаторов.
  9. Применение метода резолюций для решения проблемы дедукции в ИП.
  10. Решение задач содержательного характера с помощью метода резолюций.
  11. Доказательства теорем в аксиоматической системе с правилом вывода М.Р.
  12. Доказательства теорем в аксиоматической системе натурального вывода.
  13. Задачи на разработку алгоритмов решения задач, основанные на неформальном определении понятия алгоритм.
  14. Примеры использования машин Тьюринга общего вида.
  15. Примеры использования машин Тьюринга с разрешимой проблемой остановки. Решение задач с помощью конечных автоматов.
Примечания.
  1. При организации лабораторных занятий в компьютерных классах студенты решают задачи логического характера с использованием языка Пролог.
  2. Темы практических и лабораторных занятий и их количество могут варьироваться в рабочих программах курса.

[Наверх]

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

Примечание.Некоторые из этих тем могут быть освещены в лекциях и на практических занятиях при наличии соответствующего учебного времени.

[Наверх]

Рекомендуемое распределение часов по темам и видам работ для очной формы обучения.

№наименование разделов и темУчебные часы
всеголекц.пр.зан.
1.Раздел 1. Введение422
2.
2.1.
2.2.
2.3.
2.4.		 Раздел 2. Исчисление высказываний (ИВ).
Формулы ИВ и их интерпретация.
Алгебраический подход к ИВ.
Нормальные формы.
Метод резолюций в ИВ.		 28
4
4
10
10		 12
2
2
4
4		 16
2
2
6
6
3.
3.1.
3.2.
3.3.
3.4.
3.5.		 Раздел 3. Исчисление предикатов (ИП).
Понятие предиката.
Синтаксис и семантика формул ИП.
Клаузальные формы.
Эрбранова интерпретация.
Метод резолюций в ИП.		 50
4
10
10
10
16		 24
2
4
4
6
8		 26
2
6
6
4
8
4.
4.1.
4.2.
4.3.
4.4.		 Раздел 4. Аксиоматические системы (АС).
Определение и свойства АС.
АС с правилом вывода М.Р.
АС натурального вывода.
Теории первого порядка.		 26
2
12
10
2		 14
2
6
4
2		 12
-
6
6
-
5.
5.1.
5.2.
5.3.
5.4.		 Раздел 5. Основы теории алгоритмов.
Понятие алгоритма.
Алгоритмические проблемы.
Машины Тьюринга.
Машины Тьюринга с разрешимой проблемой остановки.		 24
4
4
8
8		 14
2
4
4
4		 10
2
-
4
4
6. Раздел 6. Заключение.844
 ИТОГО1407070

Примечания.

  1. Трудоемкость настоящего курса составляет 280 часов, из них 140 часов - самостоятельная работа студентов.
  2. В часы самостоятельной работы студентов включено время на написание реферата.
  3. При организации лабораторных занятий используются часы, отведенные под практические занятия по разделу 6.

[Наверх]

ЛИТЕРАТУРА

  1. Клини С.К. Математическая логика. М,. Мир, 1973.
  2. Мендельсон Э. Введение в математическую логику. М., Наука, 1984.
  3. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М., Наука, 1983.
  4. Тей А., Грибомон П. и др. Логический подход к искусственному интеллекту, том 1. М., Мир, 1990.
  5. Тей А., Грибомон П. и др. Логический подход к искусственному интеллекту, том 2. М., Мир, 1998.
  6. Ковальски Р. Логика в решении проблем. М., Наука, 1990.
  7. Барвайс Дж. (ред.) Справочная книга по математической логике. М., Наука, 1982.
  8. Ин Ц., Соломон Д. Использование Турбо-Пролога. М., Мир, 1993.
  9. Братчиков И.Л. Синтаксис языков программирования. М., Наука, 1975.