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

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


Модальная логика (В. Б. Шехтман, Л. Д. Беклемишев, В. Н. Крупский, Т. Л. Яворская, Е. Е. Золин)

В естественном языке имеется большое число логических связок, которые не сводятся к стандартным «и», «или», «не», например: «возможно», «обязательно», «всегда», «здесь», «завтра». Связки такого рода называются модальностями. Изучение модальностей, начатое ещё Аристотелем, до начала XX века оставалось предметом философии и филологии. К середине века модальная логика стала разделом математической логики. С конца 1970-х гг. эта область начала стремительно развиваться: с одной стороны, здесь появились глубокие математические результаты, а с другой — в информатике, в лингвистике и в других разделах математической логики возникли многочисленные приложения модальных логик.

На нашей кафедре исследования по модальной логике активно ведутся в течение последних 25 лет. Развиваются следующие направления.

  • Общая теория модальных логик — доказательство теорем о полноте, разрешимости и других общих свойствах модальных логик. Здесь исследуются вопросы: как аксиоматизировать все модальные законы интересующей нас модели или класса моделей; какие классы моделей определимы в том или ином модальном языке; разрешима ли та или иная модальная логика и какова ее вычислительная сложность. (В. Б. Шехтман, Е. Е. Золин)
  • Модальная логика и теория доказательств — приложение модальной логики к исследованию аксиоматических теорий и автоматическому построению доказательств. Это направление было инициировано Гёделем, который заметил, что доказуемость можно рассматривать как модальность. Фундаментальная проблема: описать все принципы, которым подчиняется модальность «доказуемо» для выбранной теории. Теорема Соловея отвечает этот вопрос для формальной арифметики; теорема Беклемишева классифицирует всевозможные логики, описывающие принципы доказуемости в одной арифметической теории с точки зрения другой арифметической теории. (С. Н. Артёмов, Л. Д. Беклемишев, В. Н. Крупский, Т. Л. Яворская)
  • Временная логика — раздел модальной логики, изучающий временные модальности: «будет», «было», «сейчас», «всегда» и т.п. Этот раздел связан с лингвистикой и информатикой; одним из приложений является верификация (проверка правильности) программ. (В. Б. Шехтман)
  • Пространственная логика — раздел модальной логики, изучающий топологических и пространственных модальностей. Этот раздел начал активно развиваться после публикации работ Тарского и Маккинси, где была выявлена аналогия между операцией замыкания в топологии и модальностью «возможно». В последние годы пространственные логики стали применяться в работах по искусственному интеллекту. (В. Б. Шехтман)
  • Дескрипционная логика — возникла при разработке языков для представления знаний (в том числе, для Semantic Web), но является родственной модальной логике как по языку, так и по методам исследования. Изучаются языки, с одной стороны, достаточно богатые для записи знаний какой-либо предметной области (медицина, биоинформатика, semantic web), а с другой стороны, являющиеся разрешимыми, то есть для которых существует алгоритм (компьютерная программа), позволяющая из записанных на этом языке знаний извлекать новые знания. (Е. Е. Золин)