HOME

TheInfoList



OR:

J Strother Moore (his first name is the alphabetic character "J" – not an abbreviated "J.") is a
computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...
. He is a co-developer of the Boyer–Moore string-search algorithm,
Boyer–Moore majority vote algorithm The Boyer–Moore majority vote algorithm is an algorithm for finding the majority of a sequence of elements using linear time and constant space. It is named after Robert S. Boyer and J Strother Moore, who published it in 1981,. Originally publis ...
, and the Boyer–Moore automated theorem prover,
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 ...
. He made pioneering contributions to structure sharing including the
piece table In computing, a piece table is a data structure typically used to represent a text document while it is edited in a text editor. Initially a reference (or 'span') to the whole of the original file is created, which represents the as yet unchanged ...
data structure and early
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic prog ...
. An example of the workings of the Boyer–Moore string search algorithm is give
in Moore's website
Moore received his
Bachelor of Science A Bachelor of Science (BS, BSc, SB, or ScB; from the Latin ') is a bachelor's degree awarded for programs that generally last three to five years. The first university to admit a student to the degree of Bachelor of Science was the University of ...
(BS) in mathematics at
Massachusetts Institute of Technology The Massachusetts Institute of Technology (MIT) is a private land-grant research university in Cambridge, Massachusetts. Established in 1861, MIT has played a key role in the development of modern technology and science, and is one of the ...
in 1970 and his
Doctor of Philosophy A Doctor of Philosophy (PhD, Ph.D., or DPhil; Latin: or ') is the most common Academic degree, degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields ...
(Ph.D.)Available at th
Edinburgh Research Archive
in
computational logic Computational logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is s ...
at the
University of Edinburgh The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 15 ...
in Scotland in 1973. In addition, Moore is a co-author of the
ACL2 ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed t ...
automated theorem prover and its predecessors including
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 ...
, for which he received, with Robert S. Boyer and Matt Kaufmann, the 2005
ACM Software System Award The ACM Software System Award is an annual award that honors people or an organization "for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both". It is awarded b ...
. He and others used ACL2 to prove the correctness of the floating point division operations of the
AMD K5 The K5 is 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 techn ...
microprocessor A microprocessor is a computer processor where the data processing logic and control is included on a single integrated circuit, or a small number of integrated circuits. The microprocessor contains the arithmetic, logic, and control circu ...
in the wake of the Pentium FDIV bug. For his contributions to
automated deduction Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...
, Moore received the 1999
Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important cont ...
with
Robert S. Boyer Robert Stephen Boyer is an American 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 efficie ...
, and in 2006 he was inducted as a
Fellow A fellow is a concept whose exact meaning depends on context. In learned or professional societies, it refers to a privileged member who is specially elected in recognition of their work and achievements. Within the context of higher education ...
in the
Association for Computing Machinery The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional member ...
. Moore was elected a member of the
National Academy of Engineering The National Academy of Engineering (NAE) is an American nonprofit, non-governmental organization. The National Academy of Engineering is part of the National Academies of Sciences, Engineering, and Medicine, along with the National Academy ...
in 2007 for contributions to automated reasoning about computing systems. He is also a Fellow of the AAAI. He was elected a Corresponding Fellow of the
Royal Society of Edinburgh The Royal Society of Edinburgh is Scotland's national academy of science and letters. It is a registered charity that operates on a wholly independent and non-partisan basis and provides public benefit throughout Scotland. It was established i ...
in 2015. He is currently the Admiral B.R. Inman Centennial Chair in Computing Theory at
The University of Texas at Austin The University of Texas at Austin (UT Austin, UT, or Texas) is a public research university in Austin, Texas. It was founded in 1883 and is the oldest institution in the University of Texas System. With 40,916 undergraduate students, 11,075 ...
, and was chair of the Department of Computer Science from 2001–2009. 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 In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer progra ...
, Robert S. Boyer. Moore enjoys
rock climbing Rock climbing is a sport in which participants climb up, across, or down natural rock formations. The goal is to reach the summit of a formation or the endpoint of a usually pre-defined route without falling. Rock climbing is a physically and ...
.


See also

*
Boyer–Moore majority vote algorithm The Boyer–Moore majority vote algorithm is an algorithm for finding the majority of a sequence of elements using linear time and constant space. It is named after Robert S. Boyer and J Strother Moore, who published it in 1981,. Originally publis ...


References


External links

*
"My" Best Ideas (from J Strother Moore's home page)Boyer–Moore fast string search algorithmMachines Reasoning about Machines
talk by J Strother Moore given at EPFL in 2011, providing an overview of some of his work American computer scientists Formal methods people Massachusetts Institute of Technology School of Science alumni Alumni of the University of Edinburgh University of Texas at Austin faculty Fellows of the Association for Computing Machinery Living people Year of birth missing (living people) Members of the United States National Academy of Engineering {{US-compu-bio-stub