Лаборатория логических проблем в информатике

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

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

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