Robert S. Boyer

from Wikipedia, the free encyclopedia

Robert Stephen Boyer (born before 1971) is an American computer scientist. He was a professor at the University of Texas at Austin .

Boyer studied at the University of Texas at Austin, where he received his doctorate from Woody Bledsoe in 1971 ( Locking: A restriction to resolution ). In 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 from 1981 professor at the University of Texas at Austin. In 2008 he retired.

1985 to 1987 he also carried out research at Microelectronics and Computer Technology Corporation in Austin and from 1993 to 1995 at Computational Logic Inc. in Austin.

He developed with J Strother Moore the Boyer-Moore algorithm (a string searching algorithm ) and an automatic proof program, the Boyer-Moore Theorem Prover (NQTHM, 1992), for both Matt Kaufmann 2005 ACM Software System Award received . With Kaufmann and Moore he developed another automatic evidence system ACL2 (A Computational Logic for Applicative Common Lisp).

In 1999 he received the Herbrand Award .

Fonts

  • with J Strother Moore Computational Logic , Academic Press 1979
  • with J Strother Moore A Computational Logic Handbook , Academic Press 1988

Web links

Individual evidence

  1. ^ Mathematics Genealogy Project