J Strother Moore
# J Strother Moore

J Strother Moore (né le 11 septembre 1947 à Seminole (Oklahoma)) est un informaticien américain. Il est professeur à l'université du Texas à Austin.

La lettre J est son prénom et n'est pas une abréviation.

## Carrière

Moore étudie au Massachusetts Institute of Technology (MIT) et obtient un Bachelor en 1970. En 1973 , il soutient un Ph. D. à l'université d'Édimbourg sous la supervision de Rodney Burstall (en) (Computational Logic: Structure Sharing and Proof of Program Properties). De 1973 à 1976, Moore est chercheur au Palo Alto Research Center , puis à partir de 1976 au Stanford Research Institute. À partir de 1983 il est professeur à l'université du Texas à Austin, à la fin titulaire de la Admiral B. R. Inman Centennial Chair. De 2001 à 2009 Moore dirige la faculté d'informatique. En 1983 il fonde, avec Robert S. Boyer, l'entreprise Computational Logic Inc. à Austin, et pendant dix ans il en est le directeur scientifique.

Moore est un alpiniste passionné.

## Travaux

Moore a développé, avec Robert Boyer, l'algorithme de recherche de sous-chaîne appelé l'algorithme de Boyer-Moore. Par ailleurs, ils ont conçu un programme de démonstration automatique appelé le Boyer-Moore Theorem Prover ou Nqthm (en), (992). Pour ce travail, ils ont reçu en 2005, avec Matt Kaufmann, le prix ACM Software System. Ils ont développé Nqthm en un système de démonstration automatique qui porte le nom ACL2.

## Prix et distinctions

Avant le prix ACM Software System en 2005, Boyer et Moore obtiennent le prix Herbrand en 1999 et en 1991 le Current Prize in Automatic Theorem Proving de l'American Mathematical Society. Moore est Fellow de l'Association for the Advancement of Artificial Intelligence, de l'Association for Computing Machinery et de l'Académie nationale d'ingénierie des États-Unis. En 2015 il est élu membre correspondant de la Royal Society of Edinburgh.

## Publications

* (en) avec Robert S. Boyer, A computational Logic, New York, Academic Press, coll. « ACM monograph series, Academic Press », 1980, xiv+397 (ISBN 978-0-12-122950-4)
* éditeur avec Robert S. Boyer, The correctness problem in computer science, Academic Press, 1981
* avec Robert S. Boyer, A Computational Logic Handbook, Academic Press, 1988 — Id., Academic Press, coll. « International series in formal methods », 1998, 2e éd., xxv +518 (ISBN 978-0-12-122955-9)
* Piton : a mechanically verified assembly-level language, Kluwer, 1996
* avec Matt Kaufmann et Panagiotis Manolios, Computer-aided reasoning : an approach, Kluwer, 2000
* éditeur avec Matt Kaufmann et Panagiotis Manolios, Computer-aided reasoning : ACL2 case studies = Kluwer, 2000
