Scientific achievements of the
Laboratory LPCS
The Laboratory for Logical Problems of Computer Science (LPCS)
was founded in 1995 on the basis of Sergei 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 achievements 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 ndimentional 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).
Last modified 30.12.1997.
Mati Pentus