Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Mon, 5 Oct 1992 13:31:36 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19864;
          Mon, 5 Oct 92 05:16:59 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA19859;
          Mon, 5 Oct 92 05:16:39 -0700
Received: by infix.cs.ruu.nl id AA21527 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Mon, 5 Oct 1992 13:15:41 +0100
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199210051215.AA21527@infix.cs.ruu.nl>
Subject: about the speed of tactical THEN
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Mon, 5 Oct 92 13:15:41 MET
X-Mailer: ELM [version 2.3 PL11]

Hi,

Supposing you want to prove the goal 

   ([],T)

by applying series of tactics T1... TN, you can do this by:

   # prove(T, T1 THEN ... THEN TN)

or by using the subgoal package, ie:

   # set_goal([],T) ;;
   # e T1 ;;
     ...
   # e TN ;;

However, when N is something about 20 and involves stuff like
resolution or tautology proving, the first method using 'prove' tend
to be long, or too long that my stack over flows. Using the subgoal
package gives no problem.

The question is, why can't people just implement THEN just like a
consecutive application of 'expand' s? Will this speed up the 'prove'
style?



Thank you kindly,


Wishnu Prasetya

--