Robert S. Boyer
Robert Stephen Boyer | |
|---|---|
| Born | August 2, 1946 Washington, D. C. |
| Education | Ph.D. in Mathematics |
| Alma mater | University of Texas at Austin |
| Occupations | Computer scientist, mathematician |
| Employers | |
| 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. Following this, he worked with Moore and Matt Kaufmann on another theorem prover called ACL2. He was elected AAAI Fellow in 1991.