Robert S. Boyer

Boyer graduated from the University of Texas at Austin, where he received his doctorate in 1971 with Woodrow Bledsoe (Locking: A restriction to resolution). 1970/71 he conducted research at the AI ​​Lab of the Massachusetts Institute of Technology, and from 1971 to 1973 at the University of Edinburgh. From 1973 he was a scientist at SRI International in Menlo Park, and since 1981 professor at the University of Texas at Austin. In 2008 he retired.

1985 to 1987 he studied also at the Microelectronics and Computer Technology Corporation in Austin and from 1993 to 1995 at Computational Logic Inc., Austin.

He developed with J. Strother Moore the Boyer- Moore algorithm (a string - matching algorithm ) and an automatic proof program, the Boyer -Moore Theorem Prover ( Nqthm, 1992), for which both Matt Kaufmann 2005 ACM Software System Award were given. With Kaufmann and Moore, he developed a further automatic proof system ACL2 (A Computational Logic for Applicative Common Lisp ).

Writings

  • With J. Strother Moore Computational Logic, Academic Press 1979
  • With J. Strother Moore A Computational Logic Handbook, Academic Press, 1988
Menlo Park, California J Strother Moore Boyer–Moore string search algorithm Integrated Authority File
688232
de