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; Tue, 21 Sep 1993 13:43:18 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA17815; Tue, 21 Sep 93 05:17:18 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA17811; Tue, 21 Sep 93 05:17:09 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Tue, 21 Sep 93 12:48:43 BST From: David Shepherd Message-Id: <15305.9309211216@frogland.inmos.co.uk> Subject: modified resolution functions To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Tue, 21 Sep 1993 13:16:27 +0100 (BST) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 24506 Ching Tsun asked about improvements to the resolution functions in HOL. I have handled some of the things that he was after. Here is a uuencoded, compressed tar file of the relevant stuff. Basically the enhancements are 1) in a resolving term P1 ==> ... ==> Pn ==> (Q1 /\ .. /\ Qm) the final conjunction is NOT split into m cases. 2) in a resolving term (P1 /\ ... /\ Pn) => Q an initial attempt is made to do n resolutions on P1 ==> ... ==> Pn ==> Q if this fails then it will expand it into the n! permutations of Pi's and try all of those. This is a big saving in the common case where all the Pi's do resolve 3) terminal resolvants are not added to the assumption list until all resolution is finished. This avoids irritating extra terms that occur when some results get added and then start to re-resolve with the resolution terms. The new functions are RESOLVE_TAC RESOLVE_THEN IMP_RESOLVE_TAC IMP_RESOLVE_THEN ANTE_RESOLVE_THEN N.b. very occasionally a tactic that you would expect should work fails with an obscure error message ... after tracking down most of the problems that affected me I could never be bothered to sort out the occasional lurking strangeness. N.b. its all in hol88 so I don't use it any more. I haven't done a hol90 version yet as (a) the existing tactics seem fast enough (at present!) in hol90 and (b) I make more direct use of MATCH_MP on ASSUMEd assumptions now to handle the difficult cases. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "They didn't like the rates, they don't like the poll tax, and they won't like the council tax." - Nicholas Ridley -------------------------------------------------------------------------- begin 644 newres.tar M;F5W"X@=#$@/3T^('0R M(" @+2TM/B @(" @(" @=#$@/3T^("%X+G0R(" @*'@@;F]T(&9R964@:6X@ M=#$I"24@"B4@(" H/W@N=#$I(#T]/B!T,B @+2TM/@DA>"2 ](&1E&-E<'0@=&AA="!I="!A;'-O(&1O M97,@;F]T('-T5]A5]A7!E(#T@8VP*3&ES<" ](&-L"DQI2!@)"I@.SLG7 H)(" @(" G<')I;G1?=&AE;W)Y(& D*F [ M.R=<"@D@(" @("=Q=6ET*"D[.R<@?" D>TAO;'T@?"!T86EL("LQ," ^("0J M+G!R:6YT"@IC;&5A;CH*"7)M("UF("0H3T)*14-44RD*"4!E8VAO("(]/3T^ M(&QI8G)ATAO;'T*"2UM=B D)$A/344O+FAO M;"UI;FET+FUL("0D2$]-12]H;VPM:6YI="YM; H*(PEM=B D)$A/344O+FAO M;"UI;FET+FUL("0D2$]-12]H;VPM:6YI="YM; H*86QL.B D*$]"2D5#5%,I M("0H4%))3E0I"@E 96-H;R B/3T]/B!L:6)R87)Y(&YE=W)E2 _(&9A:6QW:71H(&!)35!? M4D533TQ615]42$5..B!N;R!I;7!L:6-A=&EO;F @:6X*(" @("@H:68@*&ES M7V-O;FH@86YT92D*(" @(" @=&AE;B E('=E('1R>2!T;R!R97-O;'9E(&%L M;"!T:&4@8V]N:G5N8W1S(&9I