Студентам младших курсов
о кафедре математической логики
и теории алгоритмов

Материалы к курсу "Введение в математическую логику" (весенний семестр 2011 года) находятся на отдельной странице.

На отдельной странице приведено расписание спецкурсов и спецсеминаров.

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

Модальная логика

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

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

Математическая лингвистика

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

Центральное место в математической лингвистике занимает теория формальных грамматик. Формальная грамматика — это алгоритм, позволяющий перечислить множество всех "правильных текстов" некоторого языка. Основные типы формальных грамматик — порождающие грамматики (иерархия Хомского), категориальные грамматики (основанные на логико-алгебраических исчислениях) и трансформационные грамматики.

На кафедре математической логики и теории алгоритмов исследуются математические свойства исчислений, применяемых в категориальных грамматиках. Для этого используются методы теории доказательств, теории алгоритмов и алгебры. Некоторые возможные темы курсовых работ приведены на странице профессора М. Р. Пентуса.

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

Существование компьютерной программы вычисления функции 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 не доказуемо. Фундаментальные теоремы Гёделя и Тьюринга показывают, что такого общего метода не существует. Конструктивная логика имеет многочисленные приложения и продолжает активно развиваться под их влиянием. Группа по конструктивной логике на кафедре поддерживает традиции А. Н. Колмогорова, П. С. Новикова и А. А. Маркова и занимает одну из ведущих позиций в мире.

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

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

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

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

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

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

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

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

Можно также прослушать спецкурсы по этим дисциплинам, читаемые руководителями семинара: "Колмогоровская сложность и теория информации", "Сложность вычислений". Второй спецкурс читается иногда в Московском центре непрерывного математического образования (МЦНМО), расположенном по адресу Б. Власьевский пер., 11.

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

Руководят семинаром Н. К. Верещагин, А. Е. Ромащенко и А. Х. Шень. Семинар работает по четвергам с 18:05 до 19:40.

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

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

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

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

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

Подробную программу и конспекты лекций можно посмотреть на странице http://lpcs.math.msu.su/~ver/.

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

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

В курсе излагаются основные результаты теории сложности вычислений — одной из центральных областей теоретической информатики. Подробную программу и конспекты лекций можно посмотреть на странице http://lpcs.math.msu.su/~ver/.

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

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

В курсе излагаются основные применения теории сложности вычислений в криптографии. Главным из таких применений является возможность дать точные определения надёжности криптографических протоколов и схем и в ряде случаев доказательство их надёжности. Подробную информацию можно найти на странице http://lpcs.math.msu.su/~ver/.

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

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

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

Адрес: http://lpcs.math.msu.su/rus/vybor.htm
Изменения внесены 06.12.2010.

Мати Рейнович ПЕНТУС