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?