Кафедра математической логики и теории алгоритмов

Механико-математического факультета МГУ


Дескрипционная логика (годовой спецкурс, 2017—2018)

с.н.с. Е.Е.Золин

Краткое содержание лекций

Весна 2018

  1. 2018.02.16: Обзор логик от ALC до SHOIQ: синтаксис, семантика. Сложность логик от ALC до ALCOIQ (проблем выполнимости концептов и совместности терминологий).
  2. 2018.03.02: Неразрешимая проблема домино. / Два определения системы домино (плитки с отношениями смежности; плитки с цветными сторонами), их эквивалентность. Проблема замощения N×N и Z×Z, их эквивалентность (два доказательства: через компактность логики высказываний, через выбор подпоследовательностей в последовательности сдвинутых замощений). Теорема о неразрешимости.
  3. 2018.03.16: Неразрешимость логики ALC+S+H+Q. / Общее определение алгоритмической проблемы, разрешимой проблемы, алгоритмической сводимости одной проблемы к другой, сохранение свойства (не)разрешимости проблемы при наличии сводимости. Сведение проблемы домино к проблеме выполнимости концептов относительно онтологий (TBox+RBox) логики ALC+S+H+Q: аксиомы RBox и TBox (фиксированные, т.е. не зависящие от системы домино), гарантирующие существование в модели сетки N×N; аксиомы TBox, описывающие замощаемость сетки N×N данной системой домино.
  4. 2018.03.23: Логики от SH до SHOIQ. / Устранимость TBox-ов (по-английски: TBox internalization).
  5. 2018.03.30: Модульное доказательство неразрешимости (проблемы совместности онтологий) логики ALC+S+H+Q. / Лемма 1. Существует онтология данной логики, «выражающая» модель, подобную N×N; Лемма 2. Всякое расширение логики ALC, в которой данная модель выражается, имеет неразрешимую проблему совместности онтологий.
  6. 2018.04.06: 1) Разрешимость логики SHOIQ. / Понятие «роли, транзитивной в данном RBox-е» (в языке без обратных ролей), понятие простой роли. Изменения этих определений, необходимые в случае языка с обратными ролями. Синтаксис логик SHOQSHIOQ. Теорема об их разрешимости и вычислительной сложности (без доказательства) проблемы совместности базы знаний.2) Базы знаний и базы данных: сходство и различие. / База знаний как набор таблиц для n-местных отношений, сравнение с ABox. Предположение об открытости мира (в DL), предположение о замкнутости мира (в БД). Пример ABox-а с неполной информацией о некотором индивиде и необходимость разбора случаев (для нахождения ответа на запрос).
  7. 2018.04.13: Запросы к базам знаний. / Конъюнктивный запрос, его размерность, булев запрос. Ответ на запрос — случай запроса со свободными переменными и булева запроса. Пример базы знаний, различных запросов, ответов на них.Включение (или вложение, импликация) запросов относительно TBox — два определения: 1) как логическое следование импликации между запросами из данного TBox; 2) как всегда (в любом ABox-е) включение ответов на первый запрос в ответы на второй запрос. Доказательство их эквивалентности. Вспомогательное понятие: канонический ABox данного конъюнктивного запроса.
  8. 2018.04.20: Алгоритмические проблемы для запросов. / Query answering, Boolean query entailment, query containment. Сводимости между ними. Устранение из запросов: а) констант; б) составных концептов (остаются лишь x:A); в) конъюнктов вида x:A (остаются лишь xRy).Вероятно: обзор сложности проблемы query answering для различных дескрипционных логик.

    Видео по теме: Decidability of conjunctive queries for description logics with counting, inverses and nominals — лекция Sebastian Rudolph (from TU Dresden), Коллоквиум ФКН ВШЭ, 15.03.2016.

  9. 2018.04.27: Логики с операциями над ролями. // Выразимость одних операций через другие. Отсутствие FMP у логики ALCIQ(*). Устранимость TBox-ов в логике ALCIQ(U,*).
  10. 2018.05.04: Неразрешимость некоторых логик с операциями над ролями (с терминологиями или без них).
  11. 2018.05.11: Вычислительная сложность логики ALC. // Напоминание определений: PSpace, PSpace-трудность, PSpace-полнота проблемы. Лемма об экспоненциальных моделях для логики ALC.
  12. 2018.05.18: PSpace-трудность логики ALC. // Булевы формулы с кванторами (БФК). PSpace-трудность множества истинных БФК. Сведение проблемы распознавания истинности БФК к проблеме распознавания выполнимости концептов логики ALC.