MIME-Version: 1.0
Server: CERN/3.0
Date: Tuesday, 07-Jan-97 15:20:13 GMT
Content-Type: text/html
Content-Length: 13319
Last-Modified: Friday, 20-Dec-96 15:21:51 GMT
Publications
Books:
Automated Reasoning: Essays in Honor of Woody Bledsoe. (editor).
Kluwer Academic, Dordrecht, The Netherlands, 1991. Picture of Woody.
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.
Articles:
Mechanized Formal Reasoning about Programs and
Computing Machines, with J Strother Moore, 1996 (to appear -- an odd
phrase in this context).
Automated Proofs of Object Code for a Widely Used
Microprocessor, with Yuan Yu, Journal of the ACM, January
1996, Vol. 43, No. 1, pp. 166-192. (This is a major revision and
extension of the paper "Automated Correctness Proofs of Machine Code
Programs for a Commercial Microprocessor", see below. The
comprehensive treatment of this subject may be found in Yuan Yu's 700+
page dissertation.)
Woody Bledsoe: His Life and Legacy, with Michael Ballantyne
and Larry Hines, AI Magazine, Vol. 17, No. 1, Spring 1996,
pp. 7-20. Picture of Woody.
The Boyer-Moore Theorem Prover and Its Interactive Enhancement,
with M. Kaufmann
and J S. Moore, Computers and Mathematics with Applications,
Vol. 29, No. 2, pp. 27-62, 1995.
Automated Correctness Proofs of
Machine Code Programs for a Commercial Microprocessor, with Yuan Yu,
in D. Kapur, editor, Automated Deduction -- CADE-11, Lecture
Notes in Computer Science 607, Springer-Verlag, 1992, pp. 416-430.
MJRTY - A Fast Majority Vote Algorithm, with J S. Moore, in Robert S.
Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe.
Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 105-117.
A Biographical Sketch of W. W. Bledsoe, with Anne Boyer, in Robert S.
Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe.
Kluwer Academic, Dordrecht, The Netherlands, 1991, pp. 1-29.
Functional Instantiation in First Order Logic, with D. Goldschlag, M.
Kaufmann, and J Moore, in V. Lifschitz (editor), Artificial
Intelligence and Mathematical Theory of Computation: Papers in Honor
of John McCarthy. Academic Press, 1991, pp. 7-26.
The file fs.ps is a somewhat extended version of the published version
because it contains some proofs that were omitted from the published
version.
A Theorem Prover for a Computational Logic, with J S. Moore, keynote
address, Automated Deduction -- CADE-10, Lecture Notes in Computer
Science 449, Springer-Verlag, 1990, pp. 1-15.
The Use of a Formal Simulator to Verify a Simple Real Time Control
Program, with M. W. Green and J S. Moore. in W. H. J. Feijen, A. J.
M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our
Business, Springer-Verlag, 1990, pp. 54-66.
The Efficient Implementation of Lattice Operations, with H. Ait-Kaci,
P. Lincoln, and R. Nasr. Association for Computing Machinery
Transactions on Programming Languages and Systems, Vol. 11, No. 1,
pp. 115-146, January 1988.
The Addition of Bounded Quantification and Partial Functions to a
Computational Logic and Its Theorem Prover, with J S. Moore, Journal
of Automated Reasoning, Volume 4, pp. 117-172, 1988.
Integrating Decision Procedures into Heuristic Theorem Provers: A Case
Study of Linear Arithmetic, with J S. Moore. Machine
Intelligence 11, Oxford University Press, 1988, pp. 83-124.
Set Theory in First Order Logic: Clauses for Goedel's Axioms, with E.
Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos, Journal of
Automated Reasoning, Vol. 2, No. 3., pp. 287-327, 1986.
Program Verification, with J S. Moore. Automated Reasoning, Vol. 1,
No. 1, 1985, pp. 17-23.
A Mechanical Proof of the Turing Completeness of PURE LISP, with J S.
Moore. In W. W. Bledsoe and D. W. Loveland, editors, Contemporary
Mathematics, Volume 29, Automated Theorem Proving: After 25 Years,
American Mathematical Society, Providence, Rhode Island, 1984, pp.
132-168.
Proof-Checking, Theorem-Proving, and Program Verification, with
J S. Moore. In W. W. Bledsoe and D. W. Loveland, editors,
Contemporary Mathematics, Volume 29, Automated Theorem Proving:
After 25 Years, American Mathematical Society, Providence, Rhode
Island, 1984, pp. 119-132.
Proof Checking the RSA Public Key Encryption Algorithm, with
J S. Moore. American Mathematical Monthly, Vol. 91, No. 3, March
1984, pp. 181-189.
A Mechanical Proof of the Unsolvability of the Halting Problem, with
J S. Moore. Journal of the Association for Computing Machinery, Vol.
31, No. 3, July 1984, pp.441-458.
A Verification Condition Generator for FORTRAN, with J S. Moore. In
R. S. Boyer and J S. Moore, editors, The Correctness Problem in
Computer Science, Academic Press, London, 1981, pp. 9-101.
Metafunctions: Proving Them Correct and Using Them Efficiently as New
Proof Procedures, with J S. Moore. In R. S. Boyer and J S. Moore,
editors, The Correctness Problem in Computer Science, Academic Press,
London, 1981, pp. 103-184.
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory,
with J S. Moore. Proceedings of the 5th International Joint Conference
on Artificial Intelligence, pp. 511-519, 1977.
A Fast String Searching Algorithm, with J S. Moore. Communications of
the Association for Computing Machinery, Vol. 20, No. 10, pp. 762-772,
1977.
Primitive Recursive Program Transformation, with J S. Moore and R. E.
Shostak. Proceedings of the Third Association for Computing Machinery
Symposium on Principles of Programming Languages, Atlanta, 1976.
SELECT--A Formal System for Testing and Debugging Programs, with K. N.
Levitt and B. Elspas. Proceedings of the International Conference
on Reliable Software, IEEE Catalogue Number 75CHO940-7CSR, pp.
234-245, 1975.
Proving Theorems about LISP Functions, with J S. Moore. Journal of
the Association for Computing Machinery, Vol. 22, No. 1, pp. 129-144,
1975.
The Sharing of Structure in Theorem-proving Programs, with J S. Moore.
In B. Meltzer and D. Michie, editors, Machine Intelligence, Vol. 7,
pp. 101-116, Edinburgh University Press, 1972.
Computer Proofs of Limit Theorems, with W. W. Bledsoe and W. H.
Henneman, Artificial Intelligence, Vol. 3, No. 1, pp. 27-60, 1972.
Other Writing:
Let's
Name the Building for Nobel Prize Winner H. J. Muller, op-ed piece,
University of Texas student newspaper Daily Texan, November
17, 1995.
http://www.cs.utexas.edu/users/boyer/fp/flames.html.
Bledsoe funeral oration, October 7, 1995.
http://www.cs.utexas.edu/users/boyer/bledsoe-funeral-oration.html
My views on undergraduate education in computer science, September,
1995.
http://www.cs.utexas.edu/users/boyer/rigor-iv.ps.
Comments upon the document "America in the Age of Information," the
Strategic Implementation Plan of the Committee on Information and
Communications of the National Science and Technology Council,
June 27, 1995.
ftp://ftp.cs.utexas.edu/pub/boyer/cic.whitepaper
A Few Minor Remarks (on Metafunctions), Proceedings of the Workshop on
Correctness and Metatheoretic Extensibility of Automated Reasoning
Systems, INRIA Lorraine, Nancy, France, 1994, p. 22.
Metafunctions in Nqthm and Acl2, with Matt Kaufmann and J Moore,
Proceedings of the Workshop on Correctness and Metatheoretic
Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy,
France, 1994, pp. 16-18.
A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We
Build One? Can We?, Proceedings of the 12th Annual Conference on
Automated Deduction, Springer-Verlag Lecture Notes in Computer Science,
Number 814, 1994, p. 237.
The preface to Machine Proofs in Geometry: Automated Production of
Readable Proofs for Geometry Theorems, Shang-Ching Chou, Xiao-Shan
Gao, and Jing-Zhong Zhang, World Scientific, 1994, pp. vii-viii.
A Formal Specification of Some User Mode Instructions for the Motorola
68020, with Yuan Yu, Technical Report TR-92-04, Computer Sciences
Department, University of Texas at Austin, Austin, Texas 78712, 1992.
Article in opposition to a multicultural curricular proposal,
University of Texas student newspaper Daily Texan,
December, 1991.
http://www.cs.utexas.edu/users/boyer/multicult.html.
Response, biographical sketch, and photo on the occasion of
receipt of the 1991 AMS Current Award for Automatic Theorem Proving,
Notices of the American Mathematical Society, vol. 38, no. 5, pp.
407-408.
The Code for a Computational Logic, with J S. Moore, Technical Report
24, Computational Logic, Inc., Austin, Texas, 1988.
Basic Events for a Computational Logic, with J S. Moore, Technical
Report Technical Report 25, Computational Logic, Inc., Austin, Texas
1988.
Efficient Unification and Backtracking in a Portable, C-based Lisp, with
W. Schelter. MCC Technical Report AI-102-87, 1987.
On Adding Some Theorem Proving Techniques to Lisp, with M. Ballantyne
and V. Lifschitz. MCC Technical Report ACA-AI-271-87-Q, 1987.
Rewrite Rule Compilation, MCC Technical Report AI-194-86-P, 1985.
A Prototype Theorem-Prover for a Higher-Order Functional Language,
with M. Kaufmann, Burroughs Austin Research Center, Technical Report
ARC 84-17, 1984.
On the Feasibility of Mechanically Verifying SASL Programs, with M.
Kaufmann, Burroughs Austin Research Center, Technical Report ARC
84-16, 1984.
The Mechanical Verification of a FORTRAN Square Root Program, with J
S. Moore. Technical Report, Computer Science Laboratory Report, SRI
International, 1981.
A Theorem-Prover for Recursive Functions, with J S. Moore. Software
Engineering Notes, Association for Computing Machinery, Vol. 5, No. 3,
pp. 26-27, 1980.
The FORTRAN Verification System, with J S. Moore. Software
Engineering Notes, Association for Computing Machinery, Vol. 5, No.
3, pp. 16-17, 1980.
A Theorem-Prover for Recursive Functions: A User's Manual, with J S.
Moore. Technical Report CSL-91, Computer Science Laboratory, SRI
International, 1979.
A Provably Secure Operating System: The System, Its Applications, and
Proofs, with P. G. Neumann, et al. Technical Report CSL-116, Computer
Science Laboratory, SRI International, 1977.
Pretty-print. Technical Report 64, Department of Computational Logic,
University of Edinburgh, 1973.
The 77-Editor, with J S. Moore and D. J. M. Davies. Technical Report 62,
Department of Computational Logic, University of Edinburgh, 1973.
Locking: A Restriction of Resolution. Ph. D. Thesis, Mathematics
Department, University of Texas, Austin, 1971.
The Boyer-Moore theorem-proving system (also known as Nqthm) may be
obtained by anonymous ftp from Internet site ftp.cli.com. The most
recent release of this program occurred in January, 1994. To obtain a
copy, fetch the file /pub/nqthm/nqthm-1992/README and follow the
directions therein. The Common Lisp sources for the system are
included in the release. The most recent release includes many
mechanically-checked theorems formulated by Bevier, Boyer, Brock,
Bronstein, Cowles, Flatau, Hunt, Kaufmann, Kunen, Moore, Nagayama,
Russinoff, Shankar, Talcott, Wilding, Yu, and others. Altogether, the
the most recent release, including the examples and documentation,
comprises approximately 15 megabytes. Running the theorem-prover on
these examples generates approximately 140 megabytes of readable
proofs.
An alternative site for the sources is here .
Back to Boyer's web page.