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

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


Научные результаты лаборатории логических проблем информатики

Лаборатория логических проблем информатики основана в 1995 году на базе научно-исследовательских семинаров «Теория доказательств» и «Логические методы в информатике» (руководитель — профессор С.Н.Артемов), работающих на Механико-математическом факультете Московского государственного университета с 1984 года.

Важнейшие научные достижения семинара/лаборатории:

  • отрицательное решение проблемы аксиоматизируемости логики доказуемости первого порядка (С.Н.Артемов, В.Варданян, 1985);
  • классификационная теорема для пропозициональной логики доказуемости (Л.Д.Беклемишев, 1989, премия Московского математического общества);
  • доказательство справедливости гипотезы Хомского, высказанной в 1958 году, о контекстной свободности всех грамматик Ламбека (М.Р.Пентус, 1992);
  • решение проблемы L-полноты исчисления Ламбека, остававшейся открытой на протяжении 36 лет (М.Р.Пентус, премия FoLLI-IGPL, 1994);
  • разрешимость линейной аффинной логики (А.П.Копылов, премия Клини LICS, 1995);
  • решение проблемы МакКинси — Тарского 1944 года об аксиоматизируемости и разрешимости модальной логики канторовской операции производного множества для конечномерных вещественных пространств (В.Б.Шехтман, 1995);
  • создание операторной модальной логики, дающей искомую доказуемостную семантику для геделевой логики доказуемости S4; этот вопрос стоял с 1933 года (С.Н.Артемов, 1995);
  • создание точной доказуемостной модели операций Брауэра—Гейтинга—Колмогорова для интуиционистской пропозициональной логики; проблема оставалась открытой с 1930 года (С.Н.Артемов, 1995).