L. Wos, "Appendix (to P825): Conjectures Concerning Proof, Design, and Verification," Preprint ANL/MCS-P825A-0500, May 2000. [pdf]
This article focuses on an esoteric but practical use of automated reasoning that may indeed be new to many, especially those concerned primarily with verification of both hardware and software. Specifically, featured are a discussion and some methodology for taking an existing design—of a circuit, a chip, a program, or the like—and refining and improving it in various ways. (Although the methodology is general and does not require the use of a specific program, McCune's program OTTER does offer what is needed. OTTER has played and continues to play the key role in my research, and an interested person can gain access to this program in various ways, not the least of which is through the included CD-ROM in Wos, L., and Pieper, G. W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific Publishing, Singapore (1999).) When success occurs, the result is a new design that may require fewer components, avoid the use of certain costly components, offer more reliability and ease of verification, and, perhaps most important, be more efficient in the contexts of speed and heat generation. Although I have minimal experience in circuit design, circuit validation, program synthesis, program verification, and similar concerns, (at the encouragement of colleagues based on successes to be cited) I present material that might indeed be of substantial interest to manufacturers and programmers.