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

Направления исследований

Научные направления

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

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

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

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

Математическая лингвистика и теория формальных языков (М. Р. Пентус, С. Л. Кузнецов, А. А. Сорокин)

Теория формальных языков возникла в 1950-х гг. как одно из направлений математической лингвистики, предназначенное для строгого описания синтаксиса как естественных языков, так и языков программирования. В настоящее время она представляет собой раздел математической логики, изучающий свойства формальных языков, способы их описания (контекстно-свободные грамматики, категориальные грамматики, расширения конечных автоматов и т. д.), алгоритмы распознавания принадлежности формальному языку и другие связанные вопросы. На кафедре математической логики и теории алгоритмов в основном исследуются математические свойства исчислений, применяемых в категориальных грамматиках. Для этого используются методы теории доказательств, теории алгоритмов и алгебры.

Более подробное представление о тематике научной работы можно получить на страницах профессора М. Р. Пентуса, к.ф.-м.н. С. Л. Кузнецова и к.ф.-м.н. А. А. Сорокина.

Под математической (или вычислительной) лингвистикой в настоящее время понимают совокупность математических методов, применяемых в лингвистических задачах. Данное направление бурно развивается начиная с 90-х гг. в связи с наличием большого числа приложений (информационный поиск, автоматическая текстовая классификация и обработка текста, машинный перевод, корпусная лингвистика, формальная семантика и т. д.) Среди прочих дисциплин, математический аппарат вычислительной лингвистики включает в себя теорию формальных языков, теорию конечных автоматов и преобразователей и категориальные грамматики, которые активно изучаются на кафедре математической логики и теории алгоритмов.

Сложность вычислений (Н. К. Верещагин, В. Н. Крупский, А. Шень)

Существование компьютерной программы вычисления функции f(x) ещё не означает возможности её вычисления на практике. Например, алгоритм распознавания простоты натурального числа x, имеющего n десятичных знаков, с помощью решета Эратосфена требует перебора 10n/2 возможных делителей x. Предположим, что этот алгоритм выполняется на компьютере с тактовой частотой 1015 Гц (частота атомных переходов). Тогда для проверки простоты 46-значного числа потребуется не меньше 108 секунд, что примерно равно трём годам!

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

Колмогоровская сложность (сложность описаний) (Н. К. Верещагин, В. Н. Крупский, А. Шень)

Колмогоровскую сложность слова в данном алфавите можно определить как длину в битах кратчайшей программы, печатающей это слово. Интуитивно, сложность x равна количеству информации в x. Например, сложность достаточно длинной последовательности из одних нулей примерно равна сложности двоичной записи её длины. А сложность «случайной» последовательности примерно равна её длине. Последнюю фразу можно принять за определение случайной последовательности и на этом основании строить теорию вероятностей как науку о свойствах случайных последовательностей. Например, закон больших чисел будет сформулирован так: в любой случайной последовательности доля единиц примерно равна 1/2. (В обычной формулировке закон больших чисел говорит, что в большинстве последовательностей доля единиц примерно равна 1/2.) На том же основании можно построить и математическую статистику.

Колмогоровская сложность применяется также в теории сложности вычислений для доказательства того, что для данной функции нет быстрого алгоритма её вычисления.

Компьютерная логика (С. Н. Артёмов, В. Н. Крупский, М. Р. Пентус)

Из двух направлений в математической логике — классического (Фреге, Гильберт, Гёдель, Тарский) и интуиционистского (Брауэр, Колмогоров, Карри, Чёрч) — последнее оказывает наибольшее влияние на области науки, лежащие вне пределов традиционной логики. Интуиционистская логика и функциональные исчисления были открыты в первой трети 20-го века как средства изучения оснований математики и впоследствии оказались мостом, соединяющим доказательства и вычислительные программы. К настоящему времени можно говорить о новом научном направлении «Компьютерная логика», выросшем на интуиционистской традиции в математической логике и ставшем неотъемлемой частью как математической логики, так и Computer Science.

Кафедра и лаборатория логических проблем информатики сотрудничают с такими центрами, как Cornell, Caltech, Stanford, UPenn, Graduate Center CUNY (США), IML — Marseille (Франция), University of Berne и IvyTeam (Швейцария), University of London, University of Amsterdam, Utrecht University и др.

Теория доказательств (С. Н. Артёмов, Л. Д. Беклемишев, В. Н. Крупский, Т. Л. Яворская)

Теория доказательств является ядром математической логики. Именно в этой области была доказана самая знаменитая математическая теорема 20-го века — теорема Гёделя о неполноте формальных систем. Согласно теореме Гёделя, никакая достаточно богатая непротиворечивая логико-математическая система (например, формальная арифметика) не в состоянии установить свою собственную непротиворечивость. Этот результат перевернул господствующие в начале прошлого века представления о математике, а также оказал решающее воздействие на наши воззрения о процессе познания вообще. Трудно также переоценить влияние теоремы Гёделя и связанных с ней результатов на теорию и практику таких дисциплин, как Computer Science и Artificial Intelligence. Группа по теории доказательств на кафедре является одной из лучших в мире.

Конструктивная логика (С. Н. Артёмов, В. Е. Плиско, Т. Л. Яворская)

Конструктивная логика возникла в работах Брауэра, Гейтинга, Колмогорова, Карри, Чёрча, Маркова как описание конструктивных методов в математике и логике. В основе брауэровского подхода к конструктивной (интуиционистской) логике лежит систематическое использование понятия доказуемости как конструктивного метода установления истинности логико-математических утверждений. Например, в рамках этого подхода классический логический принцип исключённого третьего «A или не A» становится неверным, так как его конструктивное прочтение утверждает наличие общего метода доказательства A или установления того, что A не доказуемо. Фундаментальные теоремы Гёделя и Тьюринга показывают, что такого общего метода не существует. Конструктивная логика имеет многочисленные приложения и продолжает активно развиваться под их влиянием. Группа по конструктивной логике на кафедре поддерживает традиции А. Н. Колмогорова, П. С. Новикова и А. А. Маркова и занимает одну из ведущих позиций в мире.

Модели и алгоритмы в биоинформатике (В. А. Любецкий)

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

Математическая сторона этой работы основана на решении трудных задач информатики (computer science), которые можно решать, не касаясь самих приложений.

Примеры таких задач.

  1. Даны n натуральных чисел. Можно ли разбить их множество на две части с одинаковыми суммами чисел из каждой части?
  2. Даны два графа a и b и список естественных операций над графами. Какова кратчайшая последовательность этих операций, преобразующая a в b?
  3. Как определить/вычислить расстояние между графами?
  4. Что такое средний граф для данного набора графов?
  5. Описать смену режимов в функционировании динамических систем определённых типов (важных в биологии).

Во всех случаях нужно найти низкой степени полиномиальный (практически — линейный) вычислительный алгоритм, который решает задачу.

Важную роль в исследовании играют программирование для суперкомпьютеров (распределённых вычислительных систем) и создание/использование больших данных.

Теория множеств и теория моделей (В. А. Любецкий)

Исследование направлено на изучение (1) случайных точек/чисел и (2) абсолютно неразрешимых проблем. Случайная точка (в частности, число) определяется как такая, которая не может быть локализована в пространстве с помощью простого описания (например, «прибором»). Абсолютная неразрешимость означает, что проблему нельзя решить в рамках теории, которая вмещает все рассуждения, — общей теории множеств; при этом не предполагаются ограничения на метод решения (например, не требуется алгоритмичности и т. п.). Такие проблемы встречаются среди очень простых вопросов об измеримости и топологии простых множеств вещественных чисел. Также большую важность имеет изучение взаимоотношений этих проблем между собой.

Родственное исследование ведётся вокруг теоремы Морли, которая говорит, что в определённом смысле все несчётные мощности равноценны. А также вокруг модельно полных аксиоматик, которые подобны аксиомам вещественных и комплексных чисел. Оказывается, что хорошо известные из школы свойства этих чисел и их взаимоотношений воспроизводятся на совершенно непохожих на числа парах колец.

Некоторые спецсеминары

Просеминар по математической логике для студентов первого и второго курсов

Руководят семинаром Л. Д. Беклемишев, С. Л. Кузнецов, А. А. Оноприенко и А. Л. Семёнов. Просеминар работает по пятницам с 16:45 до 18:20.

Спектр занятий широк: математическая логика, теория алгоритмов, сложность вычислений, теория игр, конструирование и анализ алгоритмов, криптография, теория автоматов. Обычно на каждый семестр выбирается новая тема или даже несколько тем. Единственное ограничение в их выборе состоит в том, что тема должна быть интересна руководителям семинара (и, мы надеемся, остальным участникам) и чтобы имелось достаточно много задач, доступных первокурсникам и второкурсникам. Просеминар имеет свой сайт (старая версия сайта доступна по ссылке).

Колмогоровский семинар

Руководят семинаром Н. К. Верещагин, А. Л. Семёнов, А. Е. Ромащенко и А. Х. Шень. Семинар работает по понедельникам с 16:20 до 17:55. Колмогоровский семинар имеет свой сайт (старая версия сайта доступна по ссылке).

Это научный семинар. На каждом занятии один из участников или гостей семинара делает доклад, в котором рассказывает о своих результатах или об изученных новых научных статьях, интересных остальным участникам. В докладах даются определения используемых понятий, формулировки доказанных теорем и объясняется их смысл и чем они интересны. Затем обычно излагаются доказательства и формулируются открытые вопросы. Довольно часто ответы на такие вопросы находятся потом участниками семинара, решения докладываются и т. д. Таким образом, семинар является важным двигателем научного исследования.

Основных тем семинара две: сложность вычислений, изучающая количество основных ресурсов (времени и памяти), необходимых для выполнения некоторого вычисления, и сложность описаний (колмогоровская сложность) — наука об информации в конечных объектах и об информационных законах. Познакомиться с этими областями можно по следующим источникам:

Образовательный семинар по математической логике

Руководят семинаром Н. К. Верещагин, Д. В. Мусатов и А. Ю. Румянцев.

Рассчитан на студентов 3—5-го курсов. Цель семинара — познакомить студентов с классическими результатами математической логики, такими как теорема Гёделя о полноте, теоремы Гёделя о неполноте (первая и вторая), разрешимость элементарной теории действительных чисел.

Некоторые спецкурсы

Колмогоровская сложность и теория информации

Спецкурс читает Н. К. Верещагин или А. Х. Шень.

Колмогоровскую сложность слова в данном алфавите можно определить как длину кратчайшей программы, печатающей слово. Цель спецкурса — изложение основ теории колмогоровской сложности и её многочисленных применений (к обоснованию теории вероятностей, к получению оценок времени работы алгоритмов и т. д.).

Подробную программу и конспекты лекций можно посмотреть на веб-странице Н.К.Верещагина.

Сложность вычислений

Спецкурс читает Н. К. Верещагин, В. Н. Крупский или А. Х. Шень.

В курсе излагаются основные результаты теории сложности вычислений — одной из центральных областей теоретической информатики. Подробную программу и конспекты лекций можно посмотреть на веб-странице Н.К.Верещагина.

Теоретико-сложностные проблемы в криптографии

Спецкурс читает Н. К. Верещагин.

В курсе излагаются основные применения теории сложности вычислений в криптографии. Главным из таких применений является возможность дать точные определения надёжности криптографических протоколов и схем и в ряде случаев доказательство их надёжности.

Подробную информацию можно найти на веб-странице Н.К.Верещагина.

Теория формальных языков

Спецкурс читает М. Р. Пентус. Курс рассчитан на студентов 1—6-го курсов.

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

Исчисление Ламбека

Спецкурс читает М. Р. Пентус.

Программа спецкурса: синтаксическое исчисление Ламбека и грамматики Ламбека, устранимость сечения в секвенциальном исчислении Ламбека и её следствия, открытые проблемы, относящиеся к фрагментам и вариантам исчисления Ламбека, языковые и реляционные модели, некоммутативная линейная логика.

На сайте выложен конспект спецкурса 2005/2006 года.