J Strother Moore
Encyclopedia
J Strother Moore is a computer scientist
, and he is a co-developer of the Boyer–Moore string search algorithm
and the Boyer–Moore automated theorem prover, Nqthm
. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his SB in mathematics at Massachusetts Institute of Technology
in 1970 and his Ph.D in computational logic
at University of Edinburgh
in Scotland in 1973.
In addition, Moore is a co-author of the ACL2 automated theorem prover. 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
of the Association for Computing Machinery
.
He is currently the Admiral B.R. Inman
Centennial Chair in Computing Theory at The University of Texas at Austin
.
Before joining the Department of Computer Sciences as the chair, he formed a company, Computational Logic Inc., along with others including his close friend at the University of Texas at Austin and one of the highly regarded professors in the field of Automated Reasoning, Robert S. Boyer
.
Moore enjoys rock climbing
.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, and he is a co-developer of the Boyer–Moore string search algorithm
Boyer–Moore string search algorithm
The Boyer–Moore string search algorithm is a particularly efficient string searching algorithm, and it has been the standard benchmark for the practical string search literature. It was developed by Bob Boyer and J Strother Moore in 1977...
and the Boyer–Moore automated theorem prover, Nqthm
Nqthm
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.- History :The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas, Austin. They began work on the system in 1971 in...
. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his SB in mathematics at Massachusetts Institute of Technology
Massachusetts Institute of Technology
The Massachusetts Institute of Technology is a private research university located in Cambridge, Massachusetts. MIT has five schools and one college, containing a total of 32 academic departments, with a strong emphasis on scientific and technological education and research.Founded in 1861 in...
in 1970 and his Ph.D in computational logic
Symbolic computation
Symbolic computation or algebraic computation, relates to the use of machines, such as computers, to manipulate mathematical equations and expressions in symbolic form, as opposed to manipulating the approximations of specific numerical quantities represented by those symbols...
at University of Edinburgh
University of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
in Scotland in 1973.
In addition, Moore is a co-author of the ACL2 automated theorem prover. He and others used ACL2 to prove the correctness of the floating point division operations of the AMD K5
AMD K5
The K5 was AMD's first x86 processor to be developed entirely in-house. Introduced in March 1996, its primary competition was Intel's Pentium microprocessor. The K5 was an ambitious design, closer to a Pentium Pro than a Pentium regarding technical solutions and internal architecture...
microprocessor
Microprocessor
A microprocessor incorporates the functions of a computer's central processing unit on a single integrated circuit, or at most a few integrated circuits. It is a multipurpose, programmable device that accepts digital data as input, processes it according to instructions stored in its memory, and...
in the wake of the Pentium FDIV bug
Pentium FDIV bug
The Pentium FDIV bug was a bug in the Intel P5 Pentium floating point unit . Certain floating point division operations performed with these processors would produce incorrect results...
.
For his contributions to automated deduction
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
, Moore received the 1999 Herbrand Award
Herbrand Award
The Herbrand Award for Distinguished Contributions to Automated Deduction is an award given by CADE Inc. to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or...
with Robert S. Boyer
Robert S. Boyer
Robert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
, and in 2006 he was inducted as a Fellow
Fellow
A fellow in the broadest sense is someone who is an equal or a comrade. The term fellow is also used to describe a person, particularly by those in the upper social classes. It is most often used in an academic context: a fellow is often part of an elite group of learned people who are awarded...
of the Association for Computing Machinery
Association for Computing Machinery
The Association for Computing Machinery is a learned society for computing. It was founded in 1947 as the world's first scientific and educational computing society. Its membership is more than 92,000 as of 2009...
.
He is currently the Admiral B.R. Inman
Bobby Ray Inman
Bobby Ray Inman is a retired United States admiral who held several influential positions in the U.S. Intelligence community.-Career:...
Centennial Chair in Computing Theory at The University of Texas at Austin
University of Texas at Austin
The University of Texas at Austin is a state research university located in Austin, Texas, USA, and is the flagship institution of the The University of Texas System. Founded in 1883, its campus is located approximately from the Texas State Capitol in Austin...
.
Before joining the Department of Computer Sciences as the chair, he formed a company, Computational Logic Inc., along with others including his close friend at the University of Texas at Austin and one of the highly regarded professors in the field of Automated Reasoning, Robert S. Boyer
Robert S. Boyer
Robert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
.
Moore enjoys rock climbing
Rock climbing
Rock climbing also lightly called 'The Gravity Game', is a sport in which participants climb up, down or across natural rock formations or artificial rock walls. The goal is to reach the summit of a formation or the endpoint of a pre-defined route without falling...
.