Robert Stephen Boyer | |
|---|---|
| Born | August 2, 1946[1] 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[1] |
| Children | Madeleine, Margaret, Nathaniel[1] |
| 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]