Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 6 Jun 1994 13:46:06 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27181; Mon, 6 Jun 1994 06:42:47 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA27177; Mon, 6 Jun 1994 06:40:59 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 6 Jun 1994 13:40:01 +0100 To: hol2000@leopard.cs.byu.edu Subject: Re: An Alternate Subgoal Package In-Reply-To: Your message of "Mon, 06 Jun 94 15:51:42 +0930." <9406060621.AA21012@itd0.dsto.gov.au> Date: Mon, 06 Jun 94 13:39:55 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:214100:940606124004"@cl.cam.ac.uk> I think Jim's suggestion is an interesting one; I was quite struck by this idea when Rob Arthan and Roger Jones gave a talk about ICL ProofPower. It does seem much cleaner than the current approach. Perhaps someone could fill in a bit more detail about exactly how multiple subgoals are represented, e.g. how is a node in a (backward) proof tree like this one: A ?- t ======================== A1 ?- t1 A2 ?- t2 done? Presumably the hypotheses A* are somehow packaged up into the term structure of the sequent we maintain. This must require a certain amount of care not to identify variables in different subgoals. With type variables there is a worse problem (the ICL crew remarked on this) in that identical type variables are necessarily linked across the whole fringe of the proof tree. It's hard to think of a real situation where this is problematic. (Type quantification would fix it anyway.) John.