Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
X400-Received: by mta relay1.pipex.net in /PRMD=pipex/ADMD=pipex/C=gb/; Relayed;
               Tue, 7 Jun 1994 09:50:45 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Tue, 7 Jun 1994 09:40:38 +0100
Date: Tue, 7 Jun 1994 09:40:38 +0100
X400-Originator: R.B.Jones@win0109.wins.icl.co.uk
X400-Recipients: hol2000@lal.cs.byu.edu
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600003588]
Original-Encoded-Information-Types: ia5 text (2),undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 3588
From: R.B.Jones@win0109.wins.icl.co.uk
Message-Id: <"3588*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: hol2000@leopard.cs.byu.edu
Subject: RE: An alternative subgoal package


------------------------------ Start of body part 1


------------------------------ Start of body part 2


The approach mentioned by Jim Grundy is implemented in ProofPower.

A similar method is implemented in ISABELLE and LAMBDA both of which
predate the ProofPower implementation and are more substantially different
to CLASSIC HOL.

The observation that this can be done in the context of CLASSIC HOL, (subject to
 
the constraint on type instantiation which appears not to be of any practical
significance), is as far as I am aware mine.  The ProofPower goal package which
actually does it was designed and implemented by Kevin Blackburn.
The representations used for subgoals involve a representation of sequents
as closed terms (to avoid identification of free variables) and the constraint
on type instantiation arises from not being able to quantify over type
variables.

The only merit in in present implementation in ProofPower is that tactic
validation takes place at time of evaluation of the tactic by means which are
logically safe.  (When last I knew tactic validation in CLASSIC HOL used mk_thm
and can be used to fake proofs.  This is OK if you don't expect the theorem
prover to provide convincing evidence that a purported proof is not fraudulent).


The reason for exploring this line was because I was interested in finding
a different proof paradigm, providing a meld of what is best in the tactic
approach and using some of the techniques described in Jim Grundy's work
on "windowing".  i.e. integrating tactics with context sensitive term surgery.
However, we never found time to explore these.

There is no need to wait for HOL2000 if you want a goal package implemented
like this, you can do it in CLASSIC HOL.  There is no reason why there
should not be several goal packages supplied.

For HOL2000 more radical thinking would be nice.  Not just different minor
variants on the goal package implementation, but alternation proof paradigms.
Again, anyone interested can experiment with these things in CLASSIC HOL.
(or ProofPower or ....).

Roger Jones
International Computers Limited

------------------------------ End of body part 2