Компьютерное зрение и обработка видео

Квалификация выпускника: бакалавр

Направление подготовки: 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.	Введение в компьютерное зрение	Основные задачи компьютерного зрения Задача классификации Задача детекции объектов Задача детекции ключевых точек Semantic segmentation Instance segmentation Panoptic segmentation Image captioning Задача предсказания глубины Задача трекинга объектов Задача повышения разрешения Inpainting Задача генерации изображений Задача переноса стиля Что такое изображение Особенности человеческой визуальной системы Особенности машинного представления изображения
2.	Свертки, алгоритмы детекции границ	Математические основы операции свертки Примеры использования сверток в обработке изображений Детектирование объектов и границ: методы и алгоритмы Реализация сверток и операторов для обработки изображений
3.	Нейросетевая обработка видео	Устройство глаза, восприятие цвета Цветовые пространства Устройство камеры Объектив камеры Виды сенсоров Типичные артефакты съемки Обработка изображений в камере Обработка RAW-кадра Демозаикинг Шумоподавление Цветокоррекция Тональная компрессия
4.	Методы сжатия данных	Основы сжатия данных без потерь и с потерями Определение энтропии источника Сжатие Хаффмана Арифметическое сжатие PPM Рекуррентные нейросети в задаче сжатия Сжатие изображений JPEG JPEG 2000 Нейросетевое сжатие JPEG AI Артефакты нейросетевого сжатия Стандарты видеокодеков Компенсация движения BSQ-rate
5.	Введение в реконструкцию 3D-сцен	Преобразование Хафа Линейные преобразования изображений Перспективные преобразования изображений RANSAC Реконструкция 3D-сцены SfM (Structure from motion) VO (Visual odometry) Калибровка камеры
6.	Реконструкция 3D-сцены	Модели камеры Модель рыбьего глаза Камера-обскура Стеноп (пинхол камера) Внутренние (intrinsic) и внешние (extrinsic) парметры камеры Радиальная дисторция Распознавание ключевых точек Детекция углов (Детектор Харриса)
7.	Атаки на методы оценки визуального качества изображений/видео	Введение в состязательные атаки Состязательные атаки методами черного ящика Состязательные атаки методами белого ящика Бенчмарк устойчивости метрик
8.	Методы защиты от атак на методы оценки визуального качества изображений/видео
9.	Задача трекинга, предсказание движения	Постановка задачи трекинга Single object tracking Online tracking SORT DeepSORT Trackformer CenterTrack PermaTrack Motion prediction
10.	4D-видео
11.	Карты внимания (салиентность)	Постановка задачи предсказания карт внимания Применение в индустрии Метрики качества Обзор методов для изображений Center Prior MSI-Net Обзор методов для видео TASED-Net UNISAL VINet
12.	Архитектура трансформера в задачах компьютерного зрения. ViT и DETR	Теоретические основы архитектуры Трансформер Архитектура ViT Архитектура DETR
13.	Компьютерное зрение в автономном вождении
14.	Мультимодальные модели в компьютерном зрении	Задача OCR Задача Image Captioning

4. Методические и оценочные материалы

Задания для практических занятий:

№ п/п	Наименование раздела дисциплины (модуля)	Перечень рассматриваемых тем (вопросов)
1.	Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений	Приведите примеры доказательств «по определению/построению», «полным перебором конечного числа случаев», «от противного» и «математической индукцией». Докажите существование объединения, пересечения, произведения и степени множеств в наивной теории множеств. Докажите (в наивной теории множеств) существование множества натуральных чисел и построите натуральные числа 0, 1 и 2 в наивной теории множеств. Докажите (в наивной теории множеств) существование множества рациональных чисел и постройте рациональное число -1⁄2 в наивной теории множеств. Докажите (в наивной теории множеств) существование множества вещественных чисел и докажите существование числа √2 в наивной теории множеств. Для каких натуральных n существует алгебра множеств, состоящая из n множеств, замкнутая относительно пересечений, объединений и дополнений? Докажите непротиворечивость понятия σ-алгебры. Для каких натуральных n существует σ-алгебра, состоящая из n множеств? Приведите пример булевской формулы, которую легко доказать в системе нормального вывода, но трудно проверить ее невыполнимость методом DPLL. Приведите пример (если возможно) тождественно истинной булевской формулы, которая при каком-либо означивании ее как формулы нечеткой и/или вероятностной логики получает значение <0.5 и <1 соотвественно.
2.	Общее понятие логической системы, разрешимости и логического вывода	Приведите примеры свойств вещественных чисел, описываемых на языке первого, второго и высших порядков. Приведите примеры эквивалентных гильбертовской и генценовской аксиоматизаций. Приведите пример аксиоматизаций (первого и второго порядка) натуральных чисел. Приведите пример аксиоматизаций (первого и второго порядка) вещественных чисел. Докажите существование (поля) комплексных чисел. Приведите примеры разрешимых теорий натуральных, рациональных и вещественных чисел. Приведите примеры неразрешимых теорий натуральных, рациональных и вещественных чисел. Выполните доказательство простейших свойств в системе Z3. Выполните доказательство простейших свойств в системе Prover9.
3.	Алгебраический подход к представлению баз данных и знаний	В чем разница алгебры бинарных отношений и алгебры отношений (т. е. реляционной алгебры)? Разрешима ли алгебра бинарных отношений? Разрешима ли реляционная алгебра? Аксиоматизируема ли алгебра бинарных отношений? Аксиоматизируема ли реляционная алгебра? Приведите примеры операций реляционной алгебры, выразимых через другие операции. Приведите примеры частичного порядка, который не является решеткой и решетки, которая не является полной решеткой. Приведите пример формального контекста и постройте решетку формальных понятий для этого контекста. Перечислите все атрибутные импликации верные в этой решетке. Приведите пример конечной решетки и постройте формальный контекст, решетка формальных понятий которого изоморфна данной решетке. Обсудите алгоритмы рисования графов для визуализации решеток формальных понятий. Представьте в виде формального контекста знания о предложенной предметной области (например, учебные курсы и их зависимостей), воспользуйтесь свободно распространяемыми инструментами работы с формальными контекстами (например, ToscanaJ) для анализа этого формального контекста.
4.	Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений	Для программы с конечным числом состояний постройте соответствующую ей систему переходов и ее дерево вычислений. Для заданной формулы пропозициональной модальной логики (например K) постройте ее каноническую модель. Приведите примеры разрешимых пропозициональных модальных, временных логик и программных логик. Приведите примеры неразрешимых пропозициональных модальных, временных логик или программных логик. Приведите примеры аксиоматизаций пропозициональных модальных, временных, эпистемических логик. Для заданной эпистемичекой головоломки постройте ее аксиоматизацию на языке пропозициональной эпистемической логики. Для заданной эпистемической головоломке постройте модель Крипке и логический запрос (на языке пропозициональной модальной, временной и/или эпистемической логики), решающего в этой модели данную головоломку. Какую решающую процедуру для этого надо применить? Постройте и обоснуйте корректность алгоритма «перевода» дискриционнй логики ALC в логику первого порядка с одной свободной переменной. Приведите примеры предметных областей, удовлетворяющих гипотезе о закрытом мире. Приведи примеры предметных областей, неудовлетворяющих гипотезе зарытого мира, объясните, почему мир этих предметных областей существенно открытый. Представьте в виде формальной онтологии знания о предложенной предметной области (например, учебные курсы и их зависимостей), воспользуйтесь системой Protégé для анализа этого формального контекста.

Текущий контроль успеваемости обучающихся по дисциплине:

№ п/п	Наименование раздела дисциплины	Форма текущего контроля	Материалы текущего контроля
1.	Наивная теория множеств, пропозициональные логики для представления знаний и рассуждений	Письменная домашняя контрольная работа с устным опросом в классе	Разберите какие методы доказательства использованы в приведенном в курсе доказательстве иррациональности числа √2. Докажите существование картежей (упорядоченных наборов любой заданной фиксированной длины) в наивной теории множеств. Докажите (в наивной теории множеств) существование множества целых чисел и построите целые числа 0, +1 и -2 в наивной теории множеств. Докажите (в наивной теории множеств) существование множества отрицательных рациональных чисел и постройте рациональное число -2 в наивной теории множеств. Докажите (в наивной теории множеств) существование множества иррациональных чисел и докажите принадлежность числа √2 этому множеству. Постройте алгебру множеств, состоящая из 2^3 множеств, замкнутую относительно пересечений, объединений и дополнений. Приведите пример σ-алгебры из 2^4 конечных множеств, которая не является алгеброй всех подмножеств некоторого конечного множества. Приведите пример булевской формулы, которую экспоненциально трудно доказать в системе нормального вывода, но легко проверить ее невыполнимость методом DPLL. Приведите пример (если возможно) тождественно ложной булевской формулы, которая при каком-либо означивании ее как формулы нечеткой и/или вероятностной логики получает значение >0.5 и >0 соотвественно.
2.	Общее понятие логической системы, разрешимости и логического вывода	Письменная домашняя контрольная работа с устным опросом в классе	Можно ли записать на языке первого порядка в сигнатуре поля для заданного натурального n утверждение, что любое уравнение степени не более n имеет корень? Докажите заданную истинную формулу пропозициональной булевской логики в гильбертовом исчислении, определенном в курсе лекций для пропозициональной булевской логики. Докажите заданную истинную формулу пропозициональной булевской логики в генценовском исчислении, определенном в курсе лекций для пропозициональной булевской логики. Выполните доказательство заданной истинной эквациональной формулы первого порядка в теории не интерпретированного равенства. Докажите коммутативность умножения в аксиоматике Пеано. Докажите, что существование бесконечно малых чисел противоречит аксиоматизации Тарского поля вещественных чисел. Можно ли записать на языке первого порядка в теории поля вещественных чисел утверждение, что любое алгебраическое уравнение степени имеет корень? Докажите разрешимость арифметики Пресбургера натуральных чисел, обогащенных унарными операциями умножения на целые константы. Приведите пример (с объяснением) утверждения, которое записывается на языке арифметики Пеано, но ни оно само, ни его отрицание недоказуемы в этой аксиоматической теории.
3.	Алгебраический подход к представлению баз данных и знаний	Письменная домашняя контрольная работа с устным опросом в классе	Для данных равенств, записанных на языке алгебры бинарных отношений, доказать, какие из них являются тождествами, а какие не являются. Для данных равенств, записанных на языке реляционных алгебр, доказать, какие из них являются тождествами, а какие не являются. Доказать, что алгебра бинарных отношений является алгеброй Клини. Приведите пример минимального базиса операций реляционных алгебр, докажите минимальность этого базиса Существует ли полная решетка, которая не является булевой алгеброй? (Докажите свой ответ.) По заданному формальному контексту постройте решетку его формальных понятий, перечислите все атрибутные импликации верные в этой решетке (с обоснованием полноты перечисления). По заданной конечной решетке постройте формальный контекст, решетка формальных понятий которого изоморфна данной решетке. По заданной информации о родственных связях внутри (игрушечной) семьи, построите формальный контекст, решетку формальных понятий и перечислите все атрибутные импликации, которые имеют место (с обоснованием полноты перечисления).
4.	Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений	Письменная домашняя контрольная работа с устным опросом в классе	Для заданной программы постройте ее булевозначную модель, соответствующую этой модели систему переходов и ее дерево вычислений. Для заданной формулы пропозициональной модальной логики (например S5) постройте ее каноническую модель. Для заданной формулы пропозициональной модальной, темпоральной или программной логики, обладающей свойством конечной модели, выполните алгоритм проверки выполнимости этой формулы с использованием свойства конечной модели. Для заданной формулы пропозициональной модальной, темпоральной или программной логики, имеющей табличную разрешающую процедуру, выполните алгоритм проверки выполнимости этой формулы с использованием этой процедуры. Для заданной эпистемической головоломке постройте модель Крипке и логический запрос (на языке пропозициональной модальной, временной и/или эпистемической логики), решающего в этой модели данную головоломку. Какую решающую процедуру для этого надо применить? По заданной информации о родственных связях внутри (игрушечной) семьи, и по описанию/определению родственных связей в терминах ролей «родитель-ребенок», «супруг-супруг», построите формальную онтологию этой семьи, задав минимальное количество аксиом. По спецификации, заданной на языке дискрипционной логики ACL, построить формальную онтологию, удовлетворяющую этой спецификации. Является ли эта онтология единственной, удовлетворяющей этой спецификации? По заданной формальной онтологии задайте полную ее спецификацию на языке дискрипционной логики ACL. Является ли заданная онтология единственной, удовлетворяющей потроенной спецификации?

Контрольные вопросы для подготовки к промежуточной аттестации:

№ п/п	Наименование раздела дисциплины	Вопросы
1.	Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений	Что такое «математическое доказательство», историческое развитие этого понятия и современное социальное содержание? Что такое «доказательство по определению/построению», «доказательство полным перебором конечного числа случаев», «доказательство от противного» и «доказательство математической индукцией»? Чем отличаются «наивная» и «формальные» теории множеств? Каковы постулаты наивной теории множеств? Как эти постулаты называются и почему? Что такое числовая система и алгебра? Что означает определить числовую систему или алгебру средствами наивной теории множеств? Как определить натуральные, целые, рациональные, вещественные и комплексные числа в раках наивной теории множеств, какие постулаты при этом используются? Как определить алгебры множеств, нечетких множеств, σ-алгебры в рамках наивной теории множеств? Что такое булева алгебра множеств, как доказать существование булевых алгебр множеств в рамках наивной теории множеств? Что такое булевская пропозициональная логика, чем булевская логика отличается от булевых алгебр и как эти понятия связаны? Что такое «разрешающая процедура» и какие разрешающие процедуры известны (из курса) для булевской логики? Что такое «аксиоматизация булевской логики», ее корректность, непротиворечивость и полнота? Какие аксиоматизации для булевской логики известны (из курса)? Что такое нечеткая пропозициональная логика? Как связана истинность в пропозициональных вариантах нечеткой и булевской логике? Что такое вероятностная пропозициональная логика? Как связана истинность в пропозициональных вариантах вероятностной и булевской логике? Какие примеры известны (из курса) применения пропозициональных булевской, нечеткой и вероятностной логики для представления данных, знаний и рассуждений?
2.	Общее понятие логической системы, разрешимости и логического вывода	Что такое синтаксис, семантика и прагматика логического языка? Что такое «формальный язык» и какие формализмы для задания формальных языков определены в курсе? Что такое иерархия множеств по степеням (power-set)? Как определяется порядок логики в зависимости от места ее семантических моделей в этой иерархии по степеням? Что такое логическая теория? Как можно определить теорию синтаксически и семантически? Что такое «аксиоматическая система гильбертовского типа»? Что такое «аксиоматическая система генценовского типа»? Что такое «доказательство» и «логический вывод» в таких системах? Как связаны доказуемости в системах этих типов? Что такое Теория неинтерпретированного равенства? Что такое арифметика Пресбургера? Что такое арифметика Пеано? Что такое стандартная и нестандартные модели арифметики? Что такое аксиоматика Тарского для поля вещественных чисел? Каков порядок этой теории? Что такое теория первого порядка поля вещественных чисел? Что означает «разрешимая теория», «аксиоматизируемая теория», «частично разрешимая теория» и «неразрешимая теория»? Как связаны эти понятия? Приведите примеры (из курса) теорий, которые «различают» различные из этих классов. Каковы основные понятия (веденные в курсе) из области (полу)автоматического доказательства теорем? Дедуктивная верификация программ как пример применения (полу)автоматического доказательства теорем. Как используются разрешающие процедуры в решении логических запросов и (полу)автоматическом доказательстве теорем? Верификация моделей (model checking) как пример использования разрешающих процедур для верификации программ, систем и решения логических запросов.
3.	Алгебраический подход к представлению баз данных и знаний	Что такое алгебра бинарных отношений? Имеет ли она каноническую модель? Разрешима ли эквициональная теория алгебры бинарных отношений? Что такое алгебра Клини? Имеет ли алгебры Клини каноническую модель? Разрешима ли эквициональная теория алгебр Клини? Как алгебры Клини связаны с алгеброй бинарных отношений? Что такое реляционная алгебра? Имеет ли реляционные алгебры каноническую модель? Разрешима ли эквициональная теория реляционных алгебр? Как алгебра бинарных отношений описывается в терминах реляционных алгебр? Что такое базис операций реляционных алгебр? Что такое нормальные формы в теории реляционных алгебр? Что такое реляционная модель и реляционные базы данных? Что такое аксиоматика Армстронга, что можно утверждать про ее корректность и полноту? Что такое частичные и линейные порядки? Что такое решетки и полные решетки? Что такое булевы алгебры? Какие пример алгебраических систем разделяют эти перечисленные классы? Что такое формальные контексты? Что такое операции содержания атрибутной спецификации и атрибутная спецификация содержания в формальном контексте? Как связаны эти операции с поиском по ключевым словам? Что такое формальное понятие в формальном контексте? Что такое решетка формальных понятий формального контекста? Что такое Основная теорема анализа формальных понятий? Как доказывается для конечного случая эта теорема? Какие еще теоремы известны с названием «основная теорема …»? Какие алгоритмы рисования графов (из курса) могут применяться для визуализации решеток формальных понятий? Что такое атрибутная импликация? Как она может быть использована в рекомендательных системах?
4.	Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений	Что такое шкалы и модели Крипке? Какая связь шкал и моделей Крипке с системами (помеченных) переходов? Почему алгебры бинарных отношений – это шкалы/модели Крипке с программируемыми бинарными отношениями? Как системы помеченных переходов и модели Крипке используются для представления времени, событий, мнений и знаний о предметных областях? Как семантически (какими шкалами Крипке) определяются классические пропозициональные модальные логики K, S4 и S5? Как аксиоматизируются классические пропозициональные модальные логики K, S4 и S5? Что такое каноническая («малая») модель для пропозициональных модальных логик K, S4 и S5? Как каноническая модель используется в доказательстве аксиоматизируемости и разрешимости этих логик? Что такое логика линейного времени LTL? Какой класс систем помеченных переходов используется для определения ее семантики? Разрешима ли и аксиоматизируема ли эта логика? Что такое логика ветвящегося времени CTL? Какой класс систем помеченных переходов используется для определения ее семантики? Разрешима ли и аксиоматизируема ли эта логика? Что такое свойство финитной аппроксимируемости («конечной модели»)? Чем это свойство отличается от свойства малой модели? Как используется в доказательстве разрешимости темпоральных логик? Чем отличается эпистемическая логика Kn от модальной логики S5? Разрешима ли, аксиоматизируема ли эта эпистемическая логика? Что такое групповое знание, распределенное знание и общее знание? Как перечисленные конструкции выражаются через знания индивидуальных агентов с использованием операций алгебры бинарных отношений и конструктора неподвижной точки? Что такое дискрипционные логики, каков их синтаксис, семантика открытого и замкнутого мира? Чем дискрипционная логика ACL отличается от полимодального варианта логики K? Что такое «формальная онтология»? Почему формальные онтологии – это представление баз знаний? Как формальная онтология специфицируется средствами дискрипционных логик? Как дискрипционные логии используются для запросов к формальным онтологиям? Что такое «табличный метод» (tablo)? Как этот метод используется (и для каких дискрипционных логик) для извлечения знаний из спецификации формальной онтологии?

Вопросы/Задания к промежуточной аттестации в устной/письменной форме:

Приведите примеры из курса Математического анализа «доказательства по определению/построению» «доказательство полным перебором конечного числа случаев», «доказательство от противного» и «доказательство математической индукцией».
Перечислите постулаты наивной теории множеств и сравните их с аксиомами теорией множеств первого порядка (например, 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), использование которого свободно допускается в учебном процесе и в демонстрационных целях.

BSc: IntroductionToComputerVision

Contents