Математическая логика и теория алгоритмов
Общий курс
Составитель: д.ф.-м.н., проф. И.Л. Братчиков
- Цели и задачи курса. Его место в учебном процессе.
- После окончания курса студенты должны знать и уметь.
- Содержание курса.
- Рекомендуемый перечень практических занятий.
- Темы практических занятий.
- Перечень вопросов, выделенных для самостоятельного изучения студентами.
- Рекомендуемое распределение часов по темам и видам работ для очной формы обучения.
- Литература.
Цели и задачи курса.
Его место в учебном процессе.
Цели и задачи данного курса определяются той ролью, которую играет математическая логика в современных математике и информатике. В первую очередь очевидно большое значение, которое имеет математическая логика в основаниях математики. Строгое, математически точное построение логических исчислений, решение проблемы дедукции, аксиоматические системы и доказательство теорем в их рамках прививают учащимся навыки работы с математическими объектами, математическую строгость мышления, совершенно необходимую для исследовательской работы в области математики и других точных наук. В то же время быстрое развитие вычислительной техники способствует расширению как круга задач, решаемых с помощью математической логики, так и методов, применяемых для их решения. Это в первую очередь относится к задачам искусственного интеллекта, решение которых немыслимо без привлечения методов математической логики. Сказанное в полной мере относится и к теории алгоритмов, тесно связанной с математической логикой. Таким образом, знание основ математической логики и теории алгоритмов совершенно необходимо преподавателям математики и информатики высших и средних учебных заведений.
Содержание данного курса несколько изменено по сравнению с традиционными курсами математической логики, читаемыми на математических факультетах. В связи с быстрым развитием методов и средств логического программирования и фундаментальным значением, которое приобретает математическая логика для дальнейшего развития информатики в целом, большее внимание, чем обычно, уделено тем аспектам, которые особенно актуальны для информатики. Этим объясняется включение в курс метода резолюций, который лежит в основе логического программирования - относительно нового направления в программировании, с помощью которого решается большинство задач искусственного интеллекта. В то же время из-за недостатка часов в программу не включены теоремы Геделя, сокращено рассмотрение аксиоматических систем.
Последний раздел курса посвящен теории алгоритмов. Здесь рассматривается лишь один класс алгоритмов - машины Тьюринга как общего вида, так и наиболее важные их подклассы. Составитель настоящего курса исходит из того, что многие свойства алгоритмов изучаются в ряде других курсов, читаемых студентам факультета.
Содержание и методика изложения предмета ориентированы на его преподавание в рамках бакалавриата в четвертом или шестом семестрах очной формы обучения.
Итак, главной целью настоящего курса следует считать изучение студентами основ математической логики и теории алгоритмов, а также приобретение необходимых навыков работы с информационными, логическими и алгоритмическими объектами, которые рассматриваются в курсе.
В число основных задач курса следует включить:
- Знакомство с основными методами логических рассуждений - дедукцией, индукцией, аналогией. Рассмотрение методов решения задач логического характера.
- Изучение классических логических исчислений - исчисления высказываний, исчисления предикатов.
- Освоение метода резолюций как основного метода решения проблемы дедукции в исчислениях высказываний и предикатов.
- Знакомство с основами логического программирования.
- Изучение основных свойств аксиоматических систем и ознакомление с методами формальных доказательств в рамках этих систем.
- Изучение машин Тьюринга и разработанных на ее основе важнейших классов алгоритмов.
[Наверх]
После окончания курса студенты должны знать и уметь.
Студенты должны знать:- Место математической логики среди других математических дисциплин; задачи, решаемые в рамках математической логики.
- Определение исчисления высказываний (ИВ) и основных понятий этого исчисления.
- Методы преобразования произвольных формул ИВ в дизъюнктивные и конъюнктивные нормальные формы.
- Проблему дедукции и ее решение методами прямой и обратной дедукции.
- Метод резолюций для ИВ и его роль в решении проблемы дедукции.
- Определение исчисления предикатов (ИП) и основных понятий этого исчисления.
- Методы преобразования произвольных формул ИП в клаузальные формы.
- Эрбранов универсум и его роль в доказательстве свойств формул ИП.
- Подстановки и унификацию литер в ИП.
- Метод резолюций для ИП и его роль в решении проблемы дедукции.
- Проблематику искусственного интеллекта и способы представления баз знаний средствами ИП.
- Понятие о логическом программировании.
- Определение, свойства аксиоматических систем и приемы работы с ними.
- Определение и классы машин Тьюринга и их роль в теории алгоритмов.
- Формулировать задачи логического характера в рамках ИВ и ИП.
- Выполнять преобразования логических формул с использованием схем тождественных преобразований.
- Проводить исследование логических формул для доказательства их свойств.
- Применять метод резолюций для решения проблемы дедукции в ИВ и ИП.
- Описывать базы знаний средствами логических исчислений.
- Проводить доказательства в рамках аксиоматических систем.
- Формулировать и решать задачи, пользуясь соответствующими классами машин Тьюринга.
По остальным вопросам программы необходимо иметь общее представление и уметь пользоваться литературой.
Ключевые понятия, которые должны быть усвоены: дедукция, индукция, аналогия, силлогизм, высказывание, предикат, логическое исчисление, логическая формула, интерпретация логических формул, общезначимость, выполнимость и невыполнимость логических формул, тождественные преобразования, дизъюнктивные и конъюнктивные нормальные формы, клаузальные формы, Эрбранов универсум, дизъюнкт, дизъюнкт Хорна, резолюция, унификация, унификатор, база знаний, аксиоматическая система, машина Тьюринга, распознаватель, преобразователь, линейно-ограниченный автомат, конечный автомат.
[Наверх]
Содержание курса.
- Раздел 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. | Раздел 1. Введение | 4 | 2 | 2 |
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. Заключение. | 8 | 4 | 4 |
ИТОГО | 140 | 70 | 70 |
Примечания.
- Трудоемкость настоящего курса составляет 280 часов, из них 140 часов - самостоятельная работа студентов.
- В часы самостоятельной работы студентов включено время на написание реферата.
- При организации лабораторных занятий используются часы, отведенные под практические занятия по разделу 6.
[Наверх]
ЛИТЕРАТУРА
- Клини С.К. Математическая логика. М,. Мир, 1973.
- Мендельсон Э. Введение в математическую логику. М., Наука, 1984.
- Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М., Наука, 1983.
- Тей А., Грибомон П. и др. Логический подход к искусственному интеллекту, том 1. М., Мир, 1990.
- Тей А., Грибомон П. и др. Логический подход к искусственному интеллекту, том 2. М., Мир, 1998.
- Ковальски Р. Логика в решении проблем. М., Наука, 1990.
- Барвайс Дж. (ред.) Справочная книга по математической логике. М., Наука, 1982.
- Ин Ц., Соломон Д. Использование Турбо-Пролога. М., Мир, 1993.
- Братчиков И.Л. Синтаксис языков программирования. М., Наука, 1975.