Some Challenges for Automated Theorem Proving

   Dana S. Scott
   University Professor Emeritus
   Carnegie Mellon University
   Visiting Scholar
   University of California, Berkeley

   Every so often I find a theorem that is "self-proving"
   in the sense that, having stated the needed definitions,
   the information in the hypotheses to the theorem somehow
   expands into what is required to establish the conclusion.
   Life is not always so easy, however.  In the talk, proofs
   of several fairly simple theorems will be presented where
   the proof seems to depend on ADDED STRUCTURE.  The question
   in my mind is: How we can guide a (semi)automated system
   to uncover such crucial structure?