View source for BSc: B1.V.DV.03.02 MFAI 2024 Mathematical logic for AI

<span id="математическая-логика-для-искусственного-интеллекта"></span>
= '''Математическая логика для искусственного интеллекта''' =

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

'''Направление подготовки''': 09.03.01 Информатика и вычислительная техника

'''Направленность (профиль) образовательной программы''': Математические основы искусственного интеллекта

'''Программу разработал(а)''': Николай Вячеславович Шилов, к.ф.-м.н., доцент Университета Иннополис
</blockquote>

== 1. Краткая характеристика дисциплины ==
: Изучение дисциплины обеспечивает формирование и развитие компетенций обучающихся в области математической логики, их применение для решения различных прикладных задач в рамках профессиональной деятельности. В ходе освоения дисциплины обучающиеся рассматривают начала теории и алгебр множеств и нечетких множеств, булевской, нечеткой и вероятностной пропозициональных логик, основы систем переходов и моделей Крипке, модальных, дискрипционных, темпоральных и эпистемических логик, элементы универсальной алгебры, теории решеток и анализа формальных понятий, логики первого и высших порядков, необходимых для представления знаний и онтологий предметных областей средствами дискрипционных логик и формальных понятий, реализации логического вывода и полуавтоматического доказательства теорем, вероятностного и нечеткого вывода для получения новых знаний в теориях предметных областей.

== 2. Перечень планируемых результатов обучения ==
: '''Целью освоения дисциплины''' является освоение студентами алгебрологических формализмов и теорий, необходимых для машинного представления знаний и онтологий предметных областей, методов формального машинного вывода новых знаний в теориях предметных областей.

: '''Задачами дисциплины''' являются
* изучение, детальное знакомство
** с началами теории и алгебр множеств и нечетких множеств, булевской, нечеткой и вероятностной пропозициональных логик,
** с системами (помеченных) переходов и шкалами/моделями Крипке, и пропозициональными модальными, дискрипционными, темпоральными и эпистемическими логиками, определимых на этих моделях,
** с элементами универсальной алгебры, теории решеток и анализа формальных понятий, логики первого и высших порядков;
* ознакомительное, обзорное изучение с подходами/системами
** представления знаний и формализованных онтологий предметных областей средствами дискрипционных логик и формальных понятий,
** реализации логического вывода и полуавтоматического доказательства теорем, вероятностного и нечеткого вывода для получения новых знаний в предметных областях.

=== Общая характеристика результата обучения по дисциплине ===
: '''Знания:''' сформированы систематические знания
* основ теории и алгебры множеств и нечетких множеств, пропозициональной булевской, нечеткой и вероятностной логик,
* понятий систем переходов и моделями Крипке, и пропозициональными модальными, дискрипционными, темпоральными и эпистемическими логиками, определимых на этих моделях,
* элементов теории универсальной алгебры, решеток и анализа формальных понятий, логик первого и высших порядков,
* базиса теории логических разрешающих процедур и логического вывода, разрешимых и аксиоматизируемых логических теорий, автоматизированного доказательства теорем.

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

: '''Навыки (владения):''' сформировано владение навыками работы с такими инструментами как
* булевские решатели (SAT- и SMT-решатели на примерe Z3), 
* фреймворки для создания и редактирования онтологий и баз знаний (на примере Protégé),
* автоматические (например, Prover9) и полуавтоматические (на примере Coq) доказатели теорем.

== 3. Структура и содержание дисциплины ==
{| class="wikitable" style="width:70%;"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| style="width:5%" | №<br>п/п
| style="width:30%" | Наименование раздела <br> дисциплины
| style="width:65%" | Содержание дисциплины по темам
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 1. || Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений
|
* доказательства «по определению/построению», «полным перебором конечного числа случаем», «от противного» и «математической индукцией».
* наивная теория множеств, числовые системы, алгебры множеств, нечетких множеств, σ-алгебры
* булевская пропозициональная логика, ее разрешающие процедуры и аксиоматизация, булевские решатели практика их использования
* нечеткие и вероятностные пропозициональные логики, нечеткое и вероятностно представление знаний и вывод
|- style="background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 2. || Общее понятие логической системы, разрешимости и логического вывода
|
* общее понятие логики, логик первого и высших порядков
* разрешимые теории, аксиоматизация и логический вывод, автоматизированное доказательство теорем  
* знакомство с SMT-решателями и инструментами автоматического доказательства 
|- style="background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 3. ||Алгебраический подход к представлению баз данных и знаний
|
* алгебры отношений, реляционная модель и реляционные базы данных, правила и аксиоматика Армстронга
* частичные порядки, решетки, булевы алгебры и формальные контексты, решетки формальных понятий 
* представление знаний о предметных областях в виде формальных понятий, атрибутная импликация
|- style="background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 4. || Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений
|
* алгебры бинарных отношений, системы переходов и моделями Крипке, их использование для представления времени, событий, мнений и знаний о предметных областях 
* классические пропозициональные модальные, темпоральные и эпистемические логики, их разрешимость и аксиоматезируемость
* дискрипционные логики их синтаксис, семантика, использование для представления баз знаний и языков запросов к базам знаний
|}

== 4. Методические и оценочные материалы ==
'''Задания для практических занятий:</b>'''
{| class="wikitable" style="width:70%;"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| style="width:5%" | №<br>п/п
| style="width:30%" | Наименование раздела<br>дисциплины (модуля)
| style="width:65%" | Перечень рассматриваемых тем (вопросов)
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 1. || Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений
|
# Приведите примеры доказательств «по определению/построению», «полным перебором конечного числа случаев», «от противного» и «математической индукцией».
# Докажите существование объединения, пересечения, произведения и степени множеств в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества натуральных чисел и построите натуральные числа 0, 1 и 2 в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества рациональных чисел и постройте рациональное число -1⁄2 в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества вещественных чисел и докажите существование числа √2 в наивной теории множеств.
# Для каких натуральных n существует алгебра множеств, состоящая из n множеств, замкнутая относительно пересечений, объединений и дополнений?
# Докажите непротиворечивость понятия σ-алгебры. Для каких натуральных n существует σ-алгебра, состоящая из n множеств?
# Приведите пример булевской формулы, которую легко доказать в системе нормального вывода, но трудно проверить ее невыполнимость методом DPLL.
# Приведите пример (если возможно) тождественно истинной булевской формулы, которая при каком-либо означивании ее как формулы нечеткой и/или вероятностной логики получает значение <0.5 и <1 соотвественно.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 2. || Общее понятие логической системы, разрешимости и логического вывода
|
# Приведите примеры свойств вещественных чисел, описываемых на языке первого, второго и высших порядков.
# Приведите примеры эквивалентных гильбертовской и генценовской аксиоматизаций.
# Приведите пример аксиоматизаций (первого и второго порядка) натуральных чисел.
# Приведите пример аксиоматизаций (первого и второго порядка) вещественных чисел.
# Докажите существование (поля) комплексных чисел.
# Приведите примеры разрешимых теорий натуральных, рациональных и вещественных чисел. 
# Приведите примеры неразрешимых теорий натуральных, рациональных и вещественных чисел. 
# Выполните доказательство простейших свойств в системе Z3.
# Выполните доказательство простейших свойств в системе Prover9.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 3. || Алгебраический подход к представлению баз данных и знаний
|
# В чем разница алгебры бинарных отношений и алгебры отношений (т. е. реляционной алгебры)?
# Разрешима ли алгебра бинарных отношений? Разрешима ли реляционная алгебра?
# Аксиоматизируема ли алгебра бинарных отношений? Аксиоматизируема ли реляционная алгебра?
# Приведите примеры операций реляционной алгебры, выразимых через другие операции.
# Приведите примеры частичного порядка, который не является решеткой и решетки, которая не является полной решеткой.
# Приведите пример формального контекста и постройте решетку формальных понятий для этого контекста. Перечислите все атрибутные импликации верные в этой решетке. 
# Приведите пример конечной решетки и постройте формальный контекст, решетка формальных понятий которого изоморфна данной решетке.
# Обсудите алгоритмы рисования графов для визуализации решеток формальных понятий.
# Представьте в виде формального контекста знания о предложенной предметной области (например, учебные курсы и их зависимостей), воспользуйтесь свободно распространяемыми инструментами работы с формальными контекстами (например, ToscanaJ) для анализа этого формального контекста.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 4. || Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений
|
# Для программы с конечным числом состояний постройте соответствующую ей систему переходов и ее дерево вычислений. 
# Для заданной формулы пропозициональной модальной логики (например K) постройте ее каноническую модель.
# Приведите примеры разрешимых пропозициональных модальных, временных логик и программных логик.
# Приведите примеры неразрешимых пропозициональных модальных, временных логик или программных логик.
# Приведите примеры аксиоматизаций пропозициональных модальных, временных, эпистемических логик. Для заданной эпистемичекой головоломки постройте ее аксиоматизацию на языке пропозициональной эпистемической логики.
# Для заданной эпистемической головоломке постройте модель Крипке и логический запрос (на языке пропозициональной модальной, временной и/или эпистемической логики), решающего в этой модели данную головоломку. Какую решающую процедуру для этого надо применить?
# Постройте и обоснуйте корректность алгоритма «перевода» дискриционнй логики ALC в логику первого порядка с одной свободной переменной.
# Приведите примеры предметных областей, удовлетворяющих гипотезе о закрытом мире. Приведи примеры предметных областей, неудовлетворяющих гипотезе зарытого мира, объясните, почему мир этих предметных областей существенно открытый.
# Представьте в виде формальной онтологии знания о предложенной предметной области (например, учебные курсы и их зависимостей), воспользуйтесь системой Protégé для анализа этого формального контекста.
|}

'''Текущий контроль успеваемости обучающихся по дисциплине:'''
{| class="wikitable" style="width:70%;"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| style="width:5%" | №<br>п/п
| style="width:20%" | Наименование раздела дисциплины
| style="width:20%" | Форма текущего контроля
| style="width:55%" | Материалы текущего контроля
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 1.
| Наивная теория множеств, пропозициональные логики для представления знаний и рассуждений
| Письменная домашняя контрольная работа с устным опросом в классе
| 
# Разберите какие методы доказательства использованы в приведенном в курсе доказательстве иррациональности числа √2.
# Докажите существование картежей (упорядоченных наборов любой заданной фиксированной длины) в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества целых чисел и построите целые числа 0, +1 и -2 в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества отрицательных рациональных чисел и постройте рациональное число -2 в наивной теории множеств.
# Докажите (в наивной теории множеств) существование множества иррациональных чисел и докажите принадлежность числа √2 этому множеству.
# Постройте алгебру множеств, состоящая из 2^3 множеств, замкнутую относительно пересечений, объединений и дополнений.
# Приведите пример σ-алгебры из 2^4 конечных множеств, которая не является алгеброй всех подмножеств некоторого конечного множества.
# Приведите пример булевской формулы, которую экспоненциально трудно доказать в системе нормального вывода, но легко проверить ее невыполнимость методом DPLL.
# Приведите пример (если возможно) тождественно ложной булевской формулы, которая при каком-либо означивании ее как формулы нечеткой и/или вероятностной логики получает значение >0.5 и >0 соотвественно.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 2.
| Общее понятие логической системы, разрешимости и логического вывода
| Письменная домашняя контрольная работа с устным опросом в классе
| 
# Можно ли записать на языке первого порядка в сигнатуре поля для заданного натурального n утверждение, что любое уравнение степени не более n имеет корень? 
# Докажите заданную истинную формулу пропозициональной булевской логики в гильбертовом исчислении, определенном в курсе лекций для пропозициональной булевской логики.
# Докажите заданную истинную формулу пропозициональной булевской логики в генценовском исчислении, определенном в курсе лекций для пропозициональной булевской логики.
# Выполните доказательство заданной истинной эквациональной формулы первого порядка в теории не интерпретированного равенства.
# Докажите коммутативность умножения в аксиоматике Пеано.
# Докажите, что существование бесконечно малых чисел противоречит аксиоматизации Тарского поля вещественных чисел.
# Можно ли записать на языке первого порядка в теории поля вещественных чисел утверждение, что любое алгебраическое уравнение степени имеет корень? 
# Докажите разрешимость арифметики Пресбургера натуральных чисел, обогащенных унарными операциями умножения на целые константы.
# Приведите пример (с объяснением) утверждения, которое записывается на языке арифметики Пеано, но ни оно само, ни его отрицание недоказуемы в этой аксиоматической теории.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 3.
| Алгебраический подход к представлению баз данных и знаний
| Письменная домашняя контрольная работа с устным опросом в классе
| 
# Для данных равенств, записанных на языке алгебры бинарных отношений, доказать, какие из них являются тождествами, а какие не являются.
# Для данных равенств, записанных на языке реляционных алгебр, доказать, какие из них являются тождествами, а какие не являются.
# Доказать, что алгебра бинарных отношений является алгеброй Клини.
# Приведите пример минимального базиса операций реляционных алгебр, докажите минимальность этого базиса
# Существует ли полная решетка, которая не является булевой алгеброй? (Докажите свой ответ.)
# По заданному формальному контексту постройте решетку его формальных понятий, перечислите все атрибутные импликации верные в этой решетке (с обоснованием полноты перечисления). 
# По заданной конечной решетке постройте формальный контекст, решетка формальных понятий которого изоморфна данной решетке.
# По заданной информации о родственных связях внутри (игрушечной) семьи, построите формальный контекст, решетку формальных понятий и перечислите все атрибутные импликации, которые имеют место (с обоснованием полноты перечисления).
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 4.
| Логически с семантикой, основанной на системах (помеченных) переходов и шкалами/моделями Крипке, их применение для представления знаний, мнений и рассуждений
| Письменная домашняя контрольная работа с устным опросом в классе
| 
# Для заданной программы постройте ее булевозначную модель, соответствующую этой модели систему переходов и ее дерево вычислений. 
# Для заданной формулы пропозициональной модальной логики (например S5) постройте ее каноническую модель.
# Для заданной формулы пропозициональной модальной, темпоральной или программной логики, обладающей свойством конечной модели, выполните алгоритм проверки выполнимости этой формулы с использованием свойства конечной модели.
# Для заданной формулы пропозициональной модальной, темпоральной или программной логики, имеющей табличную разрешающую процедуру, выполните алгоритм проверки выполнимости этой формулы с использованием этой процедуры.
# Для заданной эпистемической головоломке постройте модель Крипке и логический запрос (на языке пропозициональной модальной, временной и/или эпистемической логики), решающего в этой модели данную головоломку. Какую решающую процедуру для этого надо применить?
# По заданной информации о родственных связях внутри (игрушечной) семьи, и по описанию/определению родственных связей в терминах ролей «родитель-ребенок», «супруг-супруг», построите формальную онтологию этой семьи, задав минимальное количество аксиом.
# По спецификации, заданной на языке дискрипционной логики ACL, построить формальную онтологию, удовлетворяющую этой спецификации. Является ли эта онтология единственной, удовлетворяющей этой спецификации?
# По заданной формальной онтологии задайте полную ее спецификацию на языке дискрипционной логики ACL. Является ли заданная онтология единственной, удовлетворяющей потроенной спецификации?
|}

'''Контрольные вопросы для подготовки к промежуточной аттестации:'''
{| class="wikitable" style="width:70%;"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| style="width:5%" | №<br>п/п
| style="width:25%" | Наименование <br> раздела дисциплины
| style="width:70%" | Вопросы
|-  style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 1.
| Методы математических доказательств, наивная теория множеств, пропозициональные логики для представления знаний и рассуждений
|
# Что такое «математическое доказательство», историческое развитие этого понятия и современное социальное содержание?
# Что такое «доказательство по определению/построению», «доказательство полным перебором конечного числа случаев», «доказательство от противного» и «доказательство математической индукцией»?
# Чем отличаются «наивная» и «формальные» теории множеств? Каковы постулаты наивной теории множеств? Как эти постулаты называются и почему?
# Что такое числовая система и алгебра? Что означает определить числовую систему или алгебру средствами наивной теории множеств? 
# Как определить натуральные, целые, рациональные, вещественные и комплексные числа в раках наивной теории множеств, какие постулаты при этом используются?
# Как определить алгебры множеств, нечетких множеств, σ-алгебры в рамках наивной теории множеств?
# Что такое булева алгебра множеств, как доказать существование булевых алгебр множеств в рамках наивной теории множеств?
# Что такое булевская пропозициональная логика, чем булевская логика отличается от булевых алгебр и как эти понятия связаны? 
# Что такое «разрешающая процедура» и какие разрешающие процедуры известны (из курса) для булевской логики?
# Что такое «аксиоматизация булевской логики», ее корректность, непротиворечивость и полнота? Какие аксиоматизации для булевской логики известны (из курса)?
# Что такое нечеткая пропозициональная логика? Как связана истинность в пропозициональных вариантах нечеткой и булевской логике? 
# Что такое вероятностная пропозициональная логика? Как связана истинность в пропозициональных вариантах вероятностной и булевской логике?  
# Какие примеры известны (из курса) применения пропозициональных булевской, нечеткой и вероятностной логики для представления данных, знаний и рассуждений?
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 2.
| Общее понятие логической системы, разрешимости и логического вывода
|
# Что такое синтаксис, семантика и прагматика логического языка?
# Что такое «формальный язык» и какие формализмы для задания формальных языков определены в курсе?
# Что такое иерархия множеств по степеням (power-set)? 
# Как определяется порядок логики в зависимости от места ее семантических моделей в этой иерархии по степеням?
# Что такое логическая теория? Как можно определить теорию синтаксически и семантически?
# Что такое «аксиоматическая система гильбертовского типа»? Что такое «аксиоматическая система генценовского типа»? Что такое «доказательство» и «логический вывод» в таких системах? Как связаны доказуемости в системах этих типов?
# Что такое Теория неинтерпретированного равенства?
# Что такое арифметика Пресбургера?
# Что такое арифметика Пеано?
# Что такое стандартная и нестандартные модели арифметики?
# Что такое аксиоматика Тарского для поля вещественных чисел? Каков порядок этой теории?
# Что такое теория первого порядка поля вещественных чисел?
# Что означает «разрешимая теория», «аксиоматизируемая теория», «частично разрешимая теория» и «неразрешимая теория»? Как связаны эти понятия? Приведите примеры (из курса) теорий, которые «различают» различные из этих классов. 
# Каковы основные понятия (веденные в курсе) из области (полу)автоматического доказательства теорем? Дедуктивная верификация программ как пример применения (полу)автоматического доказательства теорем.
# Как используются разрешающие процедуры в решении логических запросов и (полу)автоматическом доказательстве теорем? Верификация моделей (model checking) как пример использования разрешающих процедур для верификации программ, систем и решения логических запросов.
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 3.
| Алгебраический подход к представлению баз данных и знаний
|
# Что такое алгебра бинарных отношений? Имеет ли она каноническую модель? Разрешима ли эквициональная теория алгебры бинарных отношений?
# Что такое алгебра Клини? Имеет ли алгебры Клини каноническую модель? Разрешима ли эквициональная теория алгебр Клини? Как алгебры Клини связаны с алгеброй бинарных отношений? 
# Что такое реляционная алгебра? Имеет ли реляционные алгебры каноническую модель? Разрешима ли эквициональная теория реляционных алгебр? Как алгебра бинарных отношений описывается в терминах реляционных алгебр?
# Что такое базис операций реляционных алгебр? Что такое нормальные формы в теории реляционных алгебр? 
# Что такое реляционная модель и реляционные базы данных? 
# Что такое аксиоматика Армстронга, что можно утверждать про ее корректность и полноту?
# Что такое частичные и линейные порядки? Что такое решетки и полные решетки? Что такое булевы алгебры? Какие пример алгебраических систем разделяют эти перечисленные классы? 
# Что такое формальные контексты? Что такое операции содержания атрибутной спецификации и атрибутная спецификация содержания в формальном контексте? Как связаны эти операции с поиском по ключевым словам?
# Что такое формальное понятие в формальном контексте? Что такое решетка формальных понятий формального контекста? 
# Что такое Основная теорема анализа формальных понятий? Как доказывается для конечного случая эта теорема? Какие еще теоремы известны с названием «основная теорема …»?
# Какие алгоритмы рисования графов (из курса) могут применяться для визуализации решеток формальных понятий?
# Что такое атрибутная импликация? Как она может быть использована в рекомендательных системах?
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| style="text-align:center;" | 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.

=== Методические указания для обучающихся по освоению дисциплины ===
{| class="wikitable" style="width:80%;"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| style="width:20%" | Вид учебных<br>занятий/деятельности
| style="width:80%" | Деятельность обучающегося
|- 
| style="vertical-align:middle; text-align:center;" | Лекция
| style="vertical-align:middle; text-align:left;" | Написание конспекта лекций: кратко, схематично, последовательно фиксировать основные положения лекции, выводы, формулировки, обобщения; помечать важные мысли, выделять ключевые слова, термины. Обозначить вопросы, термины или другой материал, который вызывает трудности, пометить и попытаться найти ответ в рекомендуемой литературе. Если самостоятельно не удается разобраться в материале, необходимо сформулировать вопрос и задать преподавателю на консультации, во время семинарского (практического) занятия.
|-
| style="vertical-align:middle; text-align:center;" | Практическое (семинарское) занятие
| style="vertical-align:middle; text-align:left;" | При подготовке к семинарскому (практическому) занятию необходимо проработать материалы лекций, основной и дополнительной литературы по заданной теме. На основании обработанной информации постараться сформировать собственное мнение по выносимой на обсуждение тематике. Обосновать его аргументами, сформировать список источников, подкрепляющих его.<br>Во время семинарского (практического) занятия активно участвовать в обсуждении вопросов, высказывать аргументированную точку зрения на проблемные вопросы. Приводить примеры из источниковой базы и научной и/или исследовательской литературы.
|-
| style="vertical-align:middle; text-align:center;" | Устный/письменный опрос
| style="vertical-align:middle; text-align:left;" | Отвечать, максимально полно, логично и структурировано, на поставленный вопрос. Основная цель – показать всю глубину знаний по конкретной теме или ее части. 
|-
| style="vertical-align:middle; text-align:center;" | Подготовка к промежуточной аттестации
| style="vertical-align:middle; text-align:left;" | При подготовке к промежуточной аттестации необходимо проработать вопросы по темам, которые рекомендуются для самостоятельной подготовки. При возникновении затруднений с ответами следует ориентироваться на конспекты лекций, семинаров, рекомендуемую литературу, материалы электронных и информационных справочных ресурсов, статей.<br>Если тема вызывает затруднение, четко сформулировать проблемный вопрос и задать его преподавателю.
|-
| style="vertical-align:middle; text-align:center;" | Практические (лабораторные) занятия
| style="vertical-align:middle; text-align:left;" | Практические занятия предназначены прежде всего для разбора отдельных сложных положений, тренировки аналитических навыков, а также для развития коммуникационных навыков. Поэтому на практических занятиях необходимо участвовать в тех формах обсуждения материала, которые предлагает преподаватель: отвечать на вопросы преподавателя, дополнять ответы других студентов, приводить примеры, задавать вопросы другим выступающим, обсуждать вопросы и выполнять задания в группах. Работа на практических занятиях подразумевает домашнюю подготовку и активную умственную работу на самом занятии. Работа на практических занятиях в форме устного опроса заключается прежде всего в тренировке навыков применять теоретические положения к самому разнообразному материалу. В ходе практических занятий студенты работают в группах для обсуждения предлагаемых вопросов. 
|-
| style="vertical-align:middle; text-align:center;" | Самостоятельная работа
| style="vertical-align:middle; text-align:left;" | Самостоятельная работа состоит из следующих частей: 1) чтение учебной, справочной, научной литературы; 2) повторение материала лекций; 3) составление планов устных выступлений; 4) подготовка видеопрезентации. При чтении учебной литературы нужно разграничивать для себя материал на отдельные проблемы, концепции, идеи. Учебную литературу можно найти в электронных библиотечных системах, на которые подписан АНО Университет Иннополис. 
|-
| style="vertical-align:middle; text-align:center;" | Контрольная работа
| style="vertical-align:middle; text-align:left;" | При подготовке к контрольной работе необходимо проработать материалы лекций, семинаров, основной и дополнительной литературы по заданной теме.
|-
| style="vertical-align:middle; text-align:center;" | Индивидуальная работа
| style="vertical-align:middle; text-align:left;" | При выполнение индивидуальной работы необходимо взять задание у преподавателя, ознакомиться с требованиями к выполнению работы, изучить поставленную проблему, найти решение проблемы. Если самостоятельно не удается разобраться в материале, необходимо сформулировать вопрос и задать преподавателю на консультации, во время семинарского (практического) занятия. Оформить результаты работы.
|}

=== Методы и технологии обучения, способствующие формированию компетенции ===
{| class="wikitable"
|- style="vertical-align:middle; text-align:center; background-color:#EAECF0; color:#202122; font-weight:bold;"
| Методы и технологии обучения, способствующие формированию компетенции
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| Традиционные технологии (классно-урочная система)
|- style="vertical-align:middle; background-color:#F8F9FA; color:#202122;"
| Программного обеспечения Prover9, Protégé (2-пунктная лицензия BSD) и Z3 (MIT License), использование которого свободно допускается в учебном процесе и в демонстрационных целях.
|}