Robert S. Boyer

Robert Stephen Boyer (geb. vor 1971) ist ein US-amerikanischer Informatiker. Er war Professor an der University of Texas at Austin.

Boyer studierte an der University of Texas at Austin, an der er 1971 bei Woody Bledsoe promoviert wurde (Locking: A restriction to resolution).[1] 1970/71 forschte er am AI Lab des Massachusetts Institute of Technology und 1971 bis 1973 an der University of Edinburgh. Ab 1973 war er Wissenschaftler bei SRI International in Menlo Park und ab 1981 Professor an der University of Texas at Austin. 2008 emeritierte er.

1985 bis 1987 forschte er außerdem bei der Microelectronics and Computer Technology Corporation in Austin und 1993 bis 1995 bei Computational Logic Inc. in Austin.

Er entwickelte mit J Strother Moore den Boyer-Moore-Algorithmus (ein String-Matching-Algorithmus) und ein automatisches Beweisprogramm, den Boyer-Moore Theorem Prover (Nqthm, 1992), für das beide mit Matt Kaufmann 2005 den ACM Software System Award erhielten. Mit Kaufmann und Moore entwickelte er ein weiteres automatisches Beweissystem ACL2 (A Computational Logic for Applicative Common Lisp).

1999 erhielt er den Herbrand Award.