C. Nelson

C. Gregory Nelson was a computer scientist at Digital Equipment Corporation’s Systems Research Center whose work on automated theorem proving and program verification helped lay the intellectual foundations for the field now known as satisfiability modulo theories. Nelson grew up in Honolulu and earned his B.A. in mathematics from Harvard University in 1976. Even before completing his doctorate, he invented the Nelson-Oppen method — a procedure for combining decision algorithms for different logical theories into a unified decision procedure — work that became foundational in the automated reasoning community. He completed his Ph.D. in computer science at Stanford University in 1980 under the supervision of Robert Tarjan. Much of his subsequent career was spent at Xerox PARC, Digital Equipment Corporation’s Systems Research Center, and HP Labs, where he developed the influential Simplify theorem prover and contributed to the design of Modula-3 and the extended static checking (ESC) discipline for Java. He received the Herbrand Award for Distinguished Contributions to Automated Reasoning from the Conference on Automated Deduction. Harvey Mudd College and Carnegie Mellon have both established honors in memory of other Hertz Fellows from his era, and the theorem proving community he shaped continues to build on his contributions.