Larry Wos
Lawrence „Larry“ T. Wos (* 1930 in Chicago) ist ein US-amerikanischer Mathematiker, der sich mit automatischem Beweisen beschäftigt, also Techniken entwickelt, mit deren Hilfe ein Computerprogramm mathematische Beweise finden kann.
Inhaltsverzeichnis
Leben
Wos. der von Geburt an blind war, wuchs mit Mutter und zwei Schwestern in einem ärmeren Viertel der West Side von Chicago auf, wo ihn seine Mutter, die in einer Fabrik arbeitete, nachdem der Vater die Familie verlassen hatte, ihn ohne Rücksicht auf seine Blindheit aufzog. Sein mathematisches Talent wurde frühzeitig erkannt und fand ihren Niederschlag in verschiedenen Zeitungsspalten. Er studierte Mathematik an der University of Chicago, wobei er als einziger blinder Student mit anderen einen geeigneten Braille-Code für Mathematik entwickelte. Zu seinen Lehrern gehörten Paul Halmos und Irving Kaplansky. 1950 erhielt er seinen Bachelor-Abschluss. Nach dem Master-Abschluss 1954 ging er auf den Rat von Halmos an die University of Illinois at Urbana-Champaign, an der er 1957 bei Reinhold Baer promoviert wurde (On Commutative Prime Power Subgroups of the Norm). Da der Dekan seiner Fakultät keine blinden Lehrer fördern wollte wechselte er zur Informatik. 1957 wechselte er als Programmierer an das Argonne National Laboratory bei Chicago, an dem er für den Rest seiner Karriere blieb. 1963 begann er sich dort für automatisches Beweisen zu interessieren (Automated theorem proving, ATP), als das Gebiet noch im Anfangsstadium war.
Von ihm stammen viele Fortschritte auf dem Gebiet wie die Erfindung der quad arithmetic in den 1970er Jahren und der Paramodulation als Technik zur Gleichheitsbehandlung. Er erzielte Fortschritte bei der Lösung des lange offenen Robbins Problem (nach Herbert Robbins) in der Booleschen Algebra. Das Robbins-Problem wurde 1996 durch seinen Kollegen William McCune (1953–2011), dem Entwickler von Otter und Prover9, mit Hilfe des am Argonne Lab entwickelten ATP-Programm EQP (Equational Prover) gelöst wurde. An dem Problem hatten sich unter anderem Alfred Tarski und seine Schüler vergeblich versucht.
Wos spielt Bowling und brachte es dort zum US-Meister für blinde Bowler. Er soll auch zur Mathematik und Informatik durch sein Faible für Poker gekommen sein, und seine Erfahrung als Spieler beeinflusst seine Herangehensweise an Probleme innerhalb des ATP.
1983 erhielt er mit Steve Winker als erster den Preis der American Mathematical Society für Automated Theorem Proving und 1992 als erster den Herbrand Award der Association for Automated Reasoning.
Schriften
- mit Gail Pieper: Collected Works of Larry Wos, 2 Bände, World Scientific 2000
- mit Gail Pieper: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific 1999
- mit Gail Pieper: Automated Reasoning and the Discovery of Missing and Elegant Proofs, World Scientific 2003
Literatur
- Robert Veroff (Hrsg.): Automated reasoning and its applications: essays in honor of Larry Wos, MIT Press 1997