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