en Robert S. Boyer

Robert Stephen Boyer
Robert Stephen Boyer
Born	August 2, 1946 (age 78); Washington, D. C.
Nationality	American
Education	Ph.D. in Mathematics
Alma mater	University of Texas at Austin
Occupation(s)	Computer scientist, mathematician
Employer(s)	The University of Texas at Austin; University of Edinburgh
Known for	Boyer–Moore string-search algorithm, Nqthm, ACL2
Spouse	Anne Olivia Herrington
Children	Madeleine, Margaret, Nathaniel
	Scientific career
Thesis	Locking: A Restriction of Resolution (1971)
Doctoral advisor	Woodrow Wilson Bledsoe
Website	https://www.cs.utexas.edu/~boyer/

Robert Stephen Boyer is an American retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string-search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore also collaborated on the Boyer–Moore automated theorem prover, Nqthm, in 1992.^[2] Following this, he worked with Moore and Matt Kaufmann on another theorem prover called ACL2. He was elected AAAI Fellow in 1991.^[3]

Publications

Boyer has published extensively, including the following books:

A Computational Logic Handbook, with J S. Moore. Second Edition. Academic Press, London, 1998.
Automated Reasoning: Essays in Honor of Woody Bledsoe, editor. Kluwer Academic, Dordrecht, The Netherlands, 1991.
A Computational Logic Handbook, with J S. Moore. Academic Press, New York, 1988.
The Correctness Problem in Computer Science, editor, with J S. Moore. Academic Press, London, 1981.
A Computational Logic, with J S. Moore. Academic Press, New York, 1979.