Программа и описание курса (1157989)

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

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

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

Логика предикатов первого порядка

1. Синтаксис и семантика логики предикатов. Термы, формулы, интерпретация. Отношение выполнимости формулы на интерпретации.

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

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

4. Семантические таблицы в логике предикатов. Табличный вывод. Теорема корректности табличного вывода.

5. Теорема полноты табличного вывода.

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

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

Метод резолюций

1. Предваренная нормальная форма. Теорема о приведении формулы к предваренной нормальной форме.

2. Сколемовская стандартная форма. Теорема о приведении формулы к сколемовской стандартной форме.

3. Эрбрановский универсум, эрбрановский базис, эрбрановские интерпретации. Теорема об эрбрановской модели для сколемовской стандартной формы. Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов. Теорема Эрбрана.

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

5. Сведение задачи унификации к задаче решения системы термальных уравнений. Лемма о связке. Алгоритм унификации. Теорема о корректности и завершаемости алгоритма унификации.

6. Метод резолюций для логики предикатов: правила резолюции и склейки, резолютивный вывод. Теорема корректности резолютивного вывода.

7. Лемма о подъеме. Теорема полноты резолютивного вывода для логики предикатов.

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

Основы логического программирования

1. Использование метода резолюций для нахождения ответов на запросы. Истолкование резолютивного вывода как вычисления. Примеры вычислительных возможностей резолютивного вывода.

2. Хорновские дизъюнкты. Синтаксис языка логического программирования: логические программы и запросы. Декларативная семантика логических программ. Правильный ответ.

3. SLD-резолюция. SLD-резолютивные вычисления (опровержения) логических программ. Процедурная интерпретация SLD-выводов. Примеры SLD-опровержений успешных, тупиковых и бесконечных. Вычислимый ответ. Операционная (процедурная) семантика логических программ.

4. Теорема корректности SLD-резолютивных вычислений логических программ.

5. Теорема полноты SLD-резолютивных вычислений логических программ.

6. Правило вычислений и его роль. R-вычислимый ответ. Переключательная лемма. Теорема о независимости правила вычислений. Теорема сильной полноты SLD-резолюции.

7. Дерево SLD-вычислений логических программ. Стратегии вычислений. Полные и неполные стратегии вычислений. Стандартная стратегия исполнения логических программ. Неполнота стандартной стратегии.

8. Управление исполнением логических программ. Оператор отсечения. Операционная семантика оператора отсечения.

9. Отрицание в Прологе. Допущение замкнутости мира. Отрицание как неудача. Эффект немонотонности вычислений логических программ с оператором отрицания.

10. Встроенные предикаты и функции. Операционная семантика встроенных средств.

11. Теорема о вычислительной универсальности чистого Пролога. Теорема Чёрча о неразрешимости логики предикатов первого порядка.

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

1. Интуиционистская логика. Модели Крипке для интуиционистской логики. Примеры интуиционистски общезначимых и необщезначимых формул. Модальные логики. Модели Крипке для модальных логик. Эпистемические логики. Темпоральные логики.

2. Проблема верификации последовательных программ. Операционная семантика типовых программных конструкций. Предусловие и постусловие. Частичная корректность программ. Тройки Хоара и их содержательный смысл. Правила вывода в логике Хоара для доказательства частичной корректности последовательных программ.

3. Моделирование программ системами переходов. Темпоральная логика высказываний линейного времени (PLTL): синтаксис и семантика. Применение темпоральных логик для спецификации поведения реагирующих программных систем.

4. Задача проверки выполнимости формул PLTL на конечной модели. Равносильные преобразования формул PLTL. Табличный алгоритм проверки выполнимости формул PLTL на конечной модели: основные этапы.

Основания математики

1. Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля. Арифметика Пеано. Теорема Геделя о неполноте формальной арифметики.

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

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 с.

Коллоквиум

Коллоквиум по курсу математической логики и логического программирования проводится по материалам лекций и семинарских занятий, охватывающих вопросы 1-15.

Коллоквиум проводится в письменной форме. На выполнение всех заданий коллквиума отводится 90 мин.

Задание коллоквиума состоит из 3 практических задач

- построение формулы логики предикатов, адекватно выражающей утверждение естественного языка;

- проверка общезначимости формулы логики предикатов при помощи табличного вывода;

- проверка общезначимости формулы логики предикатов при помощи метода резолюций;

и 9 теоретических вопросов.

В каждом теоретическом вопросе предлагается несколько вариантов ответа. Для решения задачи достаточно отметить (обвести кружком номер выбранного варианта) ВСЕ правильные варианты ответа. Возможно, что для некоторых вопросов не будет предложено ни одного правильного варианта ответа. В этом случае, естественно, ни один вариант ответа не должен быть отмечен.

Максимальная оценка за решение практической задачи - 2 очка. Максимальная оценка за решение теоретической задачи - 1 очко.

Оценка "отлично" получают работы с количеством очков 13-15. Авторы этих работ получают бонус 3 балла, который добавляется к числу баллов, полученных за экзаменационную работу.

Оценка "хорошо" получают работы с количеством очков 10-12. Авторы этих работ получают бонус 1 балл, который добавляется к числу баллов, полученных за экзаменационную работу.

Оценка "удовлетворительно" получают работы с количеством очков 7-9. Авторы этих работ получают штраф 1 балл, который вычитается из числа баллов, полученных за экзаменационную работу.

Оценка "неудовлетворительно" получают работы с количеством очков менее 7, а также все те слушатели курса, которые не приняли участие в коллоквиуме без уважительных причин. Неудовлетворительная оценка дает штраф 3 балла, которые вычитаются из числа баллов, полученных за экзаменационную работу.

Экзамен

Экзамен проводится в форме письменной контрольной работы, состоящей из 14 заданий. На выполнение работы отводится 150 минут.

Задание 0. Разработать логическую программу решения некоторой комбинаторной задачи. Максимальная оценка за решение задачи - 6 баллов.

Задания 1-4. Решить стандартные задачи курса: построить логическую формулу логики предикатов, адекватно выражающей заданное утверждение естественного языка, проверить общезначимость заданных формул логики предикатов при помощи табличного вывода и при помощи метода резолюций, построить дерево SLD-резолютивного вывода для заданной логической программы. Максимальная оценка за решение каждой задачи этого типа - 3 балла.

Задания 5-9. Привести формулировку одной из теорем или определение одного из понятий, изученных в лекционном курсе, а также дать краткий ответ (вида "да"-"нет") на дополнительный вопрос, относящийся к этой формулировке. Максимальная оценка за решение каждой задачи этого типа - 2 балла.

Задания 10-13. Представить набросок (эскиз) доказательства одной из теорем курса или выбрать правильные варианты ответа на заданный вопрос и обосновать выбор. Максимальная оценка за решение каждой задачи этого типа - 3 балла.

Экзаменационная оценка выставляется на основе суммарного количества баллов, полученных за решение задач экзаменационной контрольной работы, и количества бонусных (штрафных) баллов, полученных за решение задач коллоквиума.

Оценка отлично: не менее 32 баллов.

Оценка хорошо: не менее 24 и не более 31 баллов.

Оценка удовлетворительно: не менее 16 и не более 23 баллов.

Оценка неудовлетворительно: не более 15 баллов.

https://studizba.com

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

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

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

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

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

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