Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 6 Jun 1994 15:51:42 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9406060621.AA21012@itd0.dsto.gov.au>
To: hol2000@leopard.cs.byu.edu
Subject: An Alternate Subgoal Package


Well the HOL2000 list seems to have been dormant again for a while,
so here is a little proposal.

I would like to see the subgoal package re-implemented in a different style.
In the current implementation, the proof is constructed in the form of
a tree.  Each node has a sequent (which we would like to show is a theorem),
a number of subtrees, and a proof rule which if given a list of theorems
corresponding to the list of sequents held by the subtrees will return a
theorem corresponding to the sequent held by the node.

We start with a single goal, and by applying tactics we break the goal up
into several subgoal and then go to work on the subgoals.  This process builds
the tree and it finishes when all the leaf nodes of the tree are axioms.
At this point we collaps the tree running the inference rules stored at each
node until we finaly prove the goal we started with (this last bit is all done
automaticaly)

Well it sort of like that any way.

Instead, I think we should start with a therorem of the form (Goal |- Goal).
And progrees the proof by working on the assumptions of the thorem, slowly
reducing them to true via a process of breaking them up into simpler subgoals.
Backwards proof is essentially the same as forwards proof with inference rules
that work on the terms on the left-hand side of the turnstile rather than the
right-hand side.

This approach avoids the current two step process of building the tree and
then collapsing its.  I think this could well result in efficiency gains,
it also has the advantage that there is no danger of using a tactic that runs
OK when building the tree, but where the proof rule falls over then the proof is
finished and the tree is being collapsed.

I should point out that this is not my idea, I don't know whoes it is, perhaps
its a well known concept.  However, as I recall it, it was related to me 
a couple of years ago by Kevin Blackburn of ICL.

Jim