Re: Document -- What's Done and What's to be DoneAlan Bundy <firstname.lastname@example.org>
Via: uk.ac.edinburgh.aifh; Mon, 26 Apr 1993 13:28:32 +0100
Date: Mon, 26 Apr 93 13:28:23 BST
From: Alan Bundy <email@example.com>
Subject: Re: Document -- What's Done and What's to be Done
To: Dewey Val Schorre <firstname.lastname@example.org>
In-reply-to: Dewey Val Schorre's message of Sun, 25 Apr 93 15:16:35 -0700
> 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