Proof Explanation and Revision

Proof structures in traditional automatic theorem proving systems are generally designed for efficiently supporting certain search strategies. They are not meant as a useful representation or presentation of complete proofs: usually only the experts who designed such systems can read them. As a result, complete proofs are of little value and are generally discarded. The failure of such systems to manipulate proofs as values of their own right is one reason why theorem proving systems have not found more use in artificial intelligence and mathematical software. In this paper, we present the design of the X-proof system which attempts to correct this failure of theorem proving systems. Proofs in X are represented by natural and flexible tree-structured deductions. These deductions make very good presentations of proofs, and X has a very simple mechanism for lexicalizing them into readable natural language text. Other proof structures, such as resolution refutations, are used to provide the information necessary for building such proof trees. A programming language based on an extension of LCF tactics and tacticals is available for writing programs which manipulate proof trees. Such programs include interactive proof editors and fully automatic theorem provers. Finally, X is capable of making substantial changes in the presentation of proofs: proofs can be revised or restructured in order to present their deductions in different styles. For example, proofs which contain uses of the indirect proof method can occasionally be automatically restructured into direct proofs.