Sergei N. Artemov

Sergei Artemov, a famous specialist in mathematical logic and theoretical computer science, and a member of our editorial board, celebrates his 50th birthday in 2001.

His main scientific interests are: mathematical logic and proof theory; logic in computer science; knowledge representation and artificial intelligence; automated deduction and verification; optimal control and hybrid systems. Here are just few of his results:

• The uniform arithmetical completeness theorem (1979).
• Non-axiomatizability theorem for first-order provability logics (1985).

• Logic of proofs — a new approach to formal provability (developed in 1993—97). Solving two problems left open from the 1930s: Gödel's problem on provability intepretation for modal logic S4; the problem of adequate formalization of the ideas of Kolmogorov and Gödel on interpreting intuitionistic connectives via operations on proofs.

• Discovery of a fundamental connection between modal logic and typed lambda-calculi (1995—99).
• Explicit provability model for verification (1997).
• Construction of reflexive lambda-calculus (2000).

Professor Artemov is also known as a gifted teacher. Many of his students are well-known specialists in mathematical logic: L. Beklemishev and M. Pentus (winners of the Moscow Mathematical society prize for young mathematicians), G. Japaridze, K. Ignatiev, A. Kopylov, V. Shavrukov, and others.

We wish Sergei Artemov many happy returns of the day.

Yu. Ilyashenko, V. Shehtman, M. Tsfasman