Логическое и реляционное программирование

2019/2020

Учебный год

RUS

Обучение ведется на русском языке

4

Кредиты

Кто читает:

Департамент информатики

Статус:

Курс по выбору

Когда читается:

4-й курс, 3 модуль

Преподаватель

Булычев Дмитрий Юрьевич

Программа дисциплины

Аннотация

Является дисциплиной по выбору. Целью курса является обеспечение базовой подготовки студентов в области декларативного программирования, знакомство с основными понятиями и техникой логического и реляционного программирования В результате освоения дисциплины студент должен:  знать основные методы логического и реляционного программирования;  уметь создавать программы на языках Prolog, Datalog и miniKanren;  владеть математическим аппаратом и инструментальными средствами для написания программа в парадигме программирования “логическое и реляционное программирование”.

Цель освоения дисциплины

• Целями освоения дисциплины «Логическое и реляционное программирование» являются формирование у студентов теоретических знаний и практических навыков по основам логического и реляционного программирования, основным алгоритмам поиска решений для декларативно специфицированных задач и реализации декларативных языков.

Планируемые результаты обучения

• Знает пропозициональный метод резолюций. Знает конъюктивные и дизъюктивные нормальные формы (КНФ, ДНФ), способ Цейтина. DPP, DPLL, CDCL.
• Владеет понятиями термы, подстановки, применение подстановки к терму, композиция подстановок. Владеет понятиями унификация, наиболее общий унификатор. «Occurs check». Знает метод резолюций для формул первого порядка. Хорновские дизъюнкты. SLD-резолюция, Prolog и его операционная семантика в простейшем случае. Отсечение («cut»), «green cut», «red cut». Операционная семантика отсечения. Incremental deepening, NAF, predicate completion.
• Проводит монадический поиск. Знает Disequality constraint. Refutational completeness. Числа, списки и пр. Реляционные интерпретаторы и пр. применения.
• Использует операционную и декларативную семантику. Знает Term rewriting: основные понятия. (Semi, strong, local)-confluence, свойство Черча-Россера, diamond property. Well-founded induction, её использование. Datalog, стратифицированное отрицание, применение для анализа программ. (RO)BDD.

Содержание учебной дисциплины

• Задача выполнимости
• Prolog
• miniKanren
• Программирование в ограничениях; системы переписывания

Элементы контроля

• Домашнее задание
• Письменный экзамен
  Экзамен проводится на платформе Zoom. Экзамен проводится в устной форме (опрос по материалам курса). По просьбе преподавателя студент должен быть готов выполнить некоторые задания в письменном виде, после чего сфотографировать и выслать на почту преподавателю. К экзамену необходимо подключиться согласно расписанию, высланному преподавателем на корпоративные почты студентов накануне экзамена. Компьютер студента должен удовлетворять требованиям: наличие рабочей камеры и микрофона, поддержка платформы Zoom. Для участия в экзамене студент обязан: выбрать себе имя в Zoom совпадающее с его именем и фамилией, явиться на экзамен согласно точному расписанию, при ответе включить камеру и микрофон. Во время экзамена студентам запрещается выключать камеру. Ипользование конспектов или других справочных материалов допускается только с разрешения преподавателя. Кратковременным нарушением связи во время экзамена считается нарушение связи менее 5 минут. Долговременным нарушением связи во время экзамена считается нарушение 5 минут и более. При долговременном нарушении связи возможность продолжения студентом участие в экзамене определяется преподавателем. Процедура пересдачи подразумевает использование усложненных заданий

Промежуточная аттестация

• Промежуточная аттестация (3 модуль)
  0.6 * Домашнее задание + 0.4 * Письменный экзамен

Список литературы

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

• Pierce, B. C. (2002). Types and Programming Languages. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=70966

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

• Cardoso, J. M. P., & Diniz, P. C. (2009). Compilation Techniques for Reconfigurable Architectures. New York, NY: Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=275651