Jump to content

Robert S. Boyer

From Wikipedia, the free encyclopedia
Robert Stephen Boyer
Born (1946-08-02) August 2, 1946 (age 78)[1]
Washington, D. C.
NationalityAmerican
EducationPh.D. in Mathematics
Alma materUniversity of Texas at Austin
Occupation(s)Computer scientist, mathematician
Employer(s)The University of Texas at Austin
University of Edinburgh
Known forBoyer–Moore string-search algorithm, Nqthm, ACL2
SpouseAnne Olivia Herrington[1]
ChildrenMadeleine, Margaret, Nathaniel[1]
Scientific career
Thesis Locking: A Restriction of Resolution  (1971)
Doctoral advisorWoodrow Wilson Bledsoe
Websitehttps://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

[edit]

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.

See also

[edit]

References

[edit]
  1. ^ a b c Curriculum Vitae
  2. ^ "Nqthm, the Boyer–Moore prover". Retrieved 2006-04-21.
  3. ^ "Elected AAAI Fellows". AAAI. Retrieved 2024-01-02.
[edit]