Difference between revisions of "BSc: IntroductionToComputerVision"
Jump to navigation
Jump to search
V.matiukhin (talk | contribs) |
V.matiukhin (talk | contribs) |
||
Line 10: | Line 10: | ||
== 2. Перечень планируемых результатов обучения == |
== 2. Перечень планируемых результатов обучения == |
||
: '''Целью освоения дисциплины''' является формирование у студентов глубоких знаний и практических навыков в области анализа, обработки и интерпретации изображений и видео с применением методов машинного и глубокого обучения. Помимо теоретических аспектов, курс акцентирует внимание на разработке и применении изученных алгоритмов с использованием современных программных инструментов и библиотек в практических заданиях, что позволяет студентам применить полученные знания на практике и получить опыт в решении актуальных задач в области компьютерного зрения и обработки видео. |
: '''Целью освоения дисциплины''' является формирование у студентов глубоких знаний и практических навыков в области анализа, обработки и интерпретации изображений и видео с применением методов машинного и глубокого обучения. Помимо теоретических аспектов, курс акцентирует внимание на разработке и применении изученных алгоритмов с использованием современных программных инструментов и библиотек в практических заданиях, что позволяет студентам применить полученные знания на практике и получить опыт в решении актуальных задач в области компьютерного зрения и обработки видео. |
||
− | |||
: '''Задачами дисциплины''' являются: |
: '''Задачами дисциплины''' являются: |
||
Line 27: | Line 26: | ||
#Методы (метрики) оценки качества изображений и видео. Область их применения, методы состязательных атак на метрики качества и методы защиты от атак. |
#Методы (метрики) оценки качества изображений и видео. Область их применения, методы состязательных атак на метрики качества и методы защиты от атак. |
||
#Концепция карты внимания (салиентности) в контексте визуального восприятия и обработки изображений. |
#Концепция карты внимания (салиентности) в контексте визуального восприятия и обработки изображений. |
||
+ | #Основы 4D видео. |
||
+ | #Теоретические основы задач классификации и детекции, принципы работы Vision Transformer (ViT) и DETR (Detection Transformer). |
||
+ | : '''Умения:''' обучающийся развил умения в следующих направлениях:<br> |
||
+ | #Применение алгоритмов и техник обработки изображений для решения конкретных задач компьютерного зрения с использованием Python. |
||
+ | #Выбор корректного алгоритма компьютерного зрения для решения рассмотренных задач компьютерного зрения. |
||
+ | #Использование методов машинного и глубокого обучения для распознавания образов, включая настройку и обучение нейросетей. |
||
+ | #Реализация алгоритмов детекции границ и объектов для извлечения полезной информации из изображений. |
||
+ | #Осуществление процесса калибровки камеры и коррекции дисторсии изображений. |
||
+ | #Создание панорам и выполнение 3D-реконструкции сцен на основе набора изображений. |
||
+ | #Реализация алгоритмов плотной 3D реконструкции и методов Structure from Motion (SfM). |
||
+ | #Анализ и применение стратегий для защиты от атак на метрики качества изображений и видео. |
||
+ | #Разработка и реализация алгоритмов трекинга и предсказания движения объектов. |
||
+ | #Использование техник выделения салиентных областей на изображениях для улучшения анализа и обработки. |
||
+ | #Применение Vision Transformer и DETR для решения задач классификации и детекции объектов. |
||
+ | : '''Навыки (владения):''' обучающийся овладел следующими навыками:<br> |
||
− | : '''Умения:''' сформированы умения |
||
+ | #Программирование на Python для реализации алгоритмов компьютерного зрения и обработки изображений. |
||
− | * представления знаний средствами математической логики на пропозициональном уровне с использованием булевской, нечеткой и вероятностной логик, |
||
+ | #Работа с библиотекой OpenCV и другими инструментами для анализа и обработки изображений и видео. |
||
− | * онтологического моделирования систем знаний о предметных областях с использованием аппарата дискрипционных логик и анализа формальных понятий, |
||
+ | #Применение предварительно обученных моделей глубокого обучения для распознавания лиц, текста и объектов на изображениях. |
||
− | * формулировать и выполнять запросы к онтологиям с использованием алгебрологических формализмов дискрипционных логик и анализа формальных понятий. |
||
− | |||
− | : '''Навыки (владения):''' сформировано владение навыками работы с такими инструментами как |
||
− | * булевские решатели (SAT- и SMT-решатели на примерe Z3), |
||
− | * фреймворки для создания и редактирования онтологий и баз знаний (на примере Protégé), |
||
− | * автоматические (например, Prover9) и полуавтоматические (на примере Coq) доказатели теорем. |
||
== 3. Структура и содержание дисциплины == |
== 3. Структура и содержание дисциплины == |
||
Line 46: | Line 54: | ||
| style="width:65%" | Содержание дисциплины по темам |
| style="width:65%" | Содержание дисциплины по темам |
||
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;" |
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 1. || Введение в компьютерное зрение |
||
− | | style="text-align:center;" | 1. || Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений |
||
| |
| |
||
+ | * Основные задачи компьютерного зрения |
||
− | * доказательства «по определению/построению», «полным перебором конечного числа случаем», «от противного» и «математической индукцией». |
||
+ | **Задача классификации |
||
− | * наивная теория множеств, числовые системы, алгебры множеств, нечетких множеств, σ-алгебры |
||
+ | **Задача детекции объектов |
||
− | * булевская пропозициональная логика, ее разрешающие процедуры и аксиоматизация, булевские решатели практика их использования |
||
+ | **Задача детекции ключевых точек |
||
− | * нечеткие и вероятностные пропозициональные логики, нечеткое и вероятностно представление знаний и вывод |
||
+ | **Semantic segmentation |
||
+ | **Instance segmentation |
||
+ | **Panoptic segmentation |
||
+ | **Image captioning |
||
+ | **Задача предсказания глубины |
||
+ | **Задача трекинга объектов |
||
+ | **Задача повышения разрешения |
||
+ | **Inpainting |
||
+ | **Задача генерации изображений |
||
+ | **Задача переноса стиля |
||
+ | *Что такое изображение |
||
+ | **Особенности человеческой визуальной системы |
||
+ | **Особенности машинного представления изображения |
||
+ | |||
|- style="background-color:#F8F9FA; color:#202122;" |
|- style="background-color:#F8F9FA; color:#202122;" |
||
− | | style="text-align:center;" | 2. || |
+ | | style="text-align:center;" | 2. || Свертки, алгоритмы детекции границ |
| |
| |
||
+ | *Математические основы операции свертки |
||
− | * общее понятие логики, логик первого и высших порядков |
||
+ | *Примеры использования сверток в обработке изображений |
||
− | * разрешимые теории, аксиоматизация и логический вывод, автоматизированное доказательство теорем |
||
+ | *Детектирование объектов и границ: методы и алгоритмы |
||
− | * знакомство с SMT-решателями и инструментами автоматического доказательства |
||
+ | *Реализация сверток и операторов для обработки изображений |
||
+ | |||
|- style="background-color:#F8F9FA; color:#202122;" |
|- style="background-color:#F8F9FA; color:#202122;" |
||
− | | style="text-align:center;" | 3. || |
+ | | style="text-align:center;" | 3. ||Нейросетевая обработка видео |
| |
| |
||
+ | *Устройство глаза, восприятие цвета |
||
− | * алгебры отношений, реляционная модель и реляционные базы данных, правила и аксиоматика Армстронга |
||
+ | *Цветовые пространства |
||
− | * частичные порядки, решетки, булевы алгебры и формальные контексты, решетки формальных понятий |
||
+ | *Устройство камеры |
||
− | * представление знаний о предметных областях в виде формальных понятий, атрибутная импликация |
||
+ | **Объектив камеры |
||
+ | **Виды сенсоров |
||
+ | **Типичные артефакты съемки |
||
+ | *Обработка изображений в камере |
||
+ | **Обработка RAW-кадра |
||
+ | **Демозаикинг |
||
+ | **Шумоподавление |
||
+ | **Цветокоррекция |
||
+ | **Тональная компрессия |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 4. || Методы сжатия данных |
||
+ | | |
||
+ | * Основы сжатия данных без потерь и с потерями |
||
+ | **Определение энтропии источника |
||
+ | **Сжатие Хаффмана |
||
+ | **Арифметическое сжатие |
||
+ | **PPM |
||
+ | **Рекуррентные нейросети в задаче сжатия |
||
+ | *Сжатие изображений |
||
+ | **JPEG |
||
+ | **JPEG 2000 |
||
+ | *Нейросетевое сжатие |
||
+ | **JPEG AI |
||
+ | **Артефакты нейросетевого сжатия |
||
+ | *Стандарты видеокодеков |
||
+ | **Компенсация движения |
||
+ | **BSQ-rate |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 5. ||Введение в реконструкцию 3D-сцен |
||
+ | | |
||
+ | *Преобразование Хафа |
||
+ | *Линейные преобразования изображений |
||
+ | *Перспективные преобразования изображений |
||
+ | *RANSAC |
||
+ | *Реконструкция 3D-сцены |
||
+ | **SfM (Structure from motion) |
||
+ | **VO (Visual odometry) |
||
+ | *Калибровка камеры |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 6. || Реконструкция 3D-сцены |
||
+ | | |
||
+ | *Модели камеры |
||
+ | **Модель рыбьего глаза |
||
+ | **Камера-обскура |
||
+ | **Стеноп (пинхол камера) |
||
+ | *Внутренние (intrinsic) и внешние (extrinsic) парметры камеры |
||
+ | *Радиальная дисторция |
||
+ | *Распознавание ключевых точек |
||
+ | **Детекция углов (Детектор Харриса) |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 7. || Атаки на методы оценки визуального качества изображений/видео |
||
+ | | |
||
+ | *Введение в состязательные атаки |
||
+ | *Состязательные атаки методами черного ящика |
||
+ | *Состязательные атаки методами белого ящика |
||
+ | *Бенчмарк устойчивости метрик |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 8. || Методы защиты от атак на методы оценки визуального качества изображений/видео |
||
+ | | |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 9. || Задача трекинга, предсказание движения |
||
+ | | |
||
+ | *Постановка задачи трекинга |
||
+ | *Single object tracking |
||
+ | *Online tracking |
||
+ | **SORT |
||
+ | **DeepSORT |
||
+ | **Trackformer |
||
+ | **CenterTrack |
||
+ | **PermaTrack |
||
+ | *Motion prediction |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 10. ||4D-видео |
||
+ | | |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 11. || Карты внимания (салиентность) |
||
+ | | |
||
+ | *Постановка задачи предсказания карт внимания |
||
+ | *Применение в индустрии |
||
+ | *Метрики качества |
||
+ | *Обзор методов для изображений |
||
+ | **Center Prior |
||
+ | **MSI-Net |
||
+ | *Обзор методов для видео |
||
+ | **TASED-Net |
||
+ | **UNISAL |
||
+ | **VINet |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 12. || Архитектура трансформера в задачах компьютерного зрения. ViT и DETR |
||
+ | | |
||
+ | *Теоретические основы архитектуры Трансформер |
||
+ | *Архитектура ViT |
||
+ | *Архитектура DETR |
||
+ | |||
+ | |- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 13. || Компьютерное зрение в автономном вождении |
||
+ | | |
||
+ | |||
|- style="background-color:#F8F9FA; color:#202122;" |
|- style="background-color:#F8F9FA; color:#202122;" |
||
+ | | style="text-align:center;" | 14. || Мультимодальные модели в компьютерном зрении |
||
− | | style="text-align:center;" | 4. || Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений |
||
| |
| |
||
+ | *Задача OCR |
||
− | * алгебры бинарных отношений, системы переходов и моделями Крипке, их использование для представления времени, событий, мнений и знаний о предметных областях |
||
+ | *Задача Image Captioning |
||
− | * классические пропозициональные модальные, темпоральные и эпистемические логики, их разрешимость и аксиоматезируемость |
||
− | * дискрипционные логики их синтаксис, семантика, использование для представления баз знаний и языков запросов к базам знаний |
||
|} |
|} |
||
Revision as of 19:55, 3 April 2024
Компьютерное зрение и обработка видео
- Квалификация выпускника: бакалавр
- Направление подготовки: 09.03.01 - “Информатика и вычислительная техника”
- Направленность (профиль) образовательной программы: Математические основы ИИ
- Программу разработал(а): Д.С. Ватолин
1. Краткая характеристика дисциплины
- Изучение дисциплины обеспечивает формирование и развитие компетенций обучающихся в области компьютерного зрения и обработки видео, их применение для решения различных прикладных задач в рамках профессиональной деятельности. В ходе освоения дисциплины обучающиеся рассматривают основы и продвинутые методы компьютерного зрения и обработки видео: применение сверточных фильтров в задачах обнаружения границ, сжатие видео, основы 4D-видео, реконструкция 3D-сцен, задачи трекинга и предсказания областей внимания (салиентных областей), а также состязательные атаки на метрики качества изображений/видео и методы защиты от них.
2. Перечень планируемых результатов обучения
- Целью освоения дисциплины является формирование у студентов глубоких знаний и практических навыков в области анализа, обработки и интерпретации изображений и видео с применением методов машинного и глубокого обучения. Помимо теоретических аспектов, курс акцентирует внимание на разработке и применении изученных алгоритмов с использованием современных программных инструментов и библиотек в практических заданиях, что позволяет студентам применить полученные знания на практике и получить опыт в решении актуальных задач в области компьютерного зрения и обработки видео.
- Задачами дисциплины являются:
- освоение принципов и практик компьютерного зрения и обработки изображений и видео с использованием классических алгоритмов, машинного и глубокого обучения;
- изучение математических основ наиболее важных алгоритмов компьютерного зрения;
- изучение областей и условий применимости алгоритмов компьютерного зрения и обработки видео;
- применение изученных алгоритмов в практическом решении задач компьютерного зрения и обработки видео.
Общая характеристика результата обучения по дисциплине
- Знания: обучающийся получил систематические знания в следующих областях:
- Основы компьютерного зрения и обработки изображений: понимание принципов работы с изображениями и видео, включая их сжатие, восстановление, классификацию и сегментацию.
- Методы машинного обучения и глубокого обучения: знание алгоритмов и моделей, применяемых для распознавания образов, включая свёрточные нейронные сети.
- Алгоритмы детекции границ и объектов: понимание методов поиска границ, линий и объектов на изображениях, включая преобразование Хафа и метод RANSAC.
- Методы калибровки камеры, перспективные преобразования изображений.
- Принципы создания панорам и 3D-реконструкции: освоение методов сшивки изображений (стичинг) и построения трехмерных моделей сцен.
- Методы (метрики) оценки качества изображений и видео. Область их применения, методы состязательных атак на метрики качества и методы защиты от атак.
- Концепция карты внимания (салиентности) в контексте визуального восприятия и обработки изображений.
- Основы 4D видео.
- Теоретические основы задач классификации и детекции, принципы работы Vision Transformer (ViT) и DETR (Detection Transformer).
- Умения: обучающийся развил умения в следующих направлениях:
- Применение алгоритмов и техник обработки изображений для решения конкретных задач компьютерного зрения с использованием Python.
- Выбор корректного алгоритма компьютерного зрения для решения рассмотренных задач компьютерного зрения.
- Использование методов машинного и глубокого обучения для распознавания образов, включая настройку и обучение нейросетей.
- Реализация алгоритмов детекции границ и объектов для извлечения полезной информации из изображений.
- Осуществление процесса калибровки камеры и коррекции дисторсии изображений.
- Создание панорам и выполнение 3D-реконструкции сцен на основе набора изображений.
- Реализация алгоритмов плотной 3D реконструкции и методов Structure from Motion (SfM).
- Анализ и применение стратегий для защиты от атак на метрики качества изображений и видео.
- Разработка и реализация алгоритмов трекинга и предсказания движения объектов.
- Использование техник выделения салиентных областей на изображениях для улучшения анализа и обработки.
- Применение Vision Transformer и DETR для решения задач классификации и детекции объектов.
- Навыки (владения): обучающийся овладел следующими навыками:
- Программирование на Python для реализации алгоритмов компьютерного зрения и обработки изображений.
- Работа с библиотекой OpenCV и другими инструментами для анализа и обработки изображений и видео.
- Применение предварительно обученных моделей глубокого обучения для распознавания лиц, текста и объектов на изображениях.
3. Структура и содержание дисциплины
№ п/п |
Наименование раздела дисциплины |
Содержание дисциплины по темам |
1. | Введение в компьютерное зрение |
|
2. | Свертки, алгоритмы детекции границ |
|
3. | Нейросетевая обработка видео |
|
4. | Методы сжатия данных |
|
5. | Введение в реконструкцию 3D-сцен |
|
6. | Реконструкция 3D-сцены |
|
7. | Атаки на методы оценки визуального качества изображений/видео |
|
8. | Методы защиты от атак на методы оценки визуального качества изображений/видео | |
9. | Задача трекинга, предсказание движения |
|
10. | 4D-видео | |
11. | Карты внимания (салиентность) |
|
12. | Архитектура трансформера в задачах компьютерного зрения. ViT и DETR |
|
13. | Компьютерное зрение в автономном вождении | |
14. | Мультимодальные модели в компьютерном зрении |
|
4. Методические и оценочные материалы
Задания для практических занятий:
№ п/п |
Наименование раздела дисциплины (модуля) |
Перечень рассматриваемых тем (вопросов) |
1. | Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений |
|
2. | Общее понятие логической системы, разрешимости и логического вывода |
|
3. | Алгебраический подход к представлению баз данных и знаний |
|
4. | Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений |
|
Текущий контроль успеваемости обучающихся по дисциплине:
№ п/п |
Наименование раздела дисциплины | Форма текущего контроля | Материалы текущего контроля |
1. | Наивная теория множеств, пропозициональные логики для представления знаний и рассуждений | Письменная домашняя контрольная работа с устным опросом в классе |
|
2. | Общее понятие логической системы, разрешимости и логического вывода | Письменная домашняя контрольная работа с устным опросом в классе |
|
3. | Алгебраический подход к представлению баз данных и знаний | Письменная домашняя контрольная работа с устным опросом в классе |
|
4. | Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений | Письменная домашняя контрольная работа с устным опросом в классе |
|
Контрольные вопросы для подготовки к промежуточной аттестации:
№ п/п |
Наименование раздела дисциплины |
Вопросы |
1. | Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений |
|
2. | Общее понятие логической системы, разрешимости и логического вывода |
|
3. | Алгебраический подход к представлению баз данных и знаний |
|
4. | Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений |
|
Вопросы/Задания к промежуточной аттестации в устной/письменной форме:
- Приведите примеры из курса Математического анализа «доказательства по определению/построению» «доказательство полным перебором конечного числа случаев», «доказательство от противного» и «доказательство математической индукцией».
- Перечислите постулаты наивной теории множеств и сравните их с аксиомами теорией множеств первого порядка (например, ZFC)
- Дайте определение алгебраической системы, алгебры, предикатной модели. Приведите примеры алгебраических систем, используемых в курсе Математического анализа.
- Дайте определение (как в курсе) множества натуральных чисел с операциями сложения, умножения, и равенства, используя наивную теорию множеств). Докажите, что в этой алгебраической системе выполняется «обычное» равенство 1+2=3.
- Предполагая, что натуральные числа со сложением и умножением уже определены, дайте определение (как в курсе) множества целых чисел с операциями сложения, умножения, и равенства используя наивную теорию множеств). Докажите, что в этой алгебраической системе выполняется «обычное» равенство 1+-1=0.
- Дайте определение (как в курсе) понятие алгебры нечетких множеств с операциями объединения, пересечения, разности и предикатами принадлежности, включения и равенства, докажите непротиворечивость этого понятия (в контексте наивной теории множеств).
- Дайте определение (как в курсе) понятие σ-алгебры, докажите непротиворечивость этого понятия (в контексте наивной теории множеств).
- Дайте определение (как в курсе) булевой алгебры множеств. Докажите, что любая конечная булева алгебра множеств состоит из 2^n элементов (где n – некоторое натуральное число).
- Дайте определение (как в курсе) булевской пропозициональной. Докажите, что всякое тождество булевых алгебр является тождественно истинной эквивалентностью булевской пропозициональной логики. Верно ли обратное? (Докажите ответ.)
- Дайте определение (как в курсе) понятия канонической модели для булевской пропозициональной логики. Докажите, что булевская пропозициональная логика имеет каноническую модель (таблицу истинности).
- Докажите полноту и корректность метода DPLL проверки выполнимости формул пропозициональной булевской логики. Приведите примеры формул, когда этот метод дает существенный выигрыш по сравнению с таблицей истинности.
- Дайте определение (как в курсе) аксиоматизации пропозициональной булевской логики, докажите ее корректность, непротиворечивость и полноту.
- Дайте определение нечеткой пропозициональной логики и истинности для формул этой логики. Как связана истинность в пропозициональных вариантах нечеткой и булевской логике? (Ответ доказать.)
- Дайте определение вероятностной пропозициональной логики и истинности для формул этой логики. Как связана истинность в пропозициональных вариантах вероятностной и булевской логике? (Ответ доказать.)
- Приведите примеры (как из курса, так и дополнительные, если возможно) применения пропозициональных булевской, нечеткой и вероятностной логики для представления данных, знаний и рассуждений.
- Дайте определение формального языка (как множества слов). Определите формализм (расширенных) форм Бэкуса-Наура. Используя этот формализм, определите синтаксис пропозициональной булевской логики.
- Определите иерархию множеств по степеням (power-set). Докажите, что конечного базового множества эта иерархия бесконечна.
- Дайте пример логики первого и второго порядка с общей сигнатурой и семантикой над множеством (всех) вещественных чисел, и примеры теорем из курса Математического анализа, для записи которых предложенная логика первого порядка не подходит, а логика второго порядка – подходит.
- Сформулируйте Основную теорему анализа и Основную теорему алгебры. Каков порядок этих утверждений?
- Дайте определение логической теории (как в курсе), противоречивой и непротиворечивой теории, полной и неполной теории. Как задать логическую теорию, имея множество логических формул? Как задать логику, имея множество моделей (алгебраических систем)?
- Дайте (как в курсе) общее понятие «аксиоматической системы гильбертовского типа», доказательства и логического вывода в системе гильбертовского типа. Приведите пример вывода/доказательства в системе гильбертовского типа истинной формулы пропозициональной булевской формулы.
- Дайте (как в курсе) общее понятие «аксиоматической системы генценовского типа», доказательства и логического вывода в системе генценовского типа. Приведите пример вывода/доказательства в системе генценовского типа истинной формулы пропозициональной булевской формулы.
- Дайте определение Теории неинтерпретированного равенства? Является ли теорией эта Теория? Противоречива ли она, полна ли? (Ответ обосновать.)
- Дайте определение арифметики Пресбургера. Приведите пример использования арифметики Пресбургера над натуральными числами для выражения свойств индексных выражений для массивов в языках программирования. Докажите разрешимость арифметики Пресбургера рациональных чисел.
- Дайте определение арифметики Пеано. Докажите коммутативность умножения в арифметике Пеано. Сформулируйте первую и вторую теоремы Геделя о неполноте (без доказательства).
- Что такое стандартная и нестандартные модели арифметики? Приведите два неизоморфных примера нестандартной модели арифметики.
- Сформулируйте аксиоматику Тарского для поля вещественных чисел. Докажите, что каждое вещественное число может быть представлено в (любо) системе счисления в виде (конечной) целой части и (может быть, бесконечной) дробной части.
- Дайте определение теория первого порядка поля вещественных чисел. Расскажите об общем плане доказательства разрешимости этой теории методом элиминации кванторов (как в курсе).
- Метод (индуктивных утверждений) Флойда и аксиоматическая семантика (языка Pascal) Хоара как основа спецификации и (ручной и полуавтоматической) верификации программ.
- Дайте определение алгебр бинарных отношений. Существует ли каноническая алгебра бинарных отношений? Разрешима ли эквициональная теория алгебры бинарных отношений? (Ответы на вопросы доказать.)
- Дайте определение алгебр Клини. Существует ли каноническая алгебра Клини? Разрешима ли эквициональная теория алгебр Клини? Как алгебры Клини связаны с алгеброй бинарных отношений? (Ответы на вопросы доказать.)
- Дайте определение реляционных алгебр. Существует ли каноническая реляционная алгебра? Разрешима ли эквициональная теория реляционных алгебр? Как алгебра бинарных отношений описывается в терминах реляционных алгебр? (Ответы на вопросы доказать.)
- Что такое базис операций реляционных алгебр? Приведите примеры (полных) базисов операций (с доказательством). Дайте определение первых четырех нормальных форм в теории реляционных алгебр и объясните, поему любое выражение реляционных алгебр «нормализуемо» (т. е., приводимо к этим формам).
- Что такое реляционная модель Кодда? Дайте определение аксиоматики Армстронга, докажите ее корректность и полноту.
- Дайте определение предпорядков, частичных порядков и линейных порядков. Докажите изоморфизм любых счетных всюду плотных линейных порядка без наибольшего и наименьшего элементов.
- Дайте определение решеток и полных решеток, булевых алгебр. Приведите примеры алгебраических систем разделяют эти перечисленные классы.
- Дайте основные определения анализа формальных понятий: формальный контекст, операции содержания атрибутной спецификации и атрибутная спецификация содержания в формальном контексте, атрибутной импликации. Как связаны эти операции с поиском по ключевым словам, как могут быть использован в рекомендательных системах?
- Дайте определение что такое формальное понятие в формальном контексте. Докажите, что формальные понятия (над фиксированным формальным контекстом) образуют полную решетку.
- Сформулируйте Основную теорему анализа формальных понятий. Докажите ее для конечных решеток и формальных контекстов.
- Приведите 1-2 алгоритма рисования графов (из курса) и проиллюстрируйте применение одно из них для визуализации решетки формальных понятий.
- Дайте определения шкалы и модели Крипке, системами (помеченных) переходов. Приведите римеры. Объясните, почему алгебры бинарных отношений определяют шкалы Крипке со счетным множеством (программных) агентов.
- Приведите примеры применения помеченных переходов и моделей Крипке для моделирования (дискретного) времени, процессов и знаний о предметных областях.
- Дайте семантическое определение классических пропозициональных модальных логик K, S4 и S5, приведите аксиоматизации этих логик (как в курсе), докажите корректность одной из них, непротиворечивость другой, и полноту – третьей (по выбору).
- Дайте определение понятия каноническая («малая») модель. Докажите существование канонической модели для одной из пропозициональных модальных логик K, S4 и S5 (по выбору). Дкаите разрешимость одной из пропозициональных модальных логик K, S4 и S5 (по выбору).
- Дайте семантическое определение логики линейного времени LTL. Докажите разрешимость этой логики, приведите ее аксиоматизацию (как в курсе).
- Дайте семантическое определение логики ветвящегося времени CTL. Докажите разрешимость этой логики, приведите ее аксиоматизацию (как в курсе).
- Дайте определение эпистемическая логика Kn, сравните ее с логикой S5. Разрешима ли, аксиоматизируема ли эта эпистемическая логика, обладает ли свойствами малой или конечной модели? (Без доказательств.)
- Дайте определение понятиям «групповое знание», «распределенное знание» и «общее знание». Как перечисленные конструкции выражаются через знания индивидуальных агентов с использованием операций алгебры бинарных отношений и конструктора неподвижной точки?
- Дайте семантическое определение класса дискрипционных логик и определение дискрипционной логики ACL, сравните ее с логикой K. Разрешима ли, аксиоматизируема ли эта дискрипционная логика, обладает ли свойствами малой или конечной модели? (Без доказательств.)
- Дайте определение понятия «формальная онтология», модель открытого и замкнутого мира. Объясните (на примерах) как формальные онтологии представляют знания о предметных областях, как формальные онтология специфицируется средствами дискрипционных логик и как дискрипционные логии используются для запросов к формальным онтологиям.
- Дайте 1-2 примера (из курса) логической разрешающей процедуры, относящейся к классу табличных методов (tablo). Как этот метод используется (и для каких дискрипционных логик) для извлечения знаний из спецификации формальной онтологии? (Приведите пример.)
Перечень учебно-методического обеспечения дисциплины
Список основной литературы:
- А.К. Гуц: Математическая логика и теория алгоритмов. Омск: Наследие. Диалог-Сибирь, 2003. – 108 с.
- Ю.Л. Ершов, Е.А. Палютин: Математическая логика. М.: Физматлит. 2011 (6-е издание). – 356 с.
- В.И. Маркин, В.А. Бочаров: Введение в логику. М.: ИД Форум, 2008. – 560 с.
Список дополнительной литературы:
- Wasilewska: Logics for Computer Science. Classical and Non-Classical. Springer Cham. 2018. – 535 p.
- Handbook of Knowledge Representation. Elitors: Frank van Harmelen, Vladimir Lifschitz, Bruce Porter. Elsevier Science, 2008. – 988 p.
- D.I. Ignatov: Introduction to Formal Concept Analysis and Its Applications in Information Retrieval and Related Fields. In: Braslavski, P., Karpov, N., Worring, M., Volkovich, Y., Ignatov, D.I. (eds) Information Retrieval. RuSSIR 2014. Communications in Computer and Information Science, vol 505. Springer, Cham. P. 42-141.
- А.И. Орлов, Е.В. Луценко: Анализ данных, информации и знаний в системной нечеткой интервальной математике: научная монография. — Краснодар: КубГАУ, 2022. – 405 с.
- К. Дж. Дейт: Введение в системы баз данных. М.: Вильямс, 2005 (8-е издание). – 1328 с.
- R. Fagin, J.Y. Halpern, Y. Moses, M.Y. Vardi: Reasoning About Knowledge. The MIT Press. 1995. – 390 p.
Методические указания для обучающихся по освоению дисциплины
Вид учебных занятий/деятельности |
Деятельность обучающегося |
Лекция | Написание конспекта лекций: кратко, схематично, последовательно фиксировать основные положения лекции, выводы, формулировки, обобщения; помечать важные мысли, выделять ключевые слова, термины. Обозначить вопросы, термины или другой материал, который вызывает трудности, пометить и попытаться найти ответ в рекомендуемой литературе. Если самостоятельно не удается разобраться в материале, необходимо сформулировать вопрос и задать преподавателю на консультации, во время семинарского (практического) занятия. |
Практическое (семинарское) занятие | При подготовке к семинарскому (практическому) занятию необходимо проработать материалы лекций, основной и дополнительной литературы по заданной теме. На основании обработанной информации постараться сформировать собственное мнение по выносимой на обсуждение тематике. Обосновать его аргументами, сформировать список источников, подкрепляющих его. Во время семинарского (практического) занятия активно участвовать в обсуждении вопросов, высказывать аргументированную точку зрения на проблемные вопросы. Приводить примеры из источниковой базы и научной и/или исследовательской литературы. |
Устный/письменный опрос | Отвечать, максимально полно, логично и структурировано, на поставленный вопрос. Основная цель – показать всю глубину знаний по конкретной теме или ее части. |
Подготовка к промежуточной аттестации | При подготовке к промежуточной аттестации необходимо проработать вопросы по темам, которые рекомендуются для самостоятельной подготовки. При возникновении затруднений с ответами следует ориентироваться на конспекты лекций, семинаров, рекомендуемую литературу, материалы электронных и информационных справочных ресурсов, статей. Если тема вызывает затруднение, четко сформулировать проблемный вопрос и задать его преподавателю. |
Практические (лабораторные) занятия | Практические занятия предназначены прежде всего для разбора отдельных сложных положений, тренировки аналитических навыков, а также для развития коммуникационных навыков. Поэтому на практических занятиях необходимо участвовать в тех формах обсуждения материала, которые предлагает преподаватель: отвечать на вопросы преподавателя, дополнять ответы других студентов, приводить примеры, задавать вопросы другим выступающим, обсуждать вопросы и выполнять задания в группах. Работа на практических занятиях подразумевает домашнюю подготовку и активную умственную работу на самом занятии. Работа на практических занятиях в форме устного опроса заключается прежде всего в тренировке навыков применять теоретические положения к самому разнообразному материалу. В ходе практических занятий студенты работают в группах для обсуждения предлагаемых вопросов. |
Самостоятельная работа | Самостоятельная работа состоит из следующих частей: 1) чтение учебной, справочной, научной литературы; 2) повторение материала лекций; 3) составление планов устных выступлений; 4) подготовка видеопрезентации. При чтении учебной литературы нужно разграничивать для себя материал на отдельные проблемы, концепции, идеи. Учебную литературу можно найти в электронных библиотечных системах, на которые подписан АНО Университет Иннополис. |
Контрольная работа | При подготовке к контрольной работе необходимо проработать материалы лекций, семинаров, основной и дополнительной литературы по заданной теме. |
Индивидуальная работа | При выполнение индивидуальной работы необходимо взять задание у преподавателя, ознакомиться с требованиями к выполнению работы, изучить поставленную проблему, найти решение проблемы. Если самостоятельно не удается разобраться в материале, необходимо сформулировать вопрос и задать преподавателю на консультации, во время семинарского (практического) занятия. Оформить результаты работы. |
Методы и технологии обучения, способствующие формированию компетенции
Методы и технологии обучения, способствующие формированию компетенции |
Традиционные технологии (классно-урочная система) |
Программного обеспечения Prover9, Protégé (2-пунктная лицензия BSD) и Z3 (MIT License), использование которого свободно допускается в учебном процесе и в демонстрационных целях. |