Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Message-Id: <9309060749.AA23536@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: More on HOL improvement: Resolution
Cc: John.Harrison@cl.cam.ac.uk
Date: Mon, 06 Sep 93 00:49:32 PDT
From: chou@cs.ucla.edu

Another fertile area for improvement is resolution, which I'm sure many
of you, like me, have come to love and hate.  Of course, changing the
existing resolution procedures would wreck too many existing proofs.
But future proofs can profit greatly from an improved set of resolution
tools.  Here are some improvements that I'd like to see:

(1) There should be more flexibility in how RES_CANON works.
    For instance, the exponential blow-up caused by conjunctive
    antecedents is useless most of the time and the user should 

    be able to turn it off.  It would also be nice if the user
    can filter out unwanted theorems from the set of canonical
    implicative theorems.

(2) Similarly, the user should be able to control what resolution
    adds to the assumption list.  (Yes, I know it is possible to
    achieve this by playing with REPEAT_GTCL and IMP_RES_THEN, 

    but I have to admit that thinking about REPEAT_GTCL makes
    my head spin!)

(3) The user should be able to restrict resolution to only a subset
    of the assumption list.

(4) Resolution should be able to handle restricted and pair
    quantifications (and the combination of both!).

- Ching Tsun