Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 2 Sep 1992 16:45:33 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12170; Wed, 2 Sep 92 08:36:22 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA12165; Wed, 2 Sep 92 08:36:08 -0700 Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Wed, 2 Sep 1992 16:34:40 +0100 To: Victor "A." Carreno Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl Subject: Re: IMP_RES_TAC In-Reply-To: Your message of Tue, 01 Sep 92 15:16:55 -0400. <9209011916.AA00647@air52.larc.nasa.gov> Date: Wed, 02 Sep 92 16:34:29 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.600:02.08.92.15.34.45"@cl.cam.ac.uk> Victor Carreno 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. Tom