Larry Wos

from Wikipedia, the free encyclopedia

Lawrence "Larry" T. Wos (* 1930 in Chicago ) is an American mathematician who deals with automatic proofs , ie develops techniques with which a computer program can find mathematical proofs.

Life

What. Blind from birth, grew up with mother and two sisters in a poorer neighborhood on the West Side of Chicago, where his mother, who worked in a factory after his father left the family, raised him regardless of his blindness . His mathematical talent was recognized early on and found expression in various newspaper columns. He studied mathematics at the University of Chicago , where he was the only blind student to develop suitable Braille code for mathematics with others . His teachers included Paul Halmos and Irving Kaplansky . In 1950 he received his bachelor's degree. After completing his master's degree in 1954, on the advice of Halmos, he went to the University of Illinois at Urbana-Champaign , where he received his doctorate in 1957 under Reinhold Baer (On Commutative Prime Power Subgroups of the Norm). Since the dean of his faculty did not want to encourage blind teachers, he switched to computer science. In 1957 he moved to the Argonne National Laboratory near Chicago as a programmer , where he stayed for the rest of his career. In 1963 he became interested in automated theorem proving (ATP) there, when the field was still in its infancy.

He made many advances in the field such as the invention of quad arithmetic in the 1970s and paramodulation as a technique for treating equality. He made progress in solving the long-open Robbins problem (after Herbert Robbins ) in Boolean algebra. The Robbins problem was solved in 1996 by his colleague William McCune (1953-2011), the developer of Otter and Prover9, with the help of the ATP program EQP (Equational Prover) developed at the Argonne Lab. Alfred Tarski and his students tried to solve the problem in vain.

Wos plays bowling and became the US champion for blind bowlers. He is also said to have got into math and computer science through his penchant for poker , and his experience as a player influences his approach to problems within the ATP.

In 1983 he and Steve Winker were the first to receive the American Mathematical Society's Prize for Automated Theorem Proving and in 1992 the first to receive the Herbrand Award from the Association for Automated Reasoning.

Fonts

  • with Gail Pieper: Collected Works of Larry Wos, 2 volumes, World Scientific 2000
  • with Gail Pieper: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific 1999
  • with Gail Pieper: Automated Reasoning and the Discovery of Missing and Elegant Proofs, World Scientific 2003

literature

  • Robert Veroff (Ed.): Automated reasoning and its applications: essays in honor of Larry Wos, MIT Press 1997

Web links

Individual evidence

  1. ↑ Larry Wos in the Mathematics Genealogy Project (English)Template: MathGenealogyProject / Maintenance / id used
  2. ^ Tim Andrew Obermiller, Top of his game, University of Chicago Magazine, Online
personal data
SURNAME Wos, Larry
ALTERNATIVE NAMES Wos, Lawrence
BRIEF DESCRIPTION American mathematician and computer scientist
DATE OF BIRTH 1930
PLACE OF BIRTH Chicago