Theorem generators and Theory Generatorsval@netcom.com (Dewey Val Schorre)
Date: Fri, 23 Apr 93 09:12:25 -0700
From: firstname.lastname@example.org (Dewey Val Schorre)
Subject: Theorem generators and Theory Generators
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
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?