Логические основы программирования (ФИТ)

Лекторы
(в скобках для каждой программы обучения, на которой лектор читает курс, — количество часов лекций по учебному плану)

Яхъяева Гульнара Эркиновна (информатика и вычислительная техника (бакалавриат) 32 час.)

Программа дисциплины «Логические основы программирования» составлена в соответствии с требованиями ФГОС ВПО к структуре и результатам освоения основных образовательных программ бакалавриата по Профессиональному циклу по направлению подготовки «Информатика и вычислительная техника», а также задачами, стоящими перед Новосибирским государственным университетом по реализации Программы развития НГУ.

Автор (авторы) к.ф.-м.н., доцент Яхъяева Г.Э., к.ф.-м.н. Павловский Е.Н.

Факультет информационных технологий

Кафедра общей информатики

Contents


Место дисциплины в структуре образовательной программы

Изучение дисциплины опирается на курсы «Математическая логика и теория алгоритмов» (логика предикатов, теорема о полноте логики предикатов, теорема компактности, рекурсивные и рекурсивно-перечислимые множества), «Алгебра и геометрия» (общие сведения из теории групп, полей и колец).

Содержание дисциплины является обязательным минимум для последующих курсов: «Логические методы в инженерии знаний», «Формальные методы программной инженерии», «Методы трансляции и компиляции».

Компетенции обучающегося, формируемые в результате освоения дисциплины

Дисциплина формирует следующие компетенции:

  • ПК-26 Владеет теоретическими основами программирования, основами логического и декларативного программирования

Дисциплина участвует в формировании следующих компетенций:

  • ОК-1 владеет культурой мышления, способен к обобщению, анализу, воспри-ятию информации, постановке цели и выбору путей ее достижения
  • ОК-2 умеет логически верно, аргументировано и ясно строить устную и пись-менную речь
  • ОК-6 стремится к саморазвитию, повышению своей квалификации и мастерства
  • ОК-10 использует основные законы естественнонаучных дисциплин в профес-сиональной деятельности, применяет методы математического анализа и моделирования, теоретического и экспериментального исследования
  • ОК-11 осознает сущность и значение информации в развитии современного об-щества; владеет основными методами, способами и средствами получе-ния, хранения, переработки информации
  • ПК-28 владеет понятиями синтаксиса и семантики формальных языков. Владеет навыками формального представления содержательных знаний средствами формальных языков
  • ПК-65 Может разрабатывать интеллектуальные системы, включая агентов, действующих в вероятностной среде, систем принятия решений, аниматов
  • ПК-66 Умеет применять методы теории информации и методы обработки изо-бражений и сигналов в различных областях
  • ИК-4 владеет языком программирования высокого уровня Си и техникой программирования

В результате освоения дисциплины обучающийся должен:

  • Знать основы логического программирования, основные виды модальных и неклассических логик, логик описаний; логические основы формальной семантики языков программирования; основы теории типов и типизированного лямбда-исчисления.
  • Уметь применять резолютивный вывод для доказательства утверждений, строить фреймы для различных интуиционистских, модальных и программных логик.
  • Владеть методами унификации и резолюций, методами построения и анализа формальных моделей предметных областей; техникой построения решёток формальных понятий.

Содержание разделов и тем курса

Теория моделей

(см. сканы лекций)

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

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

  • Подстановки. Унификаторы.
  • Алгоритм унификации. Теорема об унификации.
  • Резолюции. Резольвента. Понятие вывода.
  • Метод резолюций. Теорема о корректности и полноте методы резолюций.
  • Модели Эрбрана. Наименьшая модель Эрбрана. Теорема о наименьшей модели Эрбрана.
  • Множество решений программы. Теорема о множестве решений про-граммы.
  • Теорема о полноте резолюций.
  • Алгоритмические свойства наименьшей модели Эрбрана.
  • Пруверы: Vampire, Racer.

Анализ формальных понятий

  • Определение формального контекста, формального понятия.
  • Соответствия Галуа.
  • Теорема о решётке формальных понятий.
  • Импликации в формальных контекстах.

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

Модальные логики

  • Аксиомы. Структуры Крипке. Примеры модальностей.
  • Теоремы об общезначимости аксиом в K, S4, M.
  • Теоремы о корректности и полноте.

Многозначные логики

  • Трехзначные логики Лукасевича, Клини, Геделя-Сметанича.
  • Четырехзначная логика Белнапа и отношение первопорядкового следования.
  • Нечеткие логики. Нечеткие лингвистические логики.
  • Теория приблизительных рассуждений

Дескриптивные логики

  • Пропозициональные динамические логики.
  • Темпоральные логики.

Логические основы абстрактных типов данных

  • свободные и термальные системы, структуры данных;
  • неразрешимость достаточной полноты и непротиворечивости спецификаций АТД в общем случае.

Теория типов и Лямбда-исчисление

  • бестиповое Лямбда-исчисление
  • Теория типов
  • простое типизированное Лямбда-исчисление, изоморфизм Карри-Говарда
  • Основы языков ML и Haskell.

Образовательные технологии

Рекомендуется перед посещением семинаров и лекций предварительно ознакомиться с программой курса и семинаров. Перед каждым семинаром желательно изучить материал последней лекции. Домашние задания выполняются в течение семестра после каждого семинара.

На семинарских занятиях используются технологии мониторинга качества образования студентов: опросные методы, анализ выполнения домашних заданий, тестирование.

Текущий контроль осуществляется в форме:

  1. Контрольной работы – в течение 1 часа или 1 пары студенты решают задачи по теме.
  2. Теста – в течение 5 минут вначале каждого семинара студенты выписывают по памяти 3-4 определения по пройденной теме.
  3. Коллоквиум – в течение 1 или 2 пар студенты, предварительно подготовив к докладу материал по теоретической части, доносят его до своих одногруппников (однокурсников), отвечая на появляющиеся вопросы привлекая преподавателя. Работа над большими темами предполагается в малых группах.

Темы для коллоквиума совпадают с вопросами по экзамену. Тесты стоятся на основе формулировок определений и теорем. Задания на контрольные работы формируются на основе учебников и задачников по соответствующим темам

Учебно-методическое и информационное обеспечение дисциплины

  1. Зюзьков В.М. Математическое введение в декларативное программирование — Электронное издание , 2003. — 83 c.
  2. Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика. // Пер. с англ. — М.: Мир, 1985. – 606 с.
  3. Братко И. Программирование на языке ПРОЛОГ для искусственного интеллекта. // М.: Мир, 1990. – 559 с.
  4. Заде Л. Понятие о лингвистической переменной и его применение к принятию решений. // М.: Мир, 1976. – 168 с.
  5. Кейслер Г., Чен Ч. Теория моделей. // М.: Мир, 1977. – с. 14.
  6. Многозначные логики и их применения: Логические исчисления, алгебры и функциональные свойства. Т.1, Т.2 // Коллектив авторов, 2008.
  7. Мышкис А.Д. Элементы теории математических моделей. // Изд.4, 2009. – 192 с.
  8. G.Metakides, A.Nerode. Principles of Logical Programming. // Elsevier. 1996. (Рус.перевод: Г.Метакидес, АНероуд, Принципы логики и логического программирования, М.: Факториал, 1998.)
  9. The Description Logic Handbook. // by: F. Baader. New York: Cambridge University Press, 2003. – 555 pp. ISBN 0-521-78176-0
  10. Ganter, Bernhard; Wille, Rudolf. Formal Concept Analysis: Mathematical Foundations. // Springer-Verlag, Berlin, 1998. – 348 pp. ISBN 3-63311-62767-5 .
  11. Ganter, Bernhard; Stumme, Gerd; Wille, Rudolf, eds. Formal Concept Analysis: Foundations and Applications. // Lecture Notes in Artificial Intelligence, no. 3626. Springer-Verlag, 2005. – 372 pp. ISBN 3-540-27891-5
  12. Отсканированные лекции по "Логическим основам программирования" одного из студентов ФИТ (Light Angel), 2009 год.
Добавить в избранное