Gregory S. Tseytin

Grigori Samuilovitsch Tseitin (, born November 15, 1936, in Leningrad, USSR, deceased August 27, 2022 in Campbell, CA, USA) was a Russian mathematician and computer scientist, who moved to the United States in 1999. He is best known for Tseitin transformation used in SAT solvers, Tseitin tautologies used in the proof complexity theory, and for his work on Algol 68.

Biography Tseitin studied mathematics at the Leningrad State University (now Saint Petersburg State University) from 1951 to 1956. He earned his PhD in 1960 under the supervision of Andrei Andreevich Markov. His dissertation was called "Algorithmic Operators on Constructive Complete Separable Metric Spaces". In 1968, he received the Russian doctoral degree (corresponding to a habilitation) from the same university. From 1960 to 2000 Tseitin worked at the and taught classes in computer science at his alma mater.

In 2006, Tseitin was recognized as an ACM Distinguished Scientist.

Works G. S. Tseitin. „On the complexity of derivation in propositional calculus“ in: J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970, S. 466–483. Berlin, Heidelberg, 1983.