Delivery-Date: 
Date: Fri, 23 Apr 93 09:12:25 -0700
From: val@netcom.com (Dewey Val Schorre)
Message-Id: <9304231612.AA06019@netcom4.netcom.com>
To: qed@mcs.anl.gov
Subject: Theorem generators and Theory Generators
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


Once QED gets going, we will need not only proof checkers and theorem 
provers, but also "theorem generators" and "theory generators".  A 
theorem generator will work with an existing theory of QED and 
generate interesting theorems that are not yet present. A theory 
generator will scan the QED data base and generate "little theories" 
that could have been used for proofs in existing theories.

Notice the three levels of programs:

     Proof Checkers  -- Always succeeds
     Theorem Provers -- May loop forever but the criterion
                        for success is objective
     Theorem and Theory Generators -- May loop forever and the 
criterion
                        for success can only be subjective

This leads to a new form of Turing's test for artificial intelligence.
When a paper is submitted to a journal, was it written by a human 
mathematician or by one of QED's theorem or theory generators?

Val