the base logic

dam@ai.mit.edu (David McAllester)

Mail folder: QED
Next message: David McAllester: "a multilingual approach"
Previous message: Richard Schroeppel: "comments"
In-reply-to: Bill McCune: "response to Meglicki"
Reply: Pat Lincoln: "the base logic"

From: dam@ai.mit.edu (David McAllester)
Date: Tue, 13 Apr 93 15:14:54 EDT
Message-id: <9304131914.AA00347@spock>
To: mccune@mcs.anl.gov
Cc: qed@mcs.anl.gov
In-reply-to: Bill McCune's message of Tue, 13 Apr 93 10:25:52 CDT <9304131525.AA01463@lutra.mcs.anl.gov>
Subject: the base logic
Sender: qed-owner
Precedence: bulk

One idea is that we simply collect a library of files of theorems.
Each file would be in some language, such as the Boyer-Moore logic,
HOL, nuPRL or Ontic (our language).  I am confident that I could write
a simple routine that would translate definitions and theorems from any
of these languages into Ontic.  This would make it possible to extend
the machine verified library by building on the work of other groups.
Each group could use whatever tools they like best.  Also, the ability
to translate between foundational languages could bypass the need for
a single base logic.

Unfortunately, a multilingual approach would weaken the claim to
correctness --- no single monolithic proof would exist for all
theorems in the library.  I personally think the reduction in
certainty is worth it, especially in getting the project going in the
short term.  Is there a depository somewhere of Boyer-Moore, HOL,
and/or nuPRL thoerems?  At some point I would like to try translating
existing libraries into Ontic so we can build on them further.

	David McAllester