Return-Path: Delivery-Date: Received: from toadflax.cs.ucdavis.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <28453-0@swan.cl.cam.ac.uk>; Mon, 29 Jun 1992 16:09:50 +0100 Received: from iris.cs.ucdavis.edu by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.0) id AA23360; Mon, 29 Jun 92 07:55:25 PDT Received: by iris.cs.ucdavis.edu (5.57/UCD.CS.2.0) id AA16590; Mon, 29 Jun 92 07:55:23 -0700 Received: by ux5.tfl.dk (/\==/\ Smail3.1.24.1 #24.1) id ; Mon, 29 Jun 92 16:18 MET DST Message-Id: Date: Mon, 29 Jun 92 16:54 MET DST From: kimdam@dk.tfl (Kim Dam Petersen) To: info-hol@edu.ucdavis.cs Subject: COND_RES_TAC ? Has anyone constructed a COND_RES_TAC i.e. a tactic similar to IMP_RES_TAC, that is able to simplify a condition (_ => _ | _) assumption given a (negated) theorem that matches the selector? More specific that given a goal: ... [!... p => c | a] ... ?- ... and a theorem p` (~p') that matches p reduces to the new goal: ... [!... p => c | a] ... [c' (a')] ?- ... where c' (a') is a substitution of c (a) according to the match. Regards Kim Dam Petersen (kimdam@tfl.dk)