Books

A Computational Logic Handbook, with J S. Moore. Academic Press,
London, 1998. Second Edition. xxv+518

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. xvi+408

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. xiv+397. Now public domain. The original Pub source for the book is here. The translation to TeX and pdf was kindly done by Gary Klimowicz.

Articles

Toward Automating the Discovery of Decreasing Measures, with Wilfred J. Legato and Victor W. Marek. Journal of Automated Reasoning, Vol. 35, pp. 355-371, December, 2005.

Single-Threaded Objects in ACL2, with J Strother Moore, in S. Krishnamurthi and C. R. Ramakrishnan, editors, Practical Aspects of Declarative Languages 2002, Lecture Notes in Computer Science 2257, 2002, Springer-Verlag, pp. 9-27.

Mechanized Formal Reasoning about Programs and Computing Machines, with J Strother Moore, in Robert Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1997, pp. 147-176.

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 (or fp.pdf) 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. (Many university library users and ACM members will be able to utilize this URL at the ACM site to read the paper, but not everyone.)

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



Circuit Specification, Abstraction, and Reverse Engineering, with Warren Hunt, ACL2 Workshop, 2007.

Function Memoization and Unique Object Representation for ACL2 Functions, with Warren Hunt, ACL2 Workshop, 2006.

A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance, with Warren A. Hunt, Jr., and Serita M. Nelesen. In R. Casadio and G. Meyers, editors, 5th Workshop on Algorithmics in Bioinformatics - WABI 2005. Lecture Notes in Bioinformatics, Springer, LNBI 3692.

Foreword, in Collected Works of Larry Wos, Larry Wos and Gail Pieper, World Scientific, 2000, pp. v-vi.

Bledsoe memorial resolution. With J. C. Browne, J. Misra, M. Ballantyne, and L. Hines. Faculty Council, University of Texas at Austin, 3 August 1998. 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.pdf.

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.

On the Difficulty of Automating Inductive Reasoning, with J Moore, Remarks made at a workshop on inductive reasoning, Sarasota Springs, NY, June, 1992.

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, 1991, 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 Sharing of Structure in Resolution Programs, with J S. Moore. Technical Report, Metamathematics Unit, Edinburgh University, 1972.

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.

Software System

Instructions for obtaining the Boyer-Moore theorem-proving system (also known as Nqthm) may be found at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/README. 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 current release, including the examples and documentation, comprises approximately 24 megabytes. Running the theorem-prover on these examples generates approximately 200 megabytes of readable proofs.