Larry Wos
From Wikipedia, the free encyclopedia
1930
Larry Wos | |
|---|---|
| Born | Lawrence T. Wos 1930 Chicago, U.S. |
| Died | August 21, 2020 |
| Known for | Theorem proving |
| Awards | Herbrand Award (1992) |
| Scientific career | |
| Thesis | On Commutative Prime Power Subgroups of the Norm (1957) |
Lawrence T. Wos (1930–2020) was an American mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratory.[1]
Wos studied at the University of Chicago, receiving a bachelor's degree in 1950 and a master's in mathematics in 1954, and went on for doctoral studies at the University of Illinois at Urbana-Champaign where he received PhD in 1957 supervised by Reinhold Baer.[2] He joined Argonne in 1957, and began using computers to prove mathematical theorems in 1963.[3][4]
Wos was congenitally blind. He was an avid bowler, the best male blind bowler in the US.[5][6][7]
Awards and honors
In 1982, Wos and his colleague Steve Winker were the first to win the Automated Theorem Proving Prize, given by the American Mathematical Society.[5] In 1992, Wos was the first to win the Herbrand Award for his contributions to the field of automated deduction.[8] A festschrift in his honor, Automated reasoning and its applications: essays in honor of Larry Wos (Robert Veroff, ed.) was published by the MIT Press in 1997 (ISBN 0-262-22055-5).