S. Maslov is known as the author of the inverse method in automated deduction [1] which was discovered at the same time as the resolution method of J.A. Robinson and has approximately the same range of applications. In 1981 Maslov proposed an iterative algorithm for propositional satisfiability based on some general search ideas described in detail in his book [2] published posthumously. When in 1982 Maslov was killed at the age of 43 in a car accident, a seminar was started to follow through on his ideas. The result of this collective research forms the bulk of the present book. Nina Maslova was a mathematician in her own right. She was awarded the National Prize in Mathematics, one of the highest distinctions for mathematics in the former Soviet Union. When she died in 1993 at the age of 54, the St. Petersburg Mathematical Society convened a special meeting in her honor.

The intellectual influence of the Maslov family was not restricted, however, to their scientific achievements. Their home in Leningrad (now St. Petersburg) was a meeting place of a seminar where talks on social and scientific problems were presented. One has to feel the gravity of the ideological pressure of a totalitarian state to appreciate the importance of such a free forum. The emergence of such seminars seems to be characteristic of intellectual life under oppressive regimes: recall Zilsel's seminar in Vienna where Gödel presented in January 1938 his overview [3] of possibilities for continuing Hilbert's program. Another forum for dissident thought in the USSR was provided by a Samizdat (unofficially published) journal "Summa" edited by S. Maslov [4] which was designed as a review journal for Samizdat publications.

One may hope that this book will contribute to further progress of knowledge and understanding which was the goal of Nina Maslova and Sergei Maslov.

Grigori Mints
Stanford, June 1996

[1] Maslov S.Yu., Theory of Deductive Systems and its applications, The MIT Press, 1987. Russian original 1986.

[2] Maslov S.Yu., An inverse method of establishing deducibilities in the classical predicate calculus, Soviet Mathematics, Doklady, 1964,5, 1420-1423.

[3] Gödel K., Lecture at Zilsel's, in: Feferman S. et al.(eds.), Collected works of Kurt Gödel, v. III, 87-113, Oxford University Press, 1995

[4] Vershik A., Potainoi daidzhest vremen zastoia (Concealed digest of stagnation times) Zvezda, 1991 no 11, St. Petersburg (Russian)

[5] G.Davydov, Yu. Matiyasevich, G. Mints, V. Orevkov, A. Slisenko, N. Shanin. Sergei Yuryevich Maslov. Obituary. Russian Math. Surveys, 39, no 2, 1984, 133-135

[6] Problemy Sokrashchenia Perebora, Voprosy Kibernetiki no. 131, (Russian), Scientific Council "Cybernetics'' of the USSR Academy of Sciences,  1987. English translation: Problems of reducing the exhaustive search, 53--64,
Amer. Math. Soc. Transl. Ser. 2, 178, Amer. Math. Soc., Providence, RI, 1997.