Logical and Relationa Programming

2020/2021

Academic Year

RUS

Instruction in Russian

4

ECTS credits

Delivered at:

Department of Informatics

Course type:

Elective course

When:

4 year, 3 module

Instructor

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

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

Аннотация

Является дисциплиной по выбору. Целью курса является обеспечение базовой подготовки студентов в области декларативного программирования, знакомство с основными понятиями и техникой логического и реляционного программирования В результате освоения дисциплины студент должен:  знать основные методы логического и реляционного программирования;  уметь создавать программы на языках 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
• Программирование в ограничениях; системы переписывания

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

• Домашнее задание
• Письменный экзамен
  Экзамен проводится офлайн.

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

• Промежуточная аттестация (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