Robert Stephen Boyer est un informaticien américain. Il a été professeur à l'université du Texas à Austin.
Carrière
Boyer étudie à l'Université du Texas à Austin, où il obtient son Ph. D. en 1971 sous la direction de Woody Bledsoe (Locking : A restriction to resolution). En 1970-71, il est chercheur au Laboratoire d'intelligence artificielle du Massachusetts Institute of Technology et, de 1971-1973, à l'Université d'Édimbourg. À partir de 1973, Boyer est chercheur chez SRI International à Menlo Park et à partir de 1981, il est professeur à l'Université du Texas à Austin. En 2008, il devient émérite.
De 1985 à 1987 il est également chercheur chez Microelectronics and Computer Technology Corporation à Austin. En 1983 il fonde, avec J Strother Moore), l'entreprise Computational Logic Inc. à Austin où il travaille jusqu'en 1995.
Travaux Boyer a développé, avec J Strother Moore, l'algorithme de Boyer-Moore (l'un des premiers algorithmes de recherche de sous-chaîne. Il a également conçu, toujours avec J Strother Moore et Kaufmann un programme de démonstration automatique de théorèmes, le Boyer-Moore Theorem Prover (Nqthm, 1992), pour lesquels ils ont reçu en 2005, le prix ACM Software System. Avec Kaufmann et Moore, il a développé un autre système de preuve automatique, appelé ACL2 (A Computational Logic for Applicative Common Lisp).
En 1999, il a reçu, avec J Strother Moore, le prix Herbrand.
Publications (sélection)
.
.
. . — avec des contributions de : Dijkstra, E. W.; Burstall, R. M.; Goguen, J. A.; Manna, Z.; Pnueli, A.
Notes et références
Liens externes Page personnelle
Catégorie:Date de naissance non renseignée (XXe siècle) Catégorie:Informaticien américain du XXe siècle Catégorie:Informaticien américain du XXIe siècle Catégorie:Universitaire américain du XXe siècle Catégorie:Universitaire américain du XXIe siècle