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.

Software System:

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.