Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 31 May 1993 16:13:20 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05095; Mon, 31 May 93 08:03:48 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05090; Mon, 31 May 93 08:03:41 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 31 May 1993 16:03:37 +0100 To: chou@cs.ucla.edu Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: Nicer resolution In-Reply-To: Your message of "Mon, 31 May 93 03:24:49 PDT." <9305311024.AA16123@maui.cs.ucla.edu> Date: Mon, 31 May 93 16:03:32 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:149950:930531150343"@cl.cam.ac.uk> Ching Tsun asks: > One of the most annoying features of HOL's resolution is that > it often adds too many resolvents to the assumption list, which > soon becomes unwieldy after a few resolutions. I'd appreciate > any suggestions and/or codes for making resolution nicer. More > specifically, I'd like to know: > > (1) how I can make resolution NOT to add partially resolved resolvents > (ie, those that still contain implications) to the assumption list; > > (2) how I can somehow restrict resolution to only a subset of the > assumption list; > > (3) how I can impose a "filter" to control what resolution adds to the > assumption list The HOL "resolution" tools are, quite frankly, a minor mess. There was ahn extensive rewrite (by me) for version 1.12. This was intended to sort out certain problems with the resolution tools that existed at the time, partly by modularizing and "genericizing" them by the introduction of IMP_RES_THEN and RES_THEN. The result is only a limited success... Unfortunately, any change to resolution tools is very likely to be incompatible. In particular, if people have written tactics that depend on the ordering of assumptions which a revision to resolution then changes, then proofs won't run. So I am wary of changing resolution again, even though its current implementation leaves a lot to be desired. As for the question, here are some suggestions: (1) - supply an appropriate thm_tactic to resolution. Indeed, the version 1.12 rewrite was specifically designed to give you the freedom to do things like this. Here's something rather crude that would work: let RES_ASSUM th = if (free_in "==>" (concl th)) then DISCARD_TAC th else STRIP_ASSUME_TAC th;; REPEAT_GTCL IMP_RES_THEN RES_ASSUM;; (3) You could replace the free_in test by something more selective. Tom