Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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 11:33:55 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05048;
          Mon, 31 May 93 03:24:43 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA05043;
          Mon, 31 May 93 03:24:36 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA16123;
          Mon, 31 May 93 03:24:50 -0700
Message-Id: <9305311024.AA16123@maui.cs.ucla.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Nicer resolution
Date: Mon, 31 May 93 03:24:49 PDT
From: chou@cs.ucla.edu

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


- Ching Tsun