Document -- What's Done and What's to be Done

val@netcom.com (Dewey Val Schorre)
Date: Sun, 25 Apr 93 15:16:35 -0700
From: val@netcom.com (Dewey Val Schorre)
Message-id: <9304252216.AA28228@netcom2.netcom.com>
To: qed@mcs.anl.gov
Subject: Document -- What's Done and What's to be Done
Sender: qed-owner
Precedence: bulk

Suppose we jointly produce a document, sitting in the ftp area beside 
the manifesto, stating what part of mathematics has already been done 
in 
existing theorem provers, and what ought to be done. There would be a 
section for each of the current provers, and a section for what ought 
to 
be done in QED.

David McAlister suggests that if something has been done in one prover

it should be easy to translate over to another. This is because all 
the 
vagnesses would have been removed. After we see what has been done in 
each of the provers, we will see how hard it is to translate this to 
the 
other provers.

Could the proof of Goedel's theorem that Shankar did in nqthm be 
easily 
translated to HOL? Someone could write nqthm as a tactic in HOL. Now 
that doesn't sound very easy. A translator from nqthm sorce language 
to 
HOL would be the easier step.

Even after this were done, would the classists be happy with the 
results? Wouldn't they think there should be quantifiers in the 
statement of the theorem to make it readable? 

An automatic translation from one prover to another would probably 
work 
in some cases, and in others a complete rewrite would be necessary, 
refering to the machine proof only in cases where jorunal proof were 
vague.

The production of this document does not preclude our simultaneously 
working on the base logic or the machine math source language. In fact

the production of this document is not even contrary to Konrad Slind's

cold water view if you consider the "ought to be done" section as 
applying to any theorem proving system and not just to the proposed 
new 
QED.

Val