The Laboratory for Logical Problems of Computer Science (LPCS)
was founded in 1995 on the basis of Sergei N. Artemov's research
"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
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
the decidability of the Affine Linear Logic
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
an exact provability model of Brouwer - Heyting - Kolmogorov operations for
Intuitionistic Logic (remained open since 1930, S.Artemov, 1995).
Last modified 30.12.1997.