Robert Stephen Boyer is an American retired
professor of
computer science,
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, and
philosophy
Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. Some ...
at
The University of Texas at Austin. He and
J Strother Moore
J Strother Moore (his first name is the alphabetic character "J" – not an abbreviated "J.") is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moo ...
invented the
Boyer–Moore string-search algorithm
In computer science, the Boyer–Moore string-search algorithm is an efficient string-searching algorithm that is the standard benchmark for practical string-search literature. It was developed by Robert S. Boyer and J Strother Moore in 1977.
T ...
, a particularly efficient
string searching algorithm, in 1977. He and Moore also collaborated on 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 ...
, in 1992.
Following this, he worked with Moore and Matt Kaufmann on another theorem prover called
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 to ...
.
Publications
Boyer has published extensively, including the following books:
* ''A Computational Logic Handbook'', with J S. Moore. Second Edition. Academic Press, London, 1998.
* ''Automated Reasoning: Essays in Honor of Woody Bledsoe'', editor. Kluwer Academic, Dordrecht, The Netherlands, 1991.
* ''A Computational Logic Handbook'', with J S. Moore. Academic Press, New York, 1988.
* ''The Correctness Problem in Computer Science'', editor, with J S. Moore. Academic Press, London, 1981.
* ''A Computational Logic'', with J S. Moore. Academic Press, New York, 1979.
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 ...
*
QED manifesto
The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. ( Q.E.D. means in Latin, meaning "which was to be demonstrated.")
Overview
T ...
References
External links
Home page of Robert S. Boyer Accessed February 18, 2016.
University of Texas, College of Liberal Arts Honors Retired Faculty - 2008 Accessed March 21, 2009.
Robert Stephen Boyerat the
Mathematics Genealogy Project
Living people
Alumni of the University of Edinburgh
University of Texas at Austin faculty
Fellows of the Association for the Advancement of Artificial Intelligence
Year of birth missing (living people)
Formal methods people
Lisp (programming language) people
{{US-compu-bio-stub