Scientific accomplishments
of the Laboratory LPCS

The Laboratory for Logical Problems of Computer Science (LPCS) was founded in 1995 on the basis of Sergei N. Artemov's research seminars "Proof theory" and "Logic in Computer Science" working at the Faculty of Mechanics and Mathematics, Moscow State University, since 1984.

The most important scientific accomplishments of the Seminars/Laboratory

• a negative solution of the axiomatizability problem for the first order Provability Logic (S.Artemov, V.Vardanyan, 1985),
• Classification Theorem for propositional provability logics (L.Beklemishev, 1989, Award for the best paper from the Moscow Mathematical Society),
• a proof of 33 years old Chomsky conjecture that all Lambek grammars are context free (M.Pentus, 1992),
• solution of a 36 years old "language completeness problem" for the Lambek calculus (M.Pentus, FoLLI/IGPL Award for the best paper, 1994),
• the decidability of the Affine Linear Logic (A.Kopylov, Kleene Award from LICS 1995),
• a solution of the McKinsey - Tarski's problem of 1944 on axiomatization and decidability of the modal logic of the derived set operation in the real n-dimentional space (V.Shehtman, 1995),
• the Operational Modal Logic, which provides an intended semantics for Goedel's provability logic S4; this problem was open since 1933 (S.Artemov, 1995)
• an exact provability model of Brouwer - Heyting - Kolmogorov operations for Intuitionistic Logic (remained open since 1930, S.Artemov, 1995).

Location: http://lpcs.math.msu.su/eng/lpcssa.htm
Last modified 30.12.1997.