J Strother Moore
J Strother Moore is an American computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moore automated theorem prover, Nqthm. He made pioneering contributions to structure sharing including the piece table data structure and early logic programming. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his Bachelor of Science in mathematics at Massachusetts Institute of Technology in 1970 and his Doctor of Philosophy in computational logic at the University of Edinburgh in Scotland in 1973.
In addition, Moore is a co-author of the ACL2 automated theorem prover and its predecessors including Nqthm, for which he received, with Robert S. Boyer and Matt Kaufmann, the 2005 ACM Software System Award. He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.
For his contributions to automated deduction, Moore received the 1999 Herbrand Award with Robert S. Boyer, and in 2006 he was inducted as a Fellow in the Association for Computing Machinery.
In addition, Moore is a co-author of the ACL2 automated theorem prover and its predecessors including Nqthm, for which he received, with Robert S. Boyer and Matt Kaufmann, the 2005 ACM Software System Award. He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.
For his contributions to automated deduction, Moore received the 1999 Herbrand Award with Robert S. Boyer, and in 2006 he was inducted as a Fellow in the Association for Computing Machinery.
