Рабочая программа дисциплины логические основы программирования (наименование дисциплины)



Скачать 136.27 Kb.
Дата31.12.2012
Размер136.27 Kb.
ТипРабочая программа
Министерство образования и науки Российской Федерации
Государственное образовательное учреждение высшего профессионального образования

«Новосибирский государственный университет» (НГУ)
Факультет информационных технологий

УТВЕРЖДАЮ

_______________________

« ___» _____________ 20___г.

РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ

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

(наименование дисциплины)

НАПРАВЛЕНИЕ ПОДГОТОВКИ 230100 «ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»

Квалификация (степень) выпускника

Бакалавр
Форма обучения очная

Новосибирск

2011

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

(ФИО, ученая степень, ученое звание)

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

Кафедра общей информатики
1. Цели освоения дисциплины (курса)

Дисциплина (курс) «Логические основы программирования» имеет своей целью ознакомление студентов с основными понятиями логического программирования, теоретическими основами декларативного и функционального программирования, логическими основами абстрактных типов данных и логическими основами информационных технологий.

Основной целью освоения дисциплины является изучение метода резолюций, прикладных логик, ознакомление c анализом формальных понятий, основами теории типов и типизированного лямбда-исчисления.
2. Место дисциплины в структуре образовательной программы.

Дисциплина (курс) «Логические основы программирования» относится к вариативной части цикла профессиональных дисциплин ОП бакалавра.

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

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


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

ПК-26

Владеет теоретическими основами программирования, основами логического и декларативного программирования


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

ОК-1

владеет культурой мышления, способен к обобщению, анализу, восприятию информации, постановке цели и выбору путей ее достижения

ОК-2

умеет логически верно, аргументировано и ясно строить устную и письменную речь

ОК-6

стремится к саморазвитию, повышению своей квалификации и мастерства

ОК-10

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

ОК-11

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

ПК-28

владеет понятиями синтаксиса и семантики формальных языков. Владеет навыками формального представления содержательных знаний средствами формальных языков

ПК-65

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

ПК-66

Умеет применять методы теории информации и методы обработки изображений и сигналов в различных областях

ИК-4

владеет языком программирования высокого уровня Си и техникой программирования


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

  • Знать основы логического программирования, основные виды модальных и неклассических логик, логик описаний; логические основы формальной семантики языков программирования; основы теории типов и типизированного лямбда-исчисления.

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

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


4. Структура и содержание дисциплины.

Структура

Общая трудоемкость дисциплины составляет 4 зачетных единицы, 144 часа.

Объем дисциплины и виды учебной работы – 4 зачетных единицы: 1 единица на семестровый курс лекций, 1 единица на семинарские занятия в течении семестра, 1 единица – на самостоятельную работу и 1 единица – на экзамен.






п/п


Раздел

дисциплины

Семестр

Неделя семестра

Виды учебной работы, включая самостоятельную работу студентов и трудоемкость (в часах)

Формы текущего контроля успеваемости

(по неделям семестра)

Форма промежуточной аттестации

(по семестрам)














Лекции


Семинары

Самостоятельная работа

Экзамен




1

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

5

1-4

8

8

10




Контрольная

2

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

5

5-8

8

8

10




Тест

3

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

5

9-10

4

4

8




Тест

4

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

5

11-16

10

10

10




Контрольная

5

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

5

17-18

4

4

6




Контрольная

6

Экзамен







-

-

-

36

Экзамен




Всего:







34

34

44

36





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

  • Аксиоматизируемые классы, конечно-аксиоматизируемые классы, экзистенциально-(универсально-)аксиоматизируемые классы.

  • Теоремы о замкнутости классов относительно теоретико-модельных операций.

  • Скулемизация, теорема Скулема внизю

  • Теорема Мальцева о расширении.

  • Парадокс Скулема.

  • Эрбранизация. Теорема Эрбрана.


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

  • Подстановки. Унификаторы.

  • Алгоритм унификации. Теорема об унификации.

  • Резолюции. Резольвента. Понятие вывода.

  • Метод резолюций. Теорема о корректности и полноте методы резолюций.

  • Модели Эрбрана. Наименьшая модель Эрбрана. Теорема о наименьшей модели Эрбрана.

  • Множество решений программы. Теорема о множестве решений программы.

  • Теорема о полноте резолюций.

  • Алгоритмические свойства наименьшей модели Эрбрана.

  • Пруверы: Vampire, Racer.


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

  • Определение формального контекста, формального понятия.

  • Соответствия Галуа.

  • Теорема о решётке формальных понятий.

  • Импликации в формальных контекстах.


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

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

    • Аксиомы. Структуры Крипке. Примеры модальностей.

    • Теоремы об общезначимости аксиом в K, S4, M.

    • Теоремы о корректности и полноте.




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

  • Трехзначные логики Лукасевича, Клини, Геделя-Сметанича.

  • Четырехзначная логика Белнапа и отношение первопорядкового следования.

  • Нечеткие логики. Нечеткие лингвистические логики.

  • Теория приблизительных рассуждений




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

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

  • Темпоральные логики.


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

  • свободные и термальные системы, структуры данных;

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


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

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

  • Теория типов

  • простое типизированное Лямбда-исчисление, изоморфизм Карри-Говарда

  • Основы языков ML и Haskell.


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

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

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

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

1) Контрольной работы – в течение 1 часа или 1 пары студенты решают задачи по теме.

2) Теста – в течение 5 минут вначале каждого семинара студенты выписывают по памяти 3-4 определения по пройденной теме.

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

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

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

  1. Элементарные подсистемы. Элементарная и полная диаграммы.

  2. Аксиоматизируемые классы. Теория класса и класс теории.

  3. Универсально аксиоматизируемые классы.

  4. Подсистемы и элементарные подсистемы, связь с элементарной и полной диаграммами.

  5. Экзистенциально аксиоматизируемые классы.

  6. Сохранение истинности бескванторных формул на подмоделях. Элементарные подмодели и расширения.

  7. Свойства –теорий и –теорий.

  8. Свойства аксиоматизируемых классов.

  9. Модели, обогащённые константами. Свойства элементарной и полной диаграмм.

  10. Конечно аксиоматизируемые классы.

  11. Элементарная и полная диаграммы модели. Свойства.

  12. Теорема о выполнимости и опровержимости бескванторных формул на конечных моделях.

  13. Теорема о разрешимости множеств доказуемых бескванторных и универсальных формул. Следствия.


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

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

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

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

  4. Унификация, алгоритм унификации. Теорема об унификации.

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

  6. Резольвенты, метод резолюций. Теорема о полноте метода резолюций.

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

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

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

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

  1. Решётки формальных понятий. Свойства. Основная теорема.

  2. Формальные контексты и формальные понятия. Свойства оператора .


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

  1. Индуктивная модальная логика. Пропозициональные индуктивные модальные исчисления (аксиомы, правила, основные теоремы).

  2. Семантика возможных миров и вероятностная семантика для индуктивной модальной логики. Философская интерпретация индуктивных модальностей.

  3. Индукция и немонотонность вывода. Понятие о немонотонных логиках. Логики умолчаний, немонотонные модальные логики, логики очерчивания.

  4. Правила вывода с умолчаниями. Нормальные и полунормальные умолчания. Умолчания как правила выдвижения и как правила принятия гипотез.

  5. Индуктивные выводы в нечеткой логике. Понятия нечеткой информации и нечеткого множества. Нечетко истинные, нечетко ложные и нечетко близкие формулы.

  6. Правила нечеткого вывода как правила принятия гипотез с низким пороговым значением. Лотерейный парадокс в нечеткой логике.

  7. Нефальсифицируемость предпосылок правил нечеткого вывода.


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

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

  1. Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика. // Пер. с англ. — М.: Мир, 1985. – 606 с.

  2. Братко И. Программирование на языке ПРОЛОГ для искусственного интеллекта. // М.: Мир, 1990. – 559 с.

  3. Заде Л. Понятие о лингвистической переменной и его применение к принятию решений. // М.: Мир, 1976. – 168 с.

  4. Кейслер Г., Чен Ч. Теория моделей. // М.: Мир, 1977. – с. 14.

  5. Многозначные логики и их применения: Логические исчисления, алгебры и функциональные свойства. Т.1, Т.2 // Коллектив авторов, 2008.

  6. Мышкис А.Д. Элементы теории математических моделей. // Изд.4, 2009. – 192 с.

  7. G.Metakides, A.Nerode. Principles of Logical Programming. // Elsevier. 1996. (Рус.перевод: Г.Метакидес, АНероуд, Принципы логики и логического программирования, М.: Факториал, 1998.)

  8. The Description Logic Handbook. // by: F. Baader.  New York: Cambridge University Press, 2003. – 555 pp. ISBN 0-521-78176-0

  9. Ganter, Bernhard; Wille, Rudolf. Formal Concept Analysis: Mathematical Foundations. // Springer-Verlag, Berlin, 1998. – 348 pp. ISBN 3-63311-62767-5 .

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


б) дополнительная литература:

  1. Гаврилова Т. А., Муромцев Д. И. Интеллектуальные технологии в менеджменте. // Издательство Санкт-Петербургского университета, Высшая школа менеджмента, 2008 г. – 488 стр. ISBN   978-5-9924-0017-5.

  2. Карпенко А.С. Многозначные логики. // Логика и компьютер, вып.4, М:Наука, 1997.

  3. Сидоренко Е.А. Релевантная логика. // М: ИФ РАН, 2000.

  4. Символическая логика // Изд-во Санкт-Петербургского университета, Санкт-Петербург, 2005.

  5. Расева Е., Сикорский Р. Математика метаматематики. // М.Наука, 1972.

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

  7. Шрайнер П.А. Основы программирования на языке Пролог. // П.А.Шрайнер - М.: Изд-во "Интернет-университет информационных технологий - ИНТУИТ.ру", 2005 - 176 с.

  8. Финн В.К. Автоматическое порождение гипотез в интеллектуальных системах. // 2009. – 528 с.

  9. John Sowa. Knowledge Representation: Logical, Philosophical, and Computational Foundations. // Brooks/Cole, 2000. – 512 pp. ISBN 0-534-94965-7

  10. Carpineto, Claudio; Romano, Giovanni. Concept Data Analysis: Theory and Applications. // Wiley, 2004. – 220 pp. ISBN 978-0-470-85055-8 .

  11. H.Rasiowa. An algebraic approach to non-classical logic. // North-Holland, Amsterdam, 1974.

  12. Агафонов В.Н. Спецификация программ: понятийные средства и их организация. Новосибирск, Наука, 1990.


в) программное обеспечение и Интернет-ресурсы: не требуется
8. Материально-техническое обеспечение дисциплины

не требуется
Рецензент (ы) _________________________
Программа одобрена на заседании ____________________________________________

(Наименование уполномоченного органа вуза (УМК, НМС, Ученый совет)

от ___________ года.





Похожие:

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины Основы теории управления (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconПрограмма дисциплины математические и логические основы электронно
Настоящая программа дисциплины “Математические и логические основы электронно-вычислительной техники” составлена в соответствии с...
Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconПрограмма учебной дисциплины основы археологии (Наименование дисциплины (модуля) Направление подготовки
Целями освоения дисциплины «Основы археологии» являются: формирование у студентов разносторонних и системных представлений о закономерностях...
Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины (модуля) Оптика спеклов и основы статистической оптики (Наименование дисциплины (модуля)
Рф и за рубежом, обладать универсальными и предметно специализированными компетенциями, способствующими его социальной мобильности,...
Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины основы алгоритмизации и языки программирования
Программа составлена в соответствии с Государственным образовательным стандартом высшего профессионального образования направления...
Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины Теория автоматического управления (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины теория и устройство судна (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины химия полное наименование дисциплины для специальности (ей)/ направления подготовки

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины «Механика» полное наименование дисциплины

Рабочая программа дисциплины логические основы программирования (наименование дисциплины) iconРабочая программа дисциплины " Основы философии"
Дисциплина “Основы философии” относится к циклу огсэ – “Общие гуманитарные и социально-экономические дисциплины” и изучаются в объеме...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org