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

Alan Bundy <bundy@aisb.ed.ac.uk>

Mail folder: QED
Next message: David McAllester: "Expansion Factors"
Previous message: Alan Bundy: "Re: Boyers Hypothesis"
In-reply-to: Dewey Val Schorre: "Document -- What's Done and What's to be Done"

Via: uk.ac.edinburgh.aifh; Mon, 26 Apr 1993 13:28:32 +0100
Date: Mon, 26 Apr 93 13:28:23 BST
Message-id: <28642.9304261228@etive.aisb.ed.ac.uk>
From: Alan Bundy <bundy@aisb.ed.ac.uk>
Subject: Re: Document -- What's Done and What's to be Done
To: Dewey Val Schorre <val@netcom.com>
In-reply-to: Dewey Val Schorre's message of Sun, 25 Apr 93 15:16:35 -0700
Phone: 44-31-650-2716
Fax: 44-31-650-6516
Fcc: +qed.mai
Cc: qed@aisb.ed.ac.uk
Sender: qed-owner
Precedence: bulk

Val

> Someone could write nqthm as a tactic in HOL. 

	That is essentially what we have been trying to do in the
Clam/Oyster system (see Carolyn Talcott's list).  Clam contains
tactics based on Nqthm. These drive Oyster.  Oyster is a copy of
Nuprl, but it could have been HOL, and at one time we had a
project with a student of Mike Gordon's to have Clam drive HOL.
Adaption to other tactic based provers would not be too
difficult.


			Alan