Robert S. Boyer
From Wikipedia, the free encyclopedia
| Nationalité | |
|---|---|
| Formation | |
| Activité |
Universitaire, informaticien |
| A travaillé pour | |
|---|---|
| Membre de | |
| Directeur de thèse | |
| Distinctions |
Robert Stephen Boyer est un informaticien américain. Il a été professeur à l'université du Texas à Austin.
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)[1] 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.
