ABSTRACT
This chapter mentions some of the exciting new efforts to speed up the search process in Automated Theorem Proving (ATP), and expresses the belief that these new “speed demons” will play a crucial role in modern technology, where a great deal of reasoning power is needed. It then argues that speed alone can never cope with the really difficult theorems that arise from mathematics and challenging application areas, theorems that are nevertheless fairly easy for gifted mathematicians. The authors suggests that a part of the research effort in ATP be directed toward methods which have proven useful (powerful) for human mathematicians, but which have been largely neglected by the ATP community. The field of AI has long recognized the importance of knowledge, and knowledge bases which contain “how-to” methods as well as facts. This is the key ingredient of Expert Systems, which attempt to duplicate expert behavior.
