Программа курса и литература (1131970)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Программа курса

Классические логики

1. Логика высказываний: синтаксис, семантика; выполнимость, невыполнимость, общезначимость формул. Проблема общезначимости формул логики высказываний.

2. Метод семантических таблиц в логике высказываний: семантическая таблица, табличный вывод, теорема о табличном выводе.

3. Проблема выполнимости булевых формул: приложения, основные решающие алгоритмы (алгоритм локального поиска, алгоритм DPLL).

4. Логика предикатов: синтаксис (термы, формулы, свободные и связанные переменные), семантика (интерпретации, отношение выполнимости).

5. Выполнимость, общезначимость и противоречивость формул логики предикатов. Модели. Логическое следование. Теорема о логическом следствии. Проблема общезначимости формул логики предикатов.

6. Пример выполнимой формулы логики предикатов, не имеющей конечных моделей.

7. Метод семантических таблиц в логике предикатов: семантическая таблица, табличный вывод, теорема о табличной проверке общезначимости, теорема корректности табличного вывода, теорема полноты табличного вывода.

8. Теорема Лёвенгейма-Сколема. Теорема компактности Мальцева. Теорема Чёрча.

9. Равносильные формулы. Теорема о равносильной замене.

Метод резолюций в логике предикатов

1. Предварённая нормальная форма. Теорема о предварённой нормальной форме.

2. Сколемовская стандартная форма. Алгоритм сколемизации предварённой нормальной формы. Теорема о сколемизации.

3. Дизъюнкты. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов.

4. Подстановки. Композиция подстановок. Унификатор. Наиболее общий унификатор. Задача унификации выражений логики предикатов.

5. Лемма о связке. Алгоритм унификации. Теорема об унификации.

6. Правило резолюции. Правило склейки. Резолютивный вывод. Теорема корректности резолютивного вывода.

7. Эрбрановский универсум. Эрбрановский базис. Эрбрановские интерпретации. Теорема об эрбрановских интерпретациях. Теорема Эрбрана.

8. Лемма об основных дизъюнктах. Лемма о подъёме. Теорема полноты резолютивного вывода.

9. Метод резолюций: общая схема, применение.

10. Стратегии резолютивного вывода. Семантическая резолюция. Теорема полноты семантического резолютивного вывода. Входной резолютивный вывод.

11. Резолютивный вывод как средство вычисления. Хорновские дизъюнкты.

Аксиоматические теории первого порядка

1. Аксиомы. Аксиоматическая теория первого порядка: определение; выполнимость, общезначимость и противоречивость формул в теории. Проблемы общезначимости и выполнимости формул логики предикатов в теории.

2. Основные свойства теорий: непротиворечивость, разрешимость, категоричность, полнота. Изоморфизм и элементарная эквивалентность интерпретаций. Связь изоморфизма интерпретаций, элементарной эквивалентности интерпретаций и полноты теорий.

3. Теория частичных порядков. Теория равенства: непротиворечивость, разрешимость, некатегоричность.

4. Исчисление предикатов: схемы аксиом, правило modus ponens, правило обобщения, логический вывод. Теорема Гёделя о полноте. Аксиоматические теории и исчисления.

5. Формальная арифметика. Теорема Гёделя о неполноте. Нумерации Гёделя. Арифметизуемые отношения.

6. Арифметика Пресбургера: непротиворечивость, разрешимость, полнота.

7. Бескванторные теории первого порядка. Теории с равенством. Преимущества проблемы выполнимости формул в теории перед проблемой общезначимости.

8. Теория равенства с неинтерпретируемыми функциями, разрешимость теории: сведение проблемы выполнимости в теории к проблеме выполнимости булевых формул.

9. Линейная арифметика. Виды линейных арифметик. NP-полнота линейной целочисленной арифметики.

10. Комбинация решающих алгоритмов для проблем выполнимости формул в теориях и в логике высказываний. Остовная проверка выполнимости формул в теориях. Интеграция алгоритмов проверки выполнимости формул в теориях в алгоритм DPLL.

Аксиоматическая теория множеств

1. Наивная теория множеств. Сравнение мощностей множеств. Кардинальные числа в наивной теории множеств.

2. Теорема Кантора. Теорема об объединении множества, неограниченного по мощности. Теорема Кантора-Бернштейна.

3. Примеры кардинальных чисел. Конечность множеств мощности меньше счётной. Континуум-гипотеза в наивной теории множеств.

4. Выразительные возможности наивной теории множеств: натуральные числа, кортежи, функции. Парадоксы теории множеств.

5. Аксиоматические теории множеств. Теория Цермело-Френкеля: аксиомы и схемы аксиом, доказательство существования основных множеств наивной теории, исключение основных парадоксов теории множеств. Вопросы непротиворечивости теории Цермело-Френкеля.

6. Определимость функций и отношений в теории. Применение определений для расширения теории.

7. Аксиома выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и её отрицанием.

8. Ординальные числа. Основные свойства ординальных чисел. Арифметика ординальных чисел.

9. Теорема Цермело. Кардинальные числа в теории Цермело-Френкеля с аксиомой выбора.

10. Континуум-гипотеза в теории Цермело-Френкеля с аксиомой выбора. Непротиворечивость теорий Цермело-Френкеля с аксиомой выбора и континуум-гипотезой, её отрицанием.

Неклассические прикладные логики

1. Модальные логики. Шкалы и модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.

2. Формальная верификация программ. Модель императивных программ: синтаксис, операционная семантика. Предусловия и постусловия. Корректность и частичная корректность программ. Тройки Хоара. Логика Хоара. Теорема корректности вывода в логике Хоара.

3. Верификация распределённых систем. Логика линейного времени: синтаксис, семантика. Основные равносильности в логике линейного времени. Применение темпоральных логик для спецификации поведения распределённых систем.

4. Размеченные системы переходов. Моделирование программ системами переходов. Семантика чередующихся вычислений. Задача проверки выполнимости формул логики линейного времени на размеченных системах переходов.

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

Рекомендованная литература

Основная литература

1. Клини С. Математическая логика. М.:Мир, 1973, 480 с.

2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.

3. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.

4. Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.

5. Братко И. Программирование на Прологе для искусственного интеллекта. М.:Мир, 1990, 560 с.

6. Набебин А.А. Логика и Пролог в дискретной математике. М., Изд-во МЭИ, 1997.

7. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: model checking. Изд-во МЦНМО, Москва, 2002, 405 с.

Дополнительная литература

1. Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.

2. Верещагин Н.К., Шень А. Языки и исчисления. 2004.

3. Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.

4. Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.

5. Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.

6. Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.

7. Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.

8. Хоггер К., Введение в логическое программирование. М.:Мир, 1988. 348 с.

9. Клоксин У., Меллиш К. Программирование на языке Пролог. М.:Мир, 1987. 336 с.

10. Кларк К.Л., Маккейб Ф.Г. Микро-Пролог: введение в логическое программирование. Москва, "Радио и связь". 1987, 311 с.

11. Стерлинг Л., Шапиро Э., Искусство программирования на языке ПРОЛОГ. Москва, "Мир", 1990, 235 с.

12. Ковальский Р. Логика в решении проблем. М.: Наука, 1990. 277 с.

13. Логический подход к искусственному интеллекту (от модальной логики к логике баз данных). М.:Мир, 1998. 495 с.

https://studizba.com

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов учебной работы