Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 25 Sep 1993 13:13:20 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA01331; Sat, 25 Sep 93 05:00:01 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA01327; Sat, 25 Sep 93 04:59:59 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA22635; Sat, 25 Sep 93 05:00:13 -0700 Message-Id: <9309251200.AA22635@maui.cs.ucla.edu> To: info-hol@cs.uidaho.edu Subject: Resolution with filters Date: Sat, 25 Sep 93 05:00:12 PDT From: chou@cs.ucla.edu Here are two simple resolution tactics with filters which I wrote based on Tom Melham's suggestion and have found to be very useful. The idea is that a final resolvent is added to the assumption list only if it satisfy the filter predicate f : term -> bool. For instaince, the following filter: fun no_imp (tm) = not (free_in (--`==>`--) tm) ; throws away all incompletely resolved theorems. - Ching Tsun (*============================================================================ Resolution with filters. ============================================================================*) fun FILTER_STRIP_ASSUME_TAC (f : term -> bool) th = if (f (concl th)) then (STRIP_ASSUME_TAC th) else (ALL_TAC) ; fun FILTER_IMP_RES_TAC (f : term -> bool) th g = IMP_RES_THEN (REPEAT_GTCL IMP_RES_THEN (FILTER_STRIP_ASSUME_TAC f)) th g handle _ => ALL_TAC g ; fun FILTER_RES_TAC (f : term -> bool) g = RES_THEN (REPEAT_GTCL IMP_RES_THEN (FILTER_STRIP_ASSUME_TAC f)) g handle _ => ALL_TAC g ;