The Automatic Acquisition of Proof Methods

Abstract

The SHUNYATA program constructs proof methods by analyzing proofs of simple theorems in mathematical theories such as group theory and uses these methods to form proofs of new theorems in the same or in other theories. Such methods are capable of generating proofs of theorems whose complexity represents the state of the art in automated theorem proving. They are composed of elementary functions such as the union of sets and the subset relation. Elementary knowledge about these functions such as descriptions of their domains and their ranges forms the basis of the method acquisition processes. These processes are controlled genetically, which means that SHUNYATA, starting from scratch, constructs a sequence of more and more powerful partial methods each of which forms the basis for the construction of its successor until a complete method is generated.