Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199602082149.QAA13636@circe.mitre.org>
To: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Cc: guttman@linus.mitre.org, info-hol@leopard.cs.byu.edu,
        reetz <reetz@ira.uka.de>
Subject: Re: hol90 should have more control about proofs 
In-Reply-To: Your message of "Thu, 08 Feb 1996 19:06:37 +0100."
                       <E0tkbg9-0001aS-00@bescot.cl.cam.ac.uk> 
Return-Receipt-To: guttman@linus.mitre.org
Date: Thu, 08 Feb 1996 16:49:17 -0500
From: "Joshua D. Guttman" <guttman@linus.mitre.org>

Donald writes:

>  
>  
>  Ralf raise some very interesting points about proofs, and to what extent
>  a theorem prover should have proofs as first class objects.  These
>  are subjects that I have been giving alot of thought to, and
>  which I think are crucial to the usability of theorem provers.
...
>  Other theorem provers regularly use other interaction languages besides
>  their implementation language, although their ease of programmability
>  sometimes suffer as a result.  

HOL people interested in a different perspective might want to look at
"Proof Script Pragmatics in Imps" 
(<URL:ftp://math.harvard.edu/imps/doc/proof-scripts.dvi.gz>).  

We talked about the issue of whether to keep the proof itself as a
data structure -- and if so, relative to what primitive inferences --
in our overview paper ("Imps: An Interactive Mathematical Proof
System", JAR, Oct 93).

	Josh