Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Tue, 19 Jan 1993 09:57:30 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10687; Tue, 19 Jan 93 01:47:31 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA10682; Tue, 19 Jan 93 01:47:26 -0800 Received: from 192.188.132.2 by relay.pipex.net with SMTP (PP) id <19648-0@relay.pipex.net>; Tue, 19 Jan 1993 09:46:03 +0000 Received: from eccles.dsbc.icl.co.uk by Q.icl.co.uk id AA27952; Tue, 19 Jan 93 09:47:51 GMT Received: on eccles.dsbc.icl.co.uk over UUCP id AA25443; Tue, 19 Jan 93 09:45:26 GMT Received: from wilfrid by iclbra.oasis.icl.co.uk (4.14/) id AA02899; Tue, 19 Jan 93 09:45:39 gmt From: Rob Arthan Date: Tue, 19 Jan 93 09:40:22 GMT Message-Id: <9301190940.1533.20@win.icl.co.uk> To: info-hol@edu.uidaho.cs.ted Subject: Unused Assumptions The problem that the theorem proved by a completed tactic proof may have fewer assumptions than the original goal and may have a different choice of bound variables is one we thought worth solving in ProofPower-HOL. What we did was to make TAC_PROOF and the subgoal package etc. do the extra bit of reasoning required to make sure that what you get is what you wanted. N.B. without something like this a defective tactic can prove something totally different from what you wanted. Rob Arthan. (rda@win.icl.co.uk) ICL Secure Systems, Eskdale Rd. Winnersh, Wokingham Berks. RG11 5TT ------------------------------ End of forwarded message 1