Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <17897.9209071041@frogland.inmos.co.uk>
Subject: Re: IMP_RES_TAC
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Mon, 7 Sep 92 11:41:40 BST

Tom Melham has said:
> Victor Carreno <vac@gov.nasa.larc.air16> writes:
> 
> > The problem is that IMP_RES_TAC uses RES_CANON on the implicative theorem.
> > That results in an explosion of the list of theorems produced by RES_CANON,
> > growing exponentially with the number of conjuncts.
> 
> This, very unfortunately, is sometimes quite a serious problem with
> resolution in HOL.  David Shepherd and I have been discussing possible
> fixes, but haven't yet come up with anything obviously better than
> everything else.  Besides which, I am very reluctant to impose another
> major non-compatable change on the user community --- especially one
> which involves a change to the ordering of assumptions.

as Tom says, i have encountered this problem and spent some time
looking into the cause of the problem and as a result have developed
some new resolution tactics that i have been using.

the main differences are

1) in terms of the form P0==>...==>Pn==>(Q0 /\ ... /\ Qm)
i have fixed a "feature" in RES_CANON to stop the conjunct being
split into m different resolvents

2) i use a bit of subterfuge (i.e. ref variable contain a list of
resolved terms) so that the theorem tactic (i.e. STRIP_ASSUME_TAC for
IMP_RES_TAC) isn't applied until all resolved terms have been found ...
this is because you can get situations were resolved terms will
(partially) resolve again putting some unexpected terms in the
assumption list.

3) (which addresses the problem here) for terms of the form 
(P0 /\ ... /\ Pn) ==> Q it first tries to resolve all n implicands 
off (P0 ==> ... ==> Pn ==> Q) and if that fails then it behaves as 
before resolving with all paths through the conjunction expanded into
implciations by RES_CANON. this means that if all of P0 to Pn are
already in the assumption list then it is a linear time resolution
rather than the exponential(?) number of resolutions (which all yield
the same result) as in the existing resolution tactics.

i can understand tom's reluctance to change the "official" resolution
tactics again, given all the fuss last time. my solution is to use my
tactics as a "contrib" package which provides NEW_RES_TAC,
NEW_IMP_RES_TAC, NEW_RES_THEN and NEW_IMP_RES_THEN. i have avoided
releasing it to anyone else yet as i was checking that it did what i
expected but i think it's fairly stable now so i may tidy it up and
post it here soon. this way you can use the modified version if you want
but the old ones are still there.

n.b. the new version *are* incompatible with the old ones (there not
even upwards (or is it downwards) compatible) so it is useful to still
have the old tactics around for old proofs,

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                "i don't consider myself to be narcissitic .... if i had a
                 role model from mythology it would be zeus" - woody allen