Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 18 May 1993 10:29:04 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26763;
          Tue, 18 May 93 02:16:22 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA26758;
          Tue, 18 May 93 02:16:16 -0700
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Tue, 18 May 1993 10:14:38 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Tue, 18 May 1993 10:12:31 +0100
Date: Tue, 18 May 1993 10:12:31 +0100
X400-Originator: R.B.Jones@win0109.wins.icl.co.uk
X400-Recipients: info-hol@ted.cs.uidaho.edu
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002585]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2585
From: R.B.Jones@win0109.wins.icl.co.uk
Message-Id: <"2585*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@ted.cs.uidaho.edu
Subject: First order logic in ProofPower

In ProofPower the following one-liner proves that agatha killed
herself.
  apply_tactic (contr_tac THEN REPEAT (all_asm_fc_tac[]));
in 4.1 seconds on a SPARCstation 2.
   (all_asm_fc_tac is doing forward chaining - a bit like
RES_TAC)            Roger Jones, International Computers Limited